Merge pull request #9 from QuMuLab/dynamic-solver-loading

Dynamic solver loading

Author: haz

MANIFEST.in

@@ -0,0 +1 @@
+recursive-include nnf/bin *

docs/nnf.rst

@@ -51,3 +51,11 @@ nnf.tseitin module
    :members:
    :undoc-members:
    :show-inheritance:
+
+nnf.kissat module
+-----------------
+
+.. automodule:: nnf.kissat
+   :members:
+   :undoc-members:
+   :show-inheritance:

nnf/__init__.py

@@ -32,7 +32,8 @@
 
 __all__ = ('NNF', 'Internal', 'And', 'Or', 'Var', 'Aux', 'Builder',
            'all_models', 'complete_models', 'decision', 'true', 'false',
-           'dsharp', 'dimacs', 'amc', 'tseitin', 'operators')
+           'dsharp', 'dimacs', 'amc', 'kissat', 'using_kissat', 'tseitin',
+           'operators')
 
 
 def all_models(names: 't.Iterable[Name]') -> t.Iterator[Model]:
@@ -60,6 +61,26 @@ def all_models(names: 't.Iterable[Name]') -> t.Iterator[Model]:
 T_NNF_co = t.TypeVar('T_NNF_co', bound='NNF', covariant=True)
 _Tristate = t.Optional[bool]
 
+# Valid values: native and kissat
+SAT_BACKEND = 'native'
+
+
+class using_kissat():
+    """Context manager to use the kissat solver in a block of code."""
+
+    def __init__(self) -> None:
+        self.setting = SAT_BACKEND
+
+    def __enter__(self) -> 'using_kissat':
+        global SAT_BACKEND
+        SAT_BACKEND = 'kissat'
+        return self
+
+    def __exit__(self, *_: t.Any) -> None:
+        global SAT_BACKEND
+        SAT_BACKEND = self.setting
+
+
 if t.TYPE_CHECKING:
     def memoize(func: T) -> T:
         ...
