1
$\begingroup$

In Abstract DPLL and some other sources there is a high-level framework/ model explained using states and transitions. I need (to build) such a model for a #SAT algorithm. I do know that #SAT algorithms can be build on top of DPLL or other solvers but i could not find a high-level framework/ model for #SAT.

Question: Is there any such or similar model for a #SAT solving algorithm, or else which rules will have to be added to abstract DPLL to get a #SAT solver?

$\endgroup$
2
$\begingroup$

DPLL can be modified to count model, i.e. to solve #SAT. So yes, you can modify the Abstract DPLL for #SAT.

However, AFAIK DPLL is not state-of-the-art for #SAT, so a DPLL-based framework is neither important nor useful. The Abstract DPLL is useful because it covers most state-of-the-art DPLL-based SAT solvers.

You can take a look at these following papers:

1) Counting Model using Connected Components. It is implemented in the tool RelSAT.

2) On Compiling CNF into Decision-DNNF. CNF is compited into DNF to count model. The authors have a tool, c2d, implementing this approach.

$\endgroup$
  • $\begingroup$ Thank you. I already took a look at those paper, however they do not really offer a high-level framework. Despite that DPLL is not state-of-the-art, i would still be interested if there is a framework extension. I will leave this open a little longer, if there are not any other answers referencing such a extension, i will accept yours. $\endgroup$ – Fleeep Nov 3 '15 at 3:13
0
$\begingroup$

Starting with the transition system for DPLL in definition 1 in the paper, add a state corresponding to the condition: $M \models F$ and no $l$ that appears in $F$ is undefined in $M$. The transition rule for that state should increment the model counter, and add a new clause to $F$ containing a negation of all the literals in $M$. Since the new clause will be unsatisfied the $Backjump$ state will be matched next. Eventually the system will run out models of $F$ and terminate at the $Fail$ state with the model counter containing the number of models of $F$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.