# Abstract high-level framwork for #SAT

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?

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.

• 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. Nov 3 '15 at 3:13

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$.