Re: Digest for minisat@googlegroups.com - 1 update in 1 topic

[Norbert Manthey]

Dear Joe,

The problem is that your new variable turns the learned clause under the current assignment from a unit clause after backjumping, into a clause with 2 unassigned variables (1st position, and the new variable).

You can add the clause to the database as is, but you should not add the clause for unit propagation via the enqueue method.

The case with unsat is tricky to explain. Essentially, the level for your new variable is not set, as well as no truth value is aasigned, nor a reason for assignment. Consequently, during conflict analysis invalid level information might be used, namely level 0 for your new variable, which in turn could lead to a wrong level for the learned clause, 0 again. That might cause problems when consuming the learned clause, finally resulting in unsat. (this is an educated guess, i did not test this statement. Deltadebugging and lots of debug output might help to pinpoint more precisely).

I hope this helps!

Best,

Norbert

Am 13.02.2018 03:38 schrieb <min...@googlegroups.com>:

min...@googlegroups.com

Google Groups

Topic digest
View all topics

• Replacing literals in learnt clause with a fresh variable - 1 Update

Replacing literals in learnt clause with a fresh variable

josephtu...@gmail.com: Feb 11 12:41PM -0800 Hello,   I am using minisat v2.2 and what i want to do is replace 1 or more literals in a recently learnt clause with a fresh variable (i.e. a variable which has not yet appeared in any other clauses in the formula) under certain conditions.   Logically, this should mean that the learnt clause is automatically satisfiable for the remainder of the SAT call (and in subsequent SAT calls), since the fresh variable can just be forced to be true (and this variable never shows up in the formula in the opposite polarity).   However, if for example I put the below code in the search function right before allocating a new learnt clause, things break and the formula will sometimes become unsatisfiable even when it should have been satisfiable.   // if learnt clause size > 1, replace last literal of learnt clause with fresh variable if (learnt_clause.size() > 1) { Var v = newVar(true, true); learnt_clause[learnt_clause.size()-1] = (mkLit(v, 1)); }   Can anyone can give any insight as to what I'm doing wrong?   Thanks, Joe

Back to top

You received this digest because you're subscribed to updates for this group. You can change your settings on the group membership page. To unsubscribe from this group and stop receiving emails from it send an email to minisat+unsubscribe@googlegroups.com.

[josephtu...@gmail.com]

Hi Norbert.

Thank you so much for the reply. That helped me to see what could go wrong by adding such code.

I will experiment trying to add the clause to the database as is (without enqueuing its asserting literal), and seeing if that produces a sound result.

Thanks,

Joe

On Tuesday, February 13, 2018 at 8:46:13 AM UTC-5, Norbert Manthey wrote:

Dear Joe,

The problem is that your new variable turns the learned clause under the current assignment from a unit clause after backjumping, into a clause with 2 unassigned variables (1st position, and the new variable).

You can add the clause to the database as is, but you should not add the clause for unit propagation via the enqueue method.

The case with unsat is tricky to explain. Essentially, the level for your new variable is not set, as well as no truth value is aasigned, nor a reason for assignment. Consequently, during conflict analysis invalid level information might be used, namely level 0 for your new variable, which in turn could lead to a wrong level for the learned clause, 0 again. That might cause problems when consuming the learned clause, finally resulting in unsat. (this is an educated guess, i did not test this statement. Deltadebugging and lots of debug output might help to pinpoint more precisely).

I hope this helps!

Best,

Norbert

Am 13.02.2018 03:38 schrieb 

Google Groups

Topic digest
View all topics

• Replacing literals in learnt clause with a fresh variable - 1 Update

Replacing literals in learnt clause with a fresh variable

josephtu...@gmail.com: Feb 11 12:41PM -0800 Hello,   I am using minisat v2.2 and what i want to do is replace 1 or more literals in a recently learnt clause with a fresh variable (i.e. a variable which has not yet appeared in any other clauses in the formula) under certain conditions.   Logically, this should mean that the learnt clause is automatically satisfiable for the remainder of the SAT call (and in subsequent SAT calls), since the fresh variable can just be forced to be true (and this variable never shows up in the formula in the opposite polarity).   However, if for example I put the below code in the search function right before allocating a new learnt clause, things break and the formula will sometimes become unsatisfiable even when it should have been satisfiable.   // if learnt clause size > 1, replace last literal of learnt clause with fresh variable if (learnt_clause.size() > 1) { Var v = newVar(true, true); learnt_clause[learnt_clause.size()-1] = (mkLit(v, 1)); }   Can anyone can give any insight as to what I'm doing wrong?   Thanks, Joe

Back to top

You received this digest because you're subscribed to updates for this group. You can change your settings on the group membership page.

To unsubscribe from this group and stop receiving emails from it send an email to minisat+u...@googlegroups.com.

[Allen Van Gelder]

Following up on Norbert remarks, I think there was a paper published in 2005 about incremental minisat.

Others can correct me if my memory is wrong, but in any case it sounds like Joseph Turner might be

trying to do something that the facilities of incremental minisat are useful for.

--AVG

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.