search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
386 stars 69 forks source link

solve returns false, but the formula is satisfiable #169

Closed ningit closed 5 months ago

ningit commented 5 months ago

The following piece of code produces False and T as output, i.e. it says that the formula f is not satisfiable, then simplifies it to true with some assumptions. 

from pysat.formula import Atom
from pysat.solvers import Solver

x = Atom(1)
y = Atom(2)  # true
z = Atom(3)  # false
t = Atom(4)  # true

f = ((~y >> x) & t) & ~((y >> z) & (~y >> t))

with Solver(bootstrap_with=f) as solver:
    print(solver.solve())  # False

print(f.simplified([y, ~z, t]))  # T

The formula is satisfiable, so either I am not properly using the library or this is a bug in solve.

alexeyignatiev commented 5 months ago

Most likely it is an issue in classification.

alexeyignatiev commented 5 months ago

@brossignol, by any chance does this work in your patched version?

alexeyignatiev commented 5 months ago

@ningit, I've just checked and it is true that the issue was caused by classification of negation terms, and it seems fixed in the PR prepared by @brossignol.

brossignol commented 5 months ago

The patch fix it.

It is the same problem. The double negation of Atom(2) adds [-2] to the clauses when it should not.

alexeyignatiev commented 5 months ago

Thanks for confirming. Then I am closing it.

ningit commented 5 months ago

It also works for me. Thank you!