Spaces:
Running
Running
File size: 1,317 Bytes
6a86ad5 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 |
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)
|