Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Obvious inconsistency ignored after optimization in CDCL-Tableaux #1293

Open
Halbaroth opened this issue Feb 12, 2025 · 0 comments · May be fixed by #1294
Open

Obvious inconsistency ignored after optimization in CDCL-Tableaux #1293

Halbaroth opened this issue Feb 12, 2025 · 0 comments · May be fixed by #1294
Labels
bug SAT Relates to the SAT solvers

Comments

@Halbaroth
Copy link
Collaborator

Halbaroth commented Feb 12, 2025 •
edited
Loading

As noticed in #1023, the SAT solver environment is unsat after the optimization. Consider the simplified example:

let env = SAT.empty () in 
SAT.declare env x; 
SAT.assume env (x <= 10);
SAT.maximize env x;
SAT.check_sat ();           (* A *)
SAT.assume env (x <= 10);   (* B *)
SAT.check_sat ();

After A, the environment of the SAT solver is unsat because it contains both the clause x <= 10 and x > 10 at the decision
level 0. We expect that the last assume raises an exception. As explained in PR #1291, the is_unsat field of the SatML environment is true after A, but no Unsat exception is raised at B!

Now replace the command B by SAT.assume env (x + x <= x + 10). Then B raises Unsat as expected.
The issue comes from the wrapper of SatML.assume in Satml_frontend. As the formula x <= 10 is already in the gamma set, Satml_frontend does not send twice the formula to SatML but it doesn't check the status of the SatML environment too:

alt-ergo/src/lib/reasoners/satml_frontend.ml

Lines 763 to 773 in 837293e

let _, ff = ME.find f env.gamma in
match ff with
| None ->
acc
[@ocaml.ppwarning "TODO: should be assert failure?"]
| Some ff ->
if SAT.exists_in_lazy_cnf env.satml ff then acc
else
{acc with
activate = FF.Set.add ff acc.activate;
updated = true}

I believe that checking the status of SatML at the beginning of SAT.assume and SAT.check_sat is the correct fix, but I would like to get a second opinion.

Note: CDCL is also affected.
@Halbaroth Halbaroth added bug SAT Relates to the SAT solvers labels Feb 12, 2025
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Feb 12, 2025
@Halbaroth
Check the status of SatML in Satml_frontend
e5b50fd 
As explained in the issue OCamlPro#1293,
Satml_frontend does not send to SatML a formula already present in its
lazy cnf. In particular, `assume` and `unsat` of `Satml_frontend` can
answer `unknown` for obviously unsat environment. After this commit, we
always check the status of SatML in `assume` and `unsat`.

If the solver is already unsat, the command `unsat` should return the
unsat core. As SatML does not yet support this feature, I returned an
empty explanation.
@Halbaroth Halbaroth linked a pull request Feb 12, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug SAT Relates to the SAT solvers
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Check the status of SatML in Satml_frontend Halbaroth/alt-ergo
1 participant
@Halbaroth