@@ -264,10 +285,9 @@ def satisfiable(
 
         if cnf:
             return self._cnf_satisfiable()
-
-        # todo: use a better fallback
-        return any(self.satisfied_by(model)
-                   for model in all_models(self.vars()))
+        else:
+            from nnf import tseitin
+            return tseitin.to_CNF(self)._cnf_satisfiable()
 
     def _satisfiable_decomposable(self) -> bool:
         """Checks satisfiability of decomposable sentences.
@@ -596,6 +616,16 @@ def to_CNF(self) -> 'And[Or[Var]]':
         return tseitin.to_CNF(self)
 
     def _cnf_satisfiable(self) -> bool:
+        """Call a SAT solver on the presumed CNF theory."""
+        if SAT_BACKEND == 'native':
+            return self._cnf_satisfiable_native()
+        elif SAT_BACKEND == 'kissat':
+            from nnf import kissat
+            return kissat.solve(t.cast(And[Or[Var]], self)) is not None
+        else:
+            raise NotImplementedError('Unrecognized SAT backend: '+SAT_BACKEND)
+
+    def _cnf_satisfiable_native(self) -> bool:
         """A naive DPLL SAT solver."""
         def DPLL(clauses: t.FrozenSet[t.FrozenSet[Var]]) -> bool:
             if not clauses:

nnf/bin/LICENSE.kissat

@@ -0,0 +1,19 @@
+Copyright (c) 2019-2020 Armin Biere, Johannes Kepler University Linz, Austria
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

nnf/bin/README.md

@@ -0,0 +1,5 @@
+# Binary files included with python-nnf
+
+## kissat
+
+The `kissat` SAT solver is released under MIT license, and can be found [here](https://github.com/arminbiere/kissat/). The binary included in this directory corresponds to the statically linked version at [this commit](https://github.com/arminbiere/kissat/commit/baef4609163f542dc08f43aef02ce8da0581a2b5). No modifications were made to the `kissat` solver.

nnf/bin/kissat

@@ -0,0 +1,82 @@
+"""Interoperability with `kissat <http://fmv.jku.at/kissat/>`_.
+
+``solve`` invokes the SAT solver directly on the given theory.
+"""
+
+import os
+import shutil
+import subprocess
+import typing as t
+
+from nnf import And, Or, Var, dimacs, Model
+
+__all__ = ('solve',)
+
+
+def solve(
+        sentence: And[Or[Var]],
+        extra_args: t.Sequence[str] = ()
+) -> t.Optional[Model]:
+    """Run kissat to compute a satisfying assignment.
+
+    :param sentence: The CNF sentence to solve.
+    :param extra_args: Extra arguments to pass to kissat.
+    """
+
+    if not sentence.is_CNF():
+        raise ValueError("Sentence must be in CNF")
+
+    if shutil.which('kissat') is not None:
+        SOLVER = 'kissat'
+    else:
+        SOLVER = os.path.join(
+            os.path.dirname(os.path.abspath(__file__)), 'bin', 'kissat'
+        )
+    assert os.path.isfile(SOLVER), "Cannot seem to find kissat solver."
+
+    args = [SOLVER]
+    args.extend(extra_args)
+
+    var_labels = dict(enumerate(sentence.vars(), start=1))
+    var_labels_inverse = {v: k for k, v in var_labels.items()}
+
+    cnf = dimacs.dumps(sentence, mode='cnf', var_labels=var_labels_inverse)
+
+    try:
+        proc = subprocess.Popen(
+            args,
+            stdout=subprocess.PIPE,
+            stdin=subprocess.PIPE,
+            universal_newlines=True
+        )
+        log, _ = proc.communicate(cnf)
+    except OSError as err:
+        if err.errno == 8:
+            print("Error: Attempting to run the kissat binary on an")
+            print("       incompatible system. Consider compiling kissat")
+            print("       natively so it is accessible via the command line.")
+        raise
+
+    # Two known exit codes for the solver
+    if proc.returncode not in [10, 20]:
+        raise RuntimeError(
+            "kissat failed with code {}. Log:\n\n{}".format(
+                proc.returncode, log
+            )
+        )
+
+    # Unsatisfiable
+    if proc.returncode == 20:
+        return None
+
+    assert proc.returncode == 10, "Bad error code. Log:\n\n{}".format(log)
+
+    variable_lines = [
+        line[2:] for line in log.split("\n") if line.startswith("v ")
+    ]
+    literals = [int(num) for line in variable_lines for num in line.split()]
+    assert literals[-1] == 0, "Last entry should be 0. Log:\n\n{}".format(log)
+    literals.pop()
+    model = {var_labels[abs(lit)]: lit > 0 for lit in literals}
+
+    return model

nnf/kissat.py

@@ -46,4 +46,6 @@
         'Documentation': "https://python-nnf.readthedocs.io/",
         'Source': "https://github.com/QuMuLab/python-nnf",
     },
+    include_package_data=True,
+    zip_safe=False,
 )

setup.py

@@ -1,5 +1,6 @@
 import copy
 import pickle
+import platform
 import shutil
 import os
 
@@ -13,7 +14,7 @@
 import nnf
 
 from nnf import (Var, And, Or, amc, dimacs, dsharp, operators,
-                 tseitin, complete_models)
+                 tseitin, complete_models, using_kissat)
 
 settings.register_profile('patient', deadline=2000,
                           suppress_health_check=(HealthCheck.too_slow,))
@@ -821,3 +822,21 @@ def test_complete_models(model: nnf.And[nnf.Var]):
         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)
+
+if (platform.uname().system, platform.uname().machine) == ('Linux', 'x86_64'):
+
+    def test_kissat_uf20():
+        for sentence in uf20_cnf:
+            with using_kissat():
+                assert sentence.satisfiable()
+
+    @given(CNF())
+    def test_kissat_cnf(sentence: And[Or[Var]]):
+        assume(all(len(clause) > 0 for clause in sentence))
+        with using_kissat():
+            assert sentence.satisfiable() == sentence._cnf_satisfiable_native()
+
+    @given(NNF())
+    def test_kissat_nnf(sentence: And[Or[Var]]):
+        with using_kissat():
+            assert sentence.satisfiable() == tseitin.to_CNF(sentence)._cnf_satisfiable_native()