Make kissat an optional setting at the module level.

Author: haz

nnf/__init__.py

@@ -60,6 +60,9 @@ 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, kissat, and pysat
+SAT_BACKEND = 'native'
+
 if t.TYPE_CHECKING:
     def memoize(func: T) -> T:
         ...
@@ -594,10 +597,17 @@ def to_CNF(self) -> 'And[Or[Var]]':
         from nnf import tseitin
         return tseitin.to_CNF(self)
 
-    def _cnf_satisfiable(self) -> bool:
-        """Call a SAT solver (kissat) on the presumed CNF theory."""
-        from nnf import kissat
-        return kissat.solve(self) is not None
+    def _cnf_satisfiable(self: 'And[Or[Var]]') -> bool:
+        """Call a SAT solver on the presumed CNF theory."""
+        if 'native' == SAT_BACKEND:
+            return self._cnf_satisfiable_native()
+        elif 'kissat' == SAT_BACKEND:
+            from nnf import kissat
+            return kissat.solve(self) is not None
+        elif 'pysat' == SAT_BACKEND:
+            raise NotImplementedError('pysat backend not yet implemented')
+        else:
+            raise NotImplementedError('Unrecognized SAT backend: '+SAT_BACKEND)
 
     def _cnf_satisfiable_native(self) -> bool:
         """A naive DPLL SAT solver."""