Replacing literals in learnt clause with a fresh variable

[josephtu...@gmail.com]

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