SAT solvers for counting the number of solutions

Are there existing SAT solver libraries that can count the number of solutions of a boolean formula? Can you give examples?

I mean implementations more efficient than the naive approach, i.e. each time a solution is found, a new clause is added to prevent it to be found again.

• – D.W.
Feb 15 at 22:23

Yes, they are known as #SAT solvers. Some of them are exact, some of them are approximate.

Some of them are based on a version of DPLL that exhaustively find every solution in a factorized way. Some of them, known as bottom up, are based on transforming the input CNF to Boolean circuits for which we know how to find the number of satisfying assignment and which can be inductively built from the clauses (with an exponential worst case obviously). Some of them are approximate and roughly work by trying to halve the space of satisfying assignments by cutting it with a hyperplane until they are no more than $$k$$ solutions and return $$2^\ell k$$ where $$\ell$$ is the number of times the space was divided.

Here is a non exhaustive list. See also the model counting competition of the SAT conference.

DPLL based:

Bottom up:

Approximate:

• Thank you. I was thinking about using these to prove this conjecture for n >= 7. I probably don't have enough knowledge and time to do it, but just out of curiosity could somebody submit just a problem (a benchmark?) to the model counting competition, without competing with a solver? Feb 15 at 20:02
• There is a call for benchmarks at the model counting competition mccompetition.org/2024/cfb2024. However you will have to encode it as a CNF formula first. The organizers would be very happy to receive benchmarks even (and may especially) if the author does not compete!
– holf
Feb 16 at 6:10