search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

Added --short_sat flag to stop minisat when all clauses are sat #23

Closed danbryce closed 10 years ago

danbryce commented 10 years ago

Copy of pull request for old dreal blessed.

soonhokong commented 10 years ago

merged by 4c3c1d95f83abbc0eb488020cf040558c338c42e.

danbryce commented 9 years ago

I found that I didn't completely implement this feature correctly. There are cases where the SAT solver is assigning unassigned variables appearing in satisfied clauses. I've fixed the problem in my local copy, and will request a pull soon. Before I do that I want to clarify whether some behavior I'm seeing is correct.

In one of my test cases, the SAT solver assigns several variables in a row until it gets a model of the CNF. It then pushes the literals on the theory solver's stack, only to find a conflict. The theory solver then backtracks over all of the assignments, including those preceding the conflict. The SAT solver gets this conflicting variable as a conflict clause, and then negates it. Then, the SAT solver proceeds to assign all of the variables it has previously assigned (this time w/o conflict). My question is: is it correct to backtrack over all these assignments even if they are not to blame? It seems the behavior I'm observing is correct, yet inefficient. It should have been possible to backtrack only to the conflicted variable, negate it there, and then proceed.

soonhokong commented 9 years ago

My question is: is it correct to backtrack over all these assignments even if they are not to blame? It seems the behavior I'm observing is correct, yet inefficient.

I think so. I'm not so familiar with this part of the codebase actually..

danbryce commented 9 years ago

Yes, it appears to be correct. I read through the CoreSMTSolver::analyze() method and it does set the backtrack level to zero in some cases. In my case, the conflict clause includes one of the level zero literals. This causes the reason for the conflict to be the other literal (in a two literal conflict). In cases where the reason is a single literal, MiniSAT will backtrack to level zero.

I replaced the line

out_btlevel = 0;

with

out_btlevel = level[var(out_learnt[0])];

so that the backtrack level is the level of the conflict literal and it appears to work fine.

I think the reason for this implementation is that unit conflict clauses are helpful. Mine is unit because one of the two literals is level zero (an assumption). If you can apply them to the root of the search, then you won’t backtrack over them again. The savings depends on whether you will backtrack over the unit conflict and the work you undo by backtracking to level zero. In my case, you save some nodes by not going back to level zero.

On Feb 23, 2015, at 5:40 AM, Soonho Kong notifications@github.com wrote:

My question is: is it correct to backtrack over all these assignments even if they are not to blame? It seems the behavior I'm observing is correct, yet inefficient.

I think so. I'm not so familiar with this part of the codebase actually..

— Reply to this email directly or view it on GitHub.