Wrong answer if some unit clauses of variables in e1 level

[qmo1222]

Bug Observation

Correct answer for the following test case.

p cnf 5 6
e 1 0
e 3 0
r 0.285714 2 0
r 0.461538 4 0
r 0.307692 5 0
-2 -1 0
2 1 0
1 -4 -3 0
1 4 3 0
-1 -5 -3 0
-1 5 3 0

But if I add a unit clause.

3 0

The answer will be 0 (wrong answer).

However, the following test case will be correct.

p cnf 2 3
e 1 0
r 0.285714 2 0
-2 -1 0
2 1 0
-1 0

Code Modification

I try to fix it by remove line 166 in src/ssat/core/SsatSolver.cc. And add else condition to line 168~172 as

// save unit clauses
if (lits.size() == 1) {
    unitClause.push();
    lits.copyTo(_unitClause.last());
}
else
    S.addClause_(lits);

This modification makes the above instance correct. But the solver cannot solve sand-castle benchmarks.

[nianzelee]

Thanks a lot for greatly simplifying the buggy test case. I will take a look.

[nianzelee]

Disabling the technique pure literal assertion (by specifying ssat -r) seems to fix this bug, without the patch suggested by @qmo1222.

I don't completely understand the patch: why shouldn't we add unit clauses into the solver?

Edit: Using the assumptions 1 0 or 1 0 and 3 0 give wrong answers again. It is caused by a wrong multiplier, as described in #12

[nianzelee]

@qmo1222 : Could you please confirm that the bug has been fixed? The solver should be able to obtain the correct answer without disabling the pure-literal assertion. Please read the above commit message for more details.

[qmo1222]

The bug is fixed for this small case. The big case change its result from 0 to some probability value, but the answer is still incorrect. I'm trying to find another small case to generate the condition.