From 339f3e6a4bd876c18a01deafc3c03155445bfdf0 Mon Sep 17 00:00:00 2001
From: Jan Verbeek <jan.verbeek@posteo.nl>
Date: Sat, 29 Aug 2020 20:21:10 +0200
Subject: [PATCH] Create fewer auxiliary variables when converting to CNF

We don't need auxiliary variables for nodes that are required to be
true for the sentence to be true.

Resolves #20.
---
 nnf/tseitin.py | 39 ++++++++++++++++++++++++++++++++++++---
 test_nnf.py    | 15 +++++++++++++++
 2 files changed, 51 insertions(+), 3 deletions(-)

diff --git a/nnf/tseitin.py b/nnf/tseitin.py
index 202e6a0..bfa4ce3 100644
--- a/nnf/tseitin.py
+++ b/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)
diff --git a/test_nnf.py b/test_nnf.py
index 778d117..11880a9 100644
--- a/test_nnf.py
+++ b/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}