Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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.
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$.
