Create fewer auxiliary variables when converting to CNF

nnf/tseitin.py

@@ -26,9 +26,14 @@ def process_node(node: NNF) -> Var:
 
         assert isinstance(node, Internal)
 
-        aux = Var.aux()
         children = {process_node(c) for c in node.children}
 
+        if len(children) == 1:
+            [child] = children
+            return child
+
+        aux = Var.aux()
+
         if any(~var in children for var in children):
             if isinstance(node, And):
                 clauses.append(Or({~aux}))
@@ -50,8 +55,36 @@ def process_node(node: NNF) -> Var:
 
         return aux
 
-    root = process_node(theory)
-    clauses.append(Or({root}))
+    @memoize
+    def process_required(node: NNF) -> None:
+        """For nodes that have to be satisfied.
+
+        This lets us perform some optimizations.
+        """
+        if isinstance(node, Var):
+            clauses.append(Or({node}))
+            return
+
+        assert isinstance(node, Internal)
+
+        if len(node.children) == 1:
+            [child] = node.children
+            process_required(child)
+
+        elif isinstance(node, Or):
+            children = {process_node(c) for c in node.children}
+            if any(~var in children for var in children):
+                return
+            clauses.append(Or(children))
+
+        elif isinstance(node, And):
+            for child in node.children:
+                process_required(child)
+
+        else:
+            raise TypeError(node)
+
+    process_required(theory)
     ret = And(clauses)
     NNF._is_CNF_loose.set(ret, True)
     NNF._is_CNF_strict.set(ret, True)

test_nnf.py

@@ -858,6 +858,7 @@ def test_tseitin(sentence: nnf.NNF):
     T = tseitin.to_CNF(sentence)
     assert T.is_CNF()
     assert T.is_CNF(strict=True)
+    assert tseitin.to_CNF(T) == T
     assert T.forget_aux().equivalent(sentence)
 
     models = list(complete_models(T.models(), sentence.vars() | T.vars()))
@@ -868,6 +869,20 @@ def test_tseitin(sentence: nnf.NNF):
     assert len(models) == sentence.model_count()
 
 
+@given(CNF())
+def test_tseitin_preserves_CNF(sentence: And[Or[Var]]):
+    assert sentence.to_CNF() == sentence
+
+
+def test_tseitin_required_detection():
+    assert a.to_CNF() == And({Or({a})})
+    assert And().to_CNF() == And()
+    assert Or().to_CNF() == And({Or()})
+    assert (a | b).to_CNF() == And({a | b})
+    assert And({a | b, b | c}).to_CNF() == And({a | b, b | c})
+    assert And({And({Or({And({~a})})})}).to_CNF() == And({Or({~a})})
+
+
 @given(models())
 def test_complete_models(model: nnf.And[nnf.Var]):
     m = {v.name: v.true for v in model}