My website is moved to http://www.disc.lab.uec.ac.jp/toda/index-en.html .
An AllSAT solver without blocking clause mechanism (a non-blocking solver for short), implemented on top of MiniSat-C v1.14.1, is presented.
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 in DIMACS CNF format. For details of DIMACS CNF format and benchmark problems, see SATLIB.
If no option is given, standard mode is selected.
$ tar zxvf nbc_minisat_all-1.0.0.tar.gz $ cd nbc_minisat_all-1.0.0 $ make [options] list of options s standard: debug information used by debugger is generated at compilation time, and detailed solver status is reported at runtime. p profile: in addition to standard setting, profile information used by gprof is generated at compilation time and several tests are performed at runtime. d debug: in addition to standard setting, several tests are performed at runtime and no optimization is applied. r release: release version, compiled with dynamic link rs static: release version, compiled with static link clean executable files, object files, etc are removed.
Select at most one of the following backtrack methods in conflict resolution stage: if none of them is selected, the combination of BJ and CBJ is selected.
If an output file is specified, all satisfying assignments to a CNF are generated in DIMACS CNF format without problem line. Notice: there may be as many number of assignments as can not be stored in a disk space.
Usage: ./nbc_minisat_all [options] input-file [output-file]
A huge number of assignments may be generated and disk space may be exhausted. To avoid disk overflow, take measure such as using ulimit command.
nbc_minisat_all is implemented by modifying MiniSat-C_v1.14.1. Please confirm the license file included in this software.