Table of Contents
Given a Boolean formula in CNF, ALLSAT is the problem of generating all satisfying assignments for the CNF formula.
The three types of AllSAT solvers are available.
A blocking clause-based AllSAT solver (see bc_minisat_all).
A chronological backtracking-based AllSAT solver (see nbc_minisat_all).
A BDD-based ALLSAT solver, which also can be seen as a CNF to OBDD compiler, (see bdd_minisat_all or cnf2obdd).
Sample input files, computed output files, and log files are here.
We surveyed major techniques of AllSAT solvers and conducted comprehensive experiments, which is published as an open access paper here in ACM Journal of Experimental Algorithmics.
Boolean formulae should be given in DIMACS CNF format. For details of DIMACS CNF format, see DIMACS Challenge - Satisfiability: Suggested Format. Many benchmarks are available from the following websites.
Other solvers with the support of solution generation:
clasp: A conflict-driven nogood learning answer set solver, developed as a part of Potassco project.
PicoSAT, developed by Armin Biere, Johannes Kepler University.
relsat: A propositional satisfiability solver and model counter, developed by Roberto J. Bayardo.
#SAT solvers and knowledge compilers are closely related to AllSAT solvers and they are gathered with lots of useful information and benchmarks in Beyond NP: Keeping up with solvers that reach beyond NP!.