From e8dee23b43f17644d035cc58adfaaa5f32ff3f5f Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Thu, 8 Dec 2022 21:13:35 -0500 Subject: [PATCH 1/7] Adding option to avoid simplification in conversion to CNF. --- nnf/__init__.py | 4 ++-- nnf/tseitin.py | 4 ++-- test_nnf.py | 15 +++++++++++++++ 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 0c1e3a9..d107f09 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -574,9 +574,9 @@ def neg(node: NNF) -> NNF: return neg(self) - def to_CNF(self) -> 'And[Or[Var]]': + def to_CNF(self, simplify_tautologies=True) -> 'And[Or[Var]]': """Compile theory to a semantically equivalent CNF formula.""" - return tseitin.to_CNF(self) + return tseitin.to_CNF(self, simplify_tautologies) def _cnf_satisfiable(self) -> bool: """Call a SAT solver on the presumed CNF theory.""" diff --git a/nnf/tseitin.py b/nnf/tseitin.py index bfa4ce3..55d685b 100644 --- a/nnf/tseitin.py +++ b/nnf/tseitin.py @@ -10,7 +10,7 @@ from nnf.util import memoize -def to_CNF(theory: NNF) -> And[Or[Var]]: +def to_CNF(theory: NNF, simplify_tautologies=True) -> And[Or[Var]]: """Convert an NNF into CNF using the Tseitin Encoding. :param theory: Theory to convert. @@ -73,7 +73,7 @@ def process_required(node: NNF) -> None: elif isinstance(node, Or): children = {process_node(c) for c in node.children} - if any(~var in children for var in children): + if simplify_tautologies and any(~var in children for var in children): return clauses.append(Or(children)) diff --git a/test_nnf.py b/test_nnf.py index f1d4a9c..427fea9 100644 --- a/test_nnf.py +++ b/test_nnf.py @@ -1107,6 +1107,21 @@ def test_models(sentence: nnf.NNF): assert model_set(real_models) == model_set(models) +def test_tautology_simplification(): + x = Var("x") + T = x | ~x + + T1 = T.to_CNF() + T2 = T.to_CNF(simplify_tautologies=False) + + assert T1 == nnf.true + assert T1.is_CNF() + + assert T2 != nnf.true + assert T2 == And({Or({~x, x})}) + assert T2.is_CNF() + + @config(auto_simplify=False) def test_nesting(): a, b, c, d, e, f = Var("a"), Var("b"), Var("c"), Var("d"), \ From 207074aedd5c67f1d58359877832338373c46900 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Thu, 8 Dec 2022 21:20:39 -0500 Subject: [PATCH 2/7] Reducing line length. --- nnf/tseitin.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nnf/tseitin.py b/nnf/tseitin.py index 55d685b..5b4f02f 100644 --- a/nnf/tseitin.py +++ b/nnf/tseitin.py @@ -73,7 +73,7 @@ def process_required(node: NNF) -> None: elif isinstance(node, Or): children = {process_node(c) for c in node.children} - if simplify_tautologies and any(~var in children for var in children): + if simplify_tautologies and any(~v in children for v in children): return clauses.append(Or(children)) From 1523e8add41a6b186dc038cdcf93d3a224b32ef2 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Thu, 8 Dec 2022 21:36:42 -0500 Subject: [PATCH 3/7] Some mypy fixes. --- nnf/__init__.py | 2 +- nnf/tseitin.py | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index d107f09..0e1b80d 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -574,7 +574,7 @@ def neg(node: NNF) -> NNF: return neg(self) - def to_CNF(self, simplify_tautologies=True) -> 'And[Or[Var]]': + def to_CNF(self, simplify_tautologies: bool = True) -> 'And[Or[Var]]': """Compile theory to a semantically equivalent CNF formula.""" return tseitin.to_CNF(self, simplify_tautologies) diff --git a/nnf/tseitin.py b/nnf/tseitin.py index 5b4f02f..9f58e6d 100644 --- a/nnf/tseitin.py +++ b/nnf/tseitin.py @@ -10,10 +10,11 @@ from nnf.util import memoize -def to_CNF(theory: NNF, simplify_tautologies=True) -> And[Or[Var]]: +def to_CNF(theory: NNF, simplify_tautologies: bool = True) -> And[Or[Var]]: """Convert an NNF into CNF using the Tseitin Encoding. :param theory: Theory to convert. + :param simplify_tautologies: If True, remove clauses that are always true. """ clauses = [] From 21ff041bcb1311717fb884543705ba4cbbee71ef Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Fri, 9 Dec 2022 14:17:50 -0500 Subject: [PATCH 4/7] Adding extra test for name preservation, and fixed bug for bottom clauses. --- nnf/tseitin.py | 2 +- test_nnf.py | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/nnf/tseitin.py b/nnf/tseitin.py index 9f58e6d..b96a742 100644 --- a/nnf/tseitin.py +++ b/nnf/tseitin.py @@ -35,7 +35,7 @@ def process_node(node: NNF) -> Var: aux = Var.aux() - if any(~var in children for var in children): + if simplify_tautologies and any(~var in children for var in children): if isinstance(node, And): clauses.append(Or({~aux})) else: diff --git a/test_nnf.py b/test_nnf.py index 427fea9..abd0b41 100644 --- a/test_nnf.py +++ b/test_nnf.py @@ -1107,6 +1107,14 @@ def test_models(sentence: nnf.NNF): assert model_set(real_models) == model_set(models) +@given(NNF()) +def test_tautology_simplification_names(sentence: nnf.NNF): + names1 = set(sentence.vars()) + T = sentence.to_CNF(simplify_tautologies=False) + names2 = set({v for v in T.vars() if not isinstance(v, nnf.Aux)}) + assert names1 == names2 + + def test_tautology_simplification(): x = Var("x") T = x | ~x From 279052b03f726e6d61621ba963912f3153533f5b Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Fri, 9 Dec 2022 22:33:37 -0500 Subject: [PATCH 5/7] Refactor the parameter name. --- nnf/__init__.py | 4 ++-- nnf/tseitin.py | 8 ++++---- test_nnf.py | 8 ++++---- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 0e1b80d..d568d48 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -574,9 +574,9 @@ def neg(node: NNF) -> NNF: return neg(self) - def to_CNF(self, simplify_tautologies: bool = True) -> 'And[Or[Var]]': + def to_CNF(self, simplify: bool = True) -> 'And[Or[Var]]': """Compile theory to a semantically equivalent CNF formula.""" - return tseitin.to_CNF(self, simplify_tautologies) + return tseitin.to_CNF(self, simplify) def _cnf_satisfiable(self) -> bool: """Call a SAT solver on the presumed CNF theory.""" diff --git a/nnf/tseitin.py b/nnf/tseitin.py index b96a742..fa908b6 100644 --- a/nnf/tseitin.py +++ b/nnf/tseitin.py @@ -10,11 +10,11 @@ from nnf.util import memoize -def to_CNF(theory: NNF, simplify_tautologies: bool = True) -> And[Or[Var]]: +def to_CNF(theory: NNF, simplify: bool = True) -> And[Or[Var]]: """Convert an NNF into CNF using the Tseitin Encoding. :param theory: Theory to convert. - :param simplify_tautologies: If True, remove clauses that are always true. + :param simplify: If True, remove clauses that are always true. """ clauses = [] @@ -35,7 +35,7 @@ def process_node(node: NNF) -> Var: aux = Var.aux() - if simplify_tautologies and any(~var in children for var in children): + if simplify and any(~var in children for var in children): if isinstance(node, And): clauses.append(Or({~aux})) else: @@ -74,7 +74,7 @@ def process_required(node: NNF) -> None: elif isinstance(node, Or): children = {process_node(c) for c in node.children} - if simplify_tautologies and any(~v in children for v in children): + if simplify and any(~v in children for v in children): return clauses.append(Or(children)) diff --git a/test_nnf.py b/test_nnf.py index abd0b41..28111cc 100644 --- a/test_nnf.py +++ b/test_nnf.py @@ -1108,19 +1108,19 @@ def test_models(sentence: nnf.NNF): @given(NNF()) -def test_tautology_simplification_names(sentence: nnf.NNF): +def test_toCNF_simplification_names(sentence: nnf.NNF): names1 = set(sentence.vars()) - T = sentence.to_CNF(simplify_tautologies=False) + T = sentence.to_CNF(simplify=False) names2 = set({v for v in T.vars() if not isinstance(v, nnf.Aux)}) assert names1 == names2 -def test_tautology_simplification(): +def test_toCNF_simplification(): x = Var("x") T = x | ~x T1 = T.to_CNF() - T2 = T.to_CNF(simplify_tautologies=False) + T2 = T.to_CNF(simplify=False) assert T1 == nnf.true assert T1.is_CNF() From 4a63b5015b4955368a22adbb40e109ff8194f992 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Sun, 11 Dec 2022 21:47:49 -0500 Subject: [PATCH 6/7] Update nnf/tseitin.py Co-authored-by: Jan Verbeek --- nnf/tseitin.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/nnf/tseitin.py b/nnf/tseitin.py index fa908b6..85be85e 100644 --- a/nnf/tseitin.py +++ b/nnf/tseitin.py @@ -14,7 +14,8 @@ def to_CNF(theory: NNF, simplify: bool = True) -> And[Or[Var]]: """Convert an NNF into CNF using the Tseitin Encoding. :param theory: Theory to convert. - :param simplify: If True, remove clauses that are always true. + :param simplify: If True, simplify clauses even if that means eliminating + variables. """ clauses = [] From a025fddb2cbc437b50cd9fe6b82fb10aa1a5616d Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Sun, 11 Dec 2022 21:50:55 -0500 Subject: [PATCH 7/7] Adding documentation for the new to_CNF parameter. --- nnf/__init__.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index d568d48..538e69b 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -575,7 +575,10 @@ def neg(node: NNF) -> NNF: return neg(self) def to_CNF(self, simplify: bool = True) -> 'And[Or[Var]]': - """Compile theory to a semantically equivalent CNF formula.""" + """Compile theory to a semantically equivalent CNF formula. + + :param simplify: If True, simplify clauses even if that means + eliminating variables.""" return tseitin.to_CNF(self, simplify) def _cnf_satisfiable(self) -> bool: