Spaces:
Running
Running
File size: 1,207 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 |
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)
|