All Solutions SAT Repository

Takahisa Toda

The University of Electro-Communications
Graduate School of Informatics and Engineering
Associate Professor

Last update: 2019-03-01


Table of Contents

PROBLEM DEFINITION
DOWNLOAD
SURVEY AND EXPERIMENTS
BENCHMARKS
LINKS

PROBLEM DEFINITION

Given a Boolean formula in CNF, ALLSAT is the problem of generating all satisfying assignments for the CNF formula.

DOWNLOAD

The three types of AllSAT solvers are available.

Sample input files, computed output files, and log files are here.

SURVEY AND EXPERIMENTS

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.

BENCHMARKS

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.

LINKS

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