CNF2OBDD or BDD_MINISAT_ALL

Takahisa Toda

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



Last update: 2019-03-01

Table of Contents

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

Description

A CNF to OBDD compiler or a formula-BDD caching AllSAT solver, implemented on top of MiniSat-C v1.14.1, is presented. This software has two names because of a double meaning. It may be called cnf2obdd to put more emphasis on a CNF to OBDD compiler aspect, which supports rich operations for postprocessing, and it also may be called bdd_minisat_all on an AllSAT solver aspect, which simply generates all solutions, a familiar format to wider users.

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 formula 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 bdd_minisat_all-1.0.0.tar.gz
$ cd bdd_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.

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 you want to use refresh option, define REFRESH in Makefile. 


Usage:  ./bdd_minisat_all [options] input-file [output-file]
-n<int> maximum number of obdd nodes: if exceeded, obdd is refreshed

Since variable orderings significantly affect solver's performance, we recommend that users in advance execute the software MINCE to determine a good variable ordering.

MACRO

Program behavior can be controlled by defining or not defining the following macros in Makefile.
  • CUTSETCACHE: Cutset is selected as formula-BDD caching. If this is not defined, separator is selected.
  • LAZY: Cache operations are reduced (Recommended).
Select one of the two base solver types: a blocking solver or a non-blocking solver.
  • NONBLOCKING non-blocking procedure is selected as a base solver. If this is not defined, blocking procedure is selected. For options of non-blocking solvers, see nbc_minisat_all.
  • REFRESH: refresh option in command line is enabled. If the number of BDD nodes exceeds a specified threshold, all solutions are dumpted to a file (if output file is specified in command line), all caches are refreshed, and search is continued.
Other options are as follows.
  • TRIE_RECURSION: Recursive version of trie is used. If this is not defined, iterative version is used.
  • REDUCTION: Reduction of compiled OBDD into fully reduced one is performed using CUDD library (Optional). To do this, obtain CUDD library and modify Makefile.
  • GMP: GNU MP bignum library is used to count solutions. To do this, obtain GMP library and modify Makefile.

LICENSE

bdd_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. Moreover, bdd_minisat_all requires much memory. In case of memory shortage, the solver halts with the following error message. 


error:"file name":"line number":"function name":memory allocation failed

In this case, define the REFRESH macro in Makefile, compile the code again, execute with -n option.

REFERENCES