use minisat for incremental solving
Jiang Long
I am using minisat for incremental SAT queries. For the following situation, I would like to keep the original SAT instances but query with different assumptions repeatedly.
I reset the solver, such as learnt, and assignments. But I don't know what to do with 'trail' which seems to be the implication queue(not very sure). I think this needs be cleaned other wise, the solver is not reset completely. If I clear it, I got a crash in ModelVerify.
Anybody has done this and has some suggestion ( a list of things that needs be done to reset the solver to a clean start).
Another situation is to keep existing clauses, and learnt clauses, add additional clauses for the next query ( similar to BMC style). Any suggestions.
Thanks,
-Jiang
Michael Tautschnig
What exactly is "incremental" if you reset everything? The point of incremental
SAT solving (that is, the deemed speedup) is re-using learnt clauses. Otherwise
you could just create a new solver object and go with that. You will need to
rebuild the set of input clauses but usually that is the cheapest part, given
your problems are non-trivial.
Best,
Michael
Jiang Long
I would like to restart without recreating the sat-solver instance. In my case, the set of CNF clauses is not changed, but I want to test a set of cubes if they are satisfiable or not repeatedly. In this situation, it is desirable not to recreate the solver instance on every query, but reuse the solver instance.
-Jiang
Niklas Sörensson
On Sat, Feb 13, 2010 at 11:32 PM, Jiang Long <jiang...@gmail.com> wrote:
> Hi,
>
> I would like to restart without recreating the sat-solver instance. In my
> case, the set of CNF clauses is not changed, but I want to test a set of
> cubes if they are satisfiable or not repeatedly. In this situation, it is
> desirable not to recreate the solver instance on every query, but reuse the
> solver instance.
This is already supported by MiniSat, and you don't need to do
anything else than pass different sets of assumptions to 'solve()'.
Does this help, or did you mean something else?
/Niklas
Jiang Long
I figure out my issue, thanks for the help. I force to clean up various queues in the solver instance by adding a reset call.
-Jiang
Niklas Sörensson
> It is supported by solving the assumptions. But it seems that 'trail' is not
> cleared after every run, which may not be a bug, or just a memory leak.
The trail may filled with units propagated on the top-level before the
call to solve, and clearing it is wrong. You really should not have to
change anything in MiniSat to get this.
> I figure out my issue, thanks for the help. I force to clean up various
> queues in the solver instance by adding a reset call.
Why do you think you have to do this? Maybe I'm missing some context
here that could help my understanding.
Regards,
/Niklas
Jiang Long
The set of CNF formula can get changed every time I call. I may query the satisfiability of a n-lit clause rather than a set of unit literals ( as in the assumptions), which will be changed in the next call. In doing this, the unit literals in trail shall no longer be valid in the next call, that Is why I would need to clear it.
On the other hand, it seems that the solver instance is consistent with regard to the original SAT formula, including not only the trail literals, but also all the conflict clauses. Is this valid with the option setting of removing-satisfied-literals and expensive-reduction in the conflict clauses? (remove_satisfied & expensive_ccmin, currently I disabled them for fear of inconsistency). If this is the case, there is still room for optimize the way I use minisat.
Thanks,
-Jiang
Jiang Long
It seems that I need to clear the assigned value along with trail, otherwise, leave both intact.
-Jiang
Niklas Sörensson
On Tue, Feb 16, 2010 at 2:13 AM, Jiang Long <jiang...@gmail.com> wrote:
> I see. Now, it makes more sense.
>
> The set of CNF formula can get changed every time I call. I may query the
> satisfiability of a n-lit clause rather than a set of unit literals ( as in
> the assumptions), which will be changed in the next call. In doing this,
> the unit literals in trail shall no longer be valid in the next call, that
> Is why I would need to clear it.
>
> On the other hand, it seems that the solver instance is consistent with
> regard to the original SAT formula, including not only the trail literals,
> but also all the conflict clauses. Is this valid with the option setting of
> removing-satisfied-literals and expensive-reduction in the conflict clauses?
> (remove_satisfied & expensive_ccmin, currently I disabled them for fear of
> inconsistency). If this is the case, there is still room for optimize the
> way I use minisat.
If you pass a set of assumptions in the 'assump'-vector as a parameter
to solve, then the solver will check if there is a satisfying solution
that also satisfies the units passed as assumptions. Everything that
is learned in the process is safe to keep forever. If this is all you
need, then you should not have to alter MiniSat at all. It will be
simpler and possibly more efficient that way.
Regards,
/Niklas