Could anyone please point to one or more websites where is possible to download a working implementation of a #SAT solver? I'm interested in those returning the exact solution count, not an approximation.
Tell me more
×
Theoretical Computer Science Stack Exchange is a question and answer site for
theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.
|
|
|||||||||||||||
|
|
You can do this with SAT4J, simply by iterating over all models: http://www.sat4j.org/howto.php#models. I imagine that most SAT solvers have this ability. |
|||
|
|
You can also try the #SAT solver "sharpSAT" (website, github) for counting the number of satisfying assignments of CNF formulas. |
|||||
|
|
One option is to use a BDD library, such as JavaBDD. All such libraries either have a function that counts solutions fast or, at least, they make it easy to write such a function. The disadvantage, however, is that constructing the BDD will be slow in many cases and may require much memory. In case your input is in CNF, a simple heuristic that speeds up the construction of the BDD is the following. First, build a small BDD for each clause and put them into a priority queue whose root is the smallest BDD. Second, pop two BDDs, compute AND between them and push the result to the priority queue. Here's the idea: Since computing AND between BDDs of size $m$ and $n$ takes $O(mn)$ in theory but $\sim m+n$ in practice, minimizing the runtime is the same as finding a Huffman code. |
|||
|
|
|
Related topic: Best SAT Solver. |
|||||||||
|
|
The MBound Solver given here http://www.cs.cornell.edu/~sabhar/ can give model counts with probabilistic guarantees. It's much faster than enumerating all solutions. |
|||
|
|
|
The best I found is "c2d compiler". http://reasoning.cs.ucla.edu/c2d/ It uses d-DNNF and you need the -count option. |
|||
|
|
I wrote a small model/prime implicant enumerator. This can already be used for model counting with the model enumeration but that's not very practical. If anybody's interested, I can extend it so it counts models from prime implicants. |
|||
|
|
