All Solutions SAT Repository

Takahisa Toda

Back to Top Page.

Last update: 2015-9-30


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.

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