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

<p>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.</p>

<p>You can take a look at these following papers:</p>

<p>1) <a href="https://www.aaai.org/Papers/AAAI/2000/AAAI00-024.pdf" rel="nofollow">Counting Model using Connected Components</a>. It is implemented in the tool <a href="https://code.google.com/p/relsat/" rel="nofollow">RelSAT</a>.</p>

<p>2) <a href="http://reasoning.cs.ucla.edu/fetch.php?id=145&amp;type=pdf" rel="nofollow">On Compiling CNF into Decision-DNNF</a>. CNF is compited into DNF to count model. The authors have a tool, <a href="http://reasoning.cs.ucla.edu/c2d/" rel="nofollow">c2d</a>, implementing this approach.</p>

CC BY-SA 3.0
2015-11-03T03:13:37.620Z
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.
Fleeep
CC BY-SA 3.0
2015-11-02T18:18:20.873Z
2015-11-02T18:18:20.873Z
sean
<p>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$.</p>

CC BY-SA 3.0
2015-11-04T01:00:47.723Z
2015-11-04T01:00:47.723Z
Kyle Jones
<p>In <a href="http://www.cs.upc.edu/~roberto/papers/lpar04.pdf" rel="nofollow">Abstract DPLL</a> 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.</p>

<p><strong>Question:</strong> 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?</p>

<sat>
Abstract high-level framwork for #SAT
Fleeep
# Abstract high-level framwork for #SAT

(Asked by: username_0 on 2015-11-02)

In [Abstract DPLL](http://www.cs.upc.edu/~roberto/papers/lpar04.pdf) 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?

**Tags:** sat

---

## 2 answers

### Answer by username_1 on 2015-11-02. Score: 2

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](https://www.aaai.org/Papers/AAAI/2000/AAAI00-024.pdf). It is implemented in the tool [RelSAT](https://code.google.com/p/relsat/).

2) [On Compiling CNF into Decision-DNNF](http://reasoning.cs.ucla.edu/fetch.php?id=145&type=pdf). CNF is compited into DNF to count model. The authors have a tool, [c2d](http://reasoning.cs.ucla.edu/c2d/), implementing this approach.

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_2 on 2015-11-04. Score: 0

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


---

