search

NTU-ALComLab / ssatABC

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

Computing satisfying probability while the solver contains no clause #2

Closed nianzelee closed 4 years ago

nianzelee commented 4 years ago

In src/ssat/core/ssatERSolve.cc:SsatSolver::erSolve2SSAT, after _s2 gives an assignment to exist variables, _s1 would solve the matrix under the given assumption. If the matrix is satisfiable under the assumption, model counting is used to compute the satisfying probability of the residual formula.

Question: when there is no clause left in _s1 after the assumption, is it true that the satisfying probability equals 1?

No, the satisfying probability should be the product of probabilities of random variables based on their assignments.

Currently this is considered as a special case to handle, but a solution has not yet been developed. https://github.com/nianzelee/ssatABC/blob/e036412bf8bc6ee7686bc9c74cdb0b1dece8dfbe/src/ssat/core/ssatERSolve.cc#L115-L120

nianzelee commented 4 years ago

In commit 2a26cac a quick fix is done for the situation when there is no clause left after simplification by SAT solver. In this situation, the satisfying probability is the product of the probabilities of random variables, based on their assignments.

The remaining question is: can this fix be used in the main ER-SSAT loop? That is, when _s2 assigns exist variables and _s1 becomes empty under this assignment, can we compute the probability in the same way? What about the learnt clause?

nianzelee commented 4 years ago

In commit d6f2790, the original fix is moved into SsatSolver::erSolveWMC. As explained in the commit message, the learning process will work fine in such situation, so the only thing to change is to handle the computation of satisfying probability.

@yen-shi : would you please let me know if you agree with this fix? If you agree then this issue can be closed and this bug-fixing branch can be merged back to master.

yen-shi commented 4 years ago

Just left a comment on the commit, and it looks good to me.

nianzelee commented 4 years ago

The fix has been integrated into master (with rebase). The bug-fixing branch will be deleted and this issue will be closed.