2
$\begingroup$

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.

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
3
$\begingroup$

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:

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Fabius Wiesner
    Commented Feb 15 at 20:02
  • 1
    $\begingroup$ 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! $\endgroup$
    – holf
    Commented Feb 16 at 6:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.