47 lines
1.3 KiB
Python
47 lines
1.3 KiB
Python
|
from sympy.assumptions.cnf import EncodedCNF
|
||
|
|
|
||
|
|
def minisat22_satisfiable(expr, all_models=False, minimal=False):
|
||
|
|
|
||
|
|
if not isinstance(expr, EncodedCNF):
|
||
|
|
exprs = EncodedCNF()
|
||
|
|
exprs.add_prop(expr)
|
||
|
|
expr = exprs
|
||
|
|
|
||
|
|
from pysat.solvers import Minisat22
|
||
|
|
|
||
|
|
# Return UNSAT when False (encoded as 0) is present in the CNF
|
||
|
|
if {0} in expr.data:
|
||
|
|
if all_models:
|
||
|
|
return (f for f in [False])
|
||
|
|
return False
|
||
|
|
|
||
|
|
r = Minisat22(expr.data)
|
||
|
|
|
||
|
|
if minimal:
|
||
|
|
r.set_phases([-(i+1) for i in range(r.nof_vars())])
|
||
|
|
|
||
|
|
if not r.solve():
|
||
|
|
return False
|
||
|
|
|
||
|
|
if not all_models:
|
||
|
|
return {expr.symbols[abs(lit) - 1]: lit > 0 for lit in r.get_model()}
|
||
|
|
|
||
|
|
else:
|
||
|
|
# Make solutions SymPy compatible by creating a generator
|
||
|
|
def _gen(results):
|
||
|
|
satisfiable = False
|
||
|
|
while results.solve():
|
||
|
|
sol = results.get_model()
|
||
|
|
yield {expr.symbols[abs(lit) - 1]: lit > 0 for lit in sol}
|
||
|
|
if minimal:
|
||
|
|
results.add_clause([-i for i in sol if i>0])
|
||
|
|
else:
|
||
|
|
results.add_clause([-i for i in sol])
|
||
|
|
satisfiable = True
|
||
|
|
if not satisfiable:
|
||
|
|
yield False
|
||
|
|
raise StopIteration
|
||
|
|
|
||
|
|
|
||
|
|
return _gen(r)
|