42 lines
1.2 KiB
Python
42 lines
1.2 KiB
Python
|
from sympy.assumptions.cnf import EncodedCNF
|
||
|
|
|
||
|
|
|
||
|
|
def pycosat_satisfiable(expr, all_models=False):
|
||
|
|
import pycosat
|
||
|
|
if not isinstance(expr, EncodedCNF):
|
||
|
|
exprs = EncodedCNF()
|
||
|
|
exprs.add_prop(expr)
|
||
|
|
expr = exprs
|
||
|
|
|
||
|
|
# 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
|
||
|
|
|
||
|
|
if not all_models:
|
||
|
|
r = pycosat.solve(expr.data)
|
||
|
|
result = (r != "UNSAT")
|
||
|
|
if not result:
|
||
|
|
return result
|
||
|
|
return {expr.symbols[abs(lit) - 1]: lit > 0 for lit in r}
|
||
|
|
else:
|
||
|
|
r = pycosat.itersolve(expr.data)
|
||
|
|
result = (r != "UNSAT")
|
||
|
|
if not result:
|
||
|
|
return result
|
||
|
|
|
||
|
|
# Make solutions SymPy compatible by creating a generator
|
||
|
|
def _gen(results):
|
||
|
|
satisfiable = False
|
||
|
|
try:
|
||
|
|
while True:
|
||
|
|
sol = next(results)
|
||
|
|
yield {expr.symbols[abs(lit) - 1]: lit > 0 for lit in sol}
|
||
|
|
satisfiable = True
|
||
|
|
except StopIteration:
|
||
|
|
if not satisfiable:
|
||
|
|
yield False
|
||
|
|
|
||
|
|
return _gen(r)
|