Merge pull request #6 from QuMuLab/tseitin

Tseitin Encoding

Author: haz

CONTRIBUTING.md

@@ -0,0 +1,10 @@
+# Contributing to python-nnf
+
+More information coming soon.
+
+## Notes for now
+
+- `tox -e py3`
+- Set notation for Internal nodes (rather than lists)
+- Use of `@memoize`
+- Use of Typing / mypy

nnf/__init__.py

@@ -18,7 +18,9 @@
 import functools
 import itertools
 import operator
+import os
 import typing as t
+import uuid
 
 from collections import Counter
 
@@ -28,8 +30,9 @@
 Name = t.Hashable
 Model = t.Dict[Name, bool]
 
-__all__ = ('NNF', 'Internal', 'And', 'Or', 'Var', 'Builder', 'all_models',
-           'decision', 'true', 'false', 'dsharp', 'dimacs', 'amc', 'operators')
+__all__ = ('NNF', 'Internal', 'And', 'Or', 'Var', 'Aux', 'Builder',
+           'all_models', 'complete_models', 'decision', 'true', 'false',
+           'dsharp', 'dimacs', 'amc', 'tseitin', 'operators')
 
 
 def all_models(names: 't.Iterable[Name]') -> t.Iterator[Model]:
@@ -587,6 +590,11 @@ def neg(node: NNF) -> NNF:
 
         return neg(self)
 
+    def to_CNF(self) -> 'And[Or[Var]]':
+        """Compile theory to a semantically equivalent CNF formula."""
+        from nnf import tseitin
+        return tseitin.to_CNF(self)
+
     def _cnf_satisfiable(self) -> bool:
         """A naive DPLL SAT solver."""
         def DPLL(clauses: t.FrozenSet[t.FrozenSet[Var]]) -> bool:
@@ -1067,7 +1075,13 @@ def name(node: NNF) -> int:
             if node not in names:
                 number = next(counter)
                 if isinstance(node, Var):
-                    label = str(node.name).replace('"', r'\"')
+                    if isinstance(node.name, Aux):
+                        # This matches the repr, but in this context it could
+                        # be reasonable to number them instead
+                        label = "<{}>".format(node.name.hex[:4])
+                    else:
+                        label = str(node.name)
+                    label = label.replace('"', r'\"')
                     color = colors['var']
                     if not node.true:
                         label = '¬' + label
@@ -1265,6 +1279,15 @@ def __deepcopy__(self: T_NNF, memodict: t.Dict[t.Any, t.Any]) -> T_NNF:
         return self
 
 
+class Aux(uuid.UUID):
+    """Unique UUID labels for auxiliary variables.
+
+    Don't instantiate directly, call :meth:`Var.aux` instead.
+    """
+
+    __slots__ = ()
+
+
 class Var(NNF):
     """A variable, or its negation.
 
@@ -1320,10 +1343,12 @@ def __delattr__(self, name: str) -> None:
 
     def __repr__(self) -> str:
         if isinstance(self.name, str):
-            return str(self.name) if self.true else "~{}".format(self.name)
+            base = str(self.name)
+        elif isinstance(self.name, Aux):
+            base = "<{}>".format(self.name.hex[:4])
         else:
             base = "{}({!r})".format(self.__class__.__name__, self.name)
-            return base if self.true else '~' + base
+        return base if self.true else '~' + base
 
     def __invert__(self) -> 'Var':
         return Var(self.name, not self.true)
@@ -1350,6 +1375,12 @@ def __setstate__(self, state: t.Tuple[Name, bool]) -> None:
         object.__setattr__(self, 'name', state[0])
         object.__setattr__(self, 'true', state[1])
 
+    @staticmethod
+    def aux() -> 'Var':
+        """Create an auxiliary variable with a unique label."""
+        # See implementation of uuid.uuid4()
+        return Var(Aux(bytes=os.urandom(16), version=4))
+
 
 class Internal(NNF, t.Generic[T_NNF_co]):
     """Base class for internal nodes, i.e. And and Or nodes."""
@@ -1539,6 +1570,21 @@ def map(self, func: t.Callable[[T_NNF_co], U_NNF]) -> 'Or[U_NNF]':
             ...
 
 
+def complete_models(
+        models: t.Iterable[Model],
+        names: t.Iterable[Name]
+) -> t.Iterator[Model]:
+    names = frozenset(names)
+    diff = None
+    for model in models:
+        if diff is None:
+            diff = names - model.keys()
+        for supplement in all_models(diff):
+            new = model.copy()
+            new.update(supplement)
+            yield new
+
+
 def decision(
         var: Var,
         if_true: T_NNF,

nnf/tseitin.py

@@ -0,0 +1,54 @@
+"""Transformations using the well-known Tseitin encoding
+<https://en.wikipedia.org/wiki/Tseytin_transformation>
+
+The Tseitin transformation converts any arbitrary circuit to one in CNF in
+polynomial time/space. It does so at the cost of introducing new variables
+(one for each logical connective in the formula).
+"""
+
+from nnf import NNF, Var, And, Or, memoize, Internal
+
+
+def to_CNF(theory: NNF) -> And[Or[Var]]:
+    """Convert an NNF into CNF using the Tseitin Encoding.
+
+    :param theory: Theory to convert.
+    """
+
+    clauses = []
+
+    @memoize
+    def process_node(node: NNF) -> Var:
+
+        if isinstance(node, Var):
+            return node
+
+        assert isinstance(node, Internal)
+
+        aux = Var.aux()
+        children = {process_node(c) for c in node.children}
+
+        if any(~var in children for var in children):
+            if isinstance(node, And):
+                clauses.append(Or({~aux}))
+            else:
+                clauses.append(Or({aux}))
+
+        elif isinstance(node, And):
+            clauses.append(Or({~c for c in children} | {aux}))
+            for c in children:
+                clauses.append(Or({~aux, c}))
+
+        elif isinstance(node, Or):
+            clauses.append(Or(children | {~aux}))
+            for c in children:
+                clauses.append(Or({~c, aux}))
+
+        else:
+            raise TypeError(node)
+
+        return aux
+
+    root = process_node(theory)
+    clauses.append(Or({root}))
+    return And(clauses)

test_nnf.py

@@ -12,7 +12,8 @@
 
 import nnf
 
-from nnf import Var, And, Or, amc, dimacs, dsharp, operators
+from nnf import (Var, And, Or, amc, dimacs, dsharp, operators,
+                 tseitin, complete_models)
 
 settings.register_profile('patient', deadline=2000,
                           suppress_health_check=(HealthCheck.too_slow,))
@@ -120,13 +121,19 @@ def CNF(draw):
 
 @st.composite
 def models(draw):
-    return And(Var(name, draw(st.booleans()))
-               for name in range(1, 9))
+    return And(
+        Var(name, draw(st.booleans()))
+        for name in range(1, draw(st.integers(min_value=1, max_value=9)))
+    )
 
 
 @st.composite
 def MODS(draw):
-    return Or(draw(st.frozensets(models())))
+    num = draw(st.integers(min_value=1, max_value=9))
+    amount = draw(st.integers(min_value=0, max_value=10))
+    return Or(And(Var(name, draw(st.booleans()))
+                  for name in range(1, num))
+              for _ in range(amount))
 
 
 @st.composite
@@ -702,7 +709,7 @@ def test_nor(a: nnf.NNF, b: nnf.NNF):
 
 
 @given(NNF(), NNF())
-def test_implies(a: nnf.NNF, b: nnf.NNF):
+def test_implies2(a: nnf.NNF, b: nnf.NNF):
     c = operators.implies(a, b)
     for model in nnf.all_models(c.vars()):
         assert ((a.satisfied_by(model) and not b.satisfied_by(model)) !=
@@ -771,3 +778,46 @@ def test_dsharp_compile_converting_names(sentence: And[Or[Var]]):
         assert all(isinstance(name, str) for name in compiled.vars())
         if sentence.satisfiable():
             assert sentence.equivalent(compiled)
+
+
+@given(NNF())
+def test_tseitin(sentence: nnf.NNF):
+
+    # Assumption to reduce the time in testing
+    assume(sentence.size() <= 10)
+
+    T = tseitin.to_CNF(sentence)
+    assert T.is_CNF()
+
+    # TODO: Once forgetting/projection is implemented,
+    #       do this more complete check
+    # aux = filter(lambda x: 'aux' in str(x.name), T.vars())
+    # assert T.forget(aux).equivalent(sentence)
+
+    models = list(complete_models(T.models(), sentence.vars() | T.vars()))
+
+    for mt in models:
+        assert sentence.satisfied_by(mt)
+
+    assert len(models) == sentence.model_count()
+
+@given(models())
+def test_complete_models(model: nnf.And[nnf.Var]):
+    m = {v.name: v.true for v in model}
+    neg = {v.name: not v.true for v in model}
+
+    zero = list(complete_models([m], model.vars()))
+    assert len(zero) == 1
+
+    one = list(complete_models([m], model.vars() | {"test1"}))
+    assert len(one) == 2
+
+    two = list(complete_models([m], model.vars() | {"test1", "test2"}))
+    assert len(two) == 4
+    assert all(x.keys() == m.keys() | {"test1", "test2"} for x in two)
+
+    if m:
+        multi = list(complete_models([m, neg], model.vars() | {"test1", "test2"}))
+        assert len(multi) == 8
+        assert len({frozenset(x.items()) for x in multi}) == 8  # all unique
+        assert all(x.keys() == m.keys() | {"test1", "test2"} for x in multi)

tox.ini

@@ -6,11 +6,11 @@ toxworkdir = {env:TOX_WORK_DIR:.tox}
 deps =
     pytest
     flake8
-    py{35,36,37,38}: mypy
+    py{3,35,36,37,38}: mypy
     hypothesis
 commands =
     flake8 nnf
-    py{35,36,37,38}: python -m mypy --strict nnf
+    py{3,35,36,37,38}: python -m mypy --strict nnf
     pytest
-    py{36,37,38,py3}: python -m doctest nnf/__init__.py -o ELLIPSIS
+    py{3,36,37,38,py3}: python -m doctest nnf/__init__.py -o ELLIPSIS
     python examples/socialchoice.py