search

NTU-ALComLab / ssatABC

Stochastic SAT solver within ABC
Other
5 stars 2 forks source link

The multiplier for unit clauses might not be correctly computed #12

Closed nianzelee closed 3 years ago

nianzelee commented 3 years ago

In ER-SSAT, if a random variable is a unit clause, the satisfying probability should be multiplied by the variable's probability. This multiplier is pre-computed in the parsing phase and used in the solving phase.

However, it might be wrongly computed when unit clauses of existential variables are present. In the following test case, the multiplier is wrong under unit assumptions 1) 1 0, 2) 1 0 and 3 0.

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
nianzelee commented 3 years ago

This issue should be fixed by commit 376aad4.

nianzelee commented 3 years ago

This issue should be fixed by commit 376aad4.

The fix is not complete. The code snippet below should be invoked for both the Qesto-like and for-all selection solvers. https://github.com/NTU-ALComLab/ssatABC/blob/455a7910bb26e1399897a7f2d7b56ad60af26030/src/ssat/core/SsatSolver.cc#L276-L286

nianzelee commented 3 years ago

The bug should be fixed by commit 531c888.