Merge pull request #29 from QuMuLab/simplify-tautologies

Simplify tautologies

Author: haz

nnf/__init__.py

@@ -574,9 +574,12 @@ def neg(node: NNF) -> NNF:
 
         return neg(self)
 
-    def to_CNF(self) -> 'And[Or[Var]]':
-        """Compile theory to a semantically equivalent CNF formula."""
-        return tseitin.to_CNF(self)
+    def to_CNF(self, simplify: bool = True) -> 'And[Or[Var]]':
+        """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:
         """Call a SAT solver on the presumed CNF theory."""

nnf/tseitin.py

@@ -10,10 +10,12 @@
 from nnf.util import memoize
 
 
-def to_CNF(theory: NNF) -> 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: If True, simplify clauses even if that means eliminating
+                     variables.
     """
 
     clauses = []
@@ -34,7 +36,7 @@ def process_node(node: NNF) -> Var:
 
         aux = Var.aux()
 
-        if 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:
@@ -73,7 +75,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 and any(~v in children for v in children):
                 return
             clauses.append(Or(children))
 

test_nnf.py

@@ -1107,6 +1107,29 @@ def test_models(sentence: nnf.NNF):
     assert model_set(real_models) == model_set(models)
 
 
+@given(NNF())
+def test_toCNF_simplification_names(sentence: nnf.NNF):
+    names1 = set(sentence.vars())
+    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_toCNF_simplification():
+    x = Var("x")
+    T = x | ~x
+
+    T1 = T.to_CNF()
+    T2 = T.to_CNF(simplify=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"), \