BC_MINISAT_ALL: A Blocking AllSAT Solver

Takahisa Toda

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


        
        

Last update: 2015-9-30


Table of Contents

Description
DOWNLOAD
FILE FORMAT
HOW TO COMPILE
MACRO
USAGE
LICENSE
NOTICE
REFERENCES

My website is moved to http://www.disc.lab.uec.ac.jp/toda/index-en.html .

Description

A blocking clause-based AllSAT solver (a blocking solver for short), implemented on top of MiniSat-C v1.14.1, is presented.

DOWNLOAD

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.

FILE FORMAT

Boolean formulae should be in DIMACS CNF format. For details of DIMACS CNF format and benchmark problems, see SATLIB.

HOW TO COMPILE

If no option is given, standard mode is selected.


$ tar zxvf bc_minisat_all-1.0.0.tar.gz
$ cd bc_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.

      

MACRO

Program behavior can be controlled by defining or not defining the following macros in Makefile.
  • SIMPLIFY: Simplification of assignments is enabled. If this is not defined, simplification is not performed, and blocking clauses consisting of decision literals are used instead.
  • NONDISJOINT: Nondisjoint partial assignments are computed (see Yu et al. 2014). If this is not defined, computed partial assignments are pairwise disjoint: in other words, different partial assignments do not share common total assignments. This macro makes sense only when SIMPLIFICATION is defined too.
  • CONTINUE: Search is continued at the point where a solutions is found. If this is not defined, solver starts from scratch.
  • FIXEDORDER: Variable selection heuristic is disabled and variables are selected in increasing order of variable indices. If this is not defined, variable selection heuristic is used. This functionality is added to evaluate efficiency of variable selection heuristics.
  • GMP: GNU MP bignum library is used to count solutions.

USAGE

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. If simplification is performed, computed assingments are partial, which means some variables may not appear.


Usage:  ./bc_minisat_all [options] input-file [output-file]

    

LICENSE

bc_minisat_all is implemented by modifying MiniSat-C_v1.14.1. Please confirm the license file included in this software.

NOTICE

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.

REFERENCES