Given a DNF of a Boolean function, this program computes the complete DNF (i.e. the DNF of all prime implicants) of the dual Boolean function.

Two other methonds for Dualization are also available. See Section USAGE.

Input file should be given in DIMACS CNF format. For details of DIMACS CNF format and benchmark problems, see SATLIB.

Execute make in an expanded directory.

$ tar zxvf dbtdd-2.1.0.tar.gz
$ cd dbtdd-2.1.0
$ make

      

Then the executable file dbtdd will be produced. For additional information, see Makefile.

Compilation will fail on some platform: Mac OSX, FreeBSD etc, because of different location of malloc.h and absence of malloc_usable_size(). This issue will be fixed in near future.

Usage:  ./dbtdd [options] input-file [output-file]
dbtdd   Version 2.1.0
Description: given a DNF of a Boolean functions in DIMACS CNF, dbtdd computes the complete DNF of the dual function.
-p  Receive implicants covering all satisfying assignments and compute all prime implicants.
-m<int> maximum usable memory for TDD uniquetable in Mbyte: place integer without space after 'm'.

If output-filename is not given, this program does not decompress a Z-TDD and does not produce any datafile.

With "-p" option, Dualization can be solved in cooperation with AllSAT Solver, as instructed below (see also Section NOTICE, because it is disabled in the default setting.).

$ allsat_solver in.cnf all.dnf
$ dbtdd -p all.dnf prime.dnf

The situation above is as follows. Suppose that in.cnf represents a DNF of a Boolean function f in DIMACS CNF format. To compute the complete DNF of the dual function of f, at first, run allsat solver with in.cnf by indentifying the DNF with the CNF of the dual function. We then obtain a DNF of all satisfying assignments to the dual function as all.dnf. To restrict them into prime ones, execute dbtdd with "-p" option. The algorithm in dbtdd with "-p" option is based on the recursive formula for prime implicants, proposed by Coudert and Madre.

To evaluate dbtdd with "-p" option, we implemented the two BDD-based methods using metaproduct encoding and polarity encoding: to use this, define USE_BDD and (METAPRODUCT_ENC or POLARITY_ENC), execute make, and run the compiled binary with "-p" option and a DNF of all satisfying assignments as instructed above.

We furthermore implemented consensus procedure, which is a well-studied prime implicant generation method (see, for details, Figure 3.1 at page 131 of "Yves Crama and Peter L. Hammer, Boolean Functions: Theory, Algorithms, and Applications, Encyclopedia of Mathematics and Its Applications 142, Cambridge, 2011").

Our implemented code is here:

Compile in the following way:

$ tar zxvf consensus-1.0.0.tar.gz
$ cd consensus-1.0.0
$ make

Our code "consensus" can be used in place of dbtdd with "-p" option:

$ allsat_solver in.cnf all.dnf
$ ./consensus all.dnf prime.dnf

To sum up, three different approaches for Dualization are provided:

Bash scripts for them, in which clasp is called as all solutions solver, are here: dualization_scripts version 1.0.0, released on 5th Aug., 2015.

A huge number of prime implicants may be generated and disk space may be exhausted. To avoid disk overflow, take measure such as using ulimit command.

Our method requires much memory in general. If the following error occurs, enlarge a maximum usable memory size by setting with "-m" option in command line (available from v2.0.0) or changing the last argument of tdd_init in dbtdd.c. Usage of this function is described in my_tdd.c.

error:my_tdd.c:210:mytdd_add_allocated_size:maximum usable memory exceeded

You can use BDD instead of DTDD. In particular, to enable "-p" option, BDD is required. To use BDD, modify Makefile by setting BDD to DDTYPE.

The performance of dbtdd is greatly affected by order of Boolean variables. Before execution of dbtdd, it is recommended to determine a good variable order by using MINCE. When executing MINCE, the following error may occur.

error while loading shared libraries: libstdc++-libc6.1-2.so.3: cannot open shared object file: No such file or directory

In that case, obtain libstdc++-libc6.1-2.so.3 from somewhere and specify its location in the following way.

$ env LD_PRELOAD=path_to_lib/libstdc++-libc6.1-2.so.3  MetaPlacerTest0.exeS -f out.aux -save -branchingFactor 1 -constTol 20 -saveXorder

If the macros MISC_LOG, TIME_LOG, SIZE_LOG, OPCACHE_LOG, and UT_LOG are defined in Makefile, the following information will be outputed to stdout. The meaning of each line is described as a comment following //.

$ ./dbtdd in.cnf out.cnf 
date  Tue May 20 20:11:01 2014  //  executed time
program dbtdd-1.1.0             //  program name and version
package My TDD Package          //  used package
input in.cnf                    //  intput file name
output  out.cnf                 //  output file name, if given in an argument.

generator_type  default         //  selected random number generator
first_value 975960880           //  the first generated random number
max_value 2147483647            //  the maximum value of random numbers
seed  1400584261                //  seed used to produce a random number

problem p cnf 192 445           //  problem line in input file
maxval  192                     //  the maximum value of items (in other words, Boolean variable index)
#clauses  445                   //  the number of clauses with repetition
#literals 999                   //  the number of literals with repetition

tdd_node  48  byte              //  the byte size of a single TDD node
ut_max_usable 4294967296  byte  //  the maximum usable memory of TDD package

dimacs_to_setfam  9384  byte    //  the memory size for the internal representation of an input data file
time(INPUT) 0.00  sec           //  the time to compress such a representation into a Z-TDD.
|ztdd|  661                     //  the number of internal nodes in a Z-TDD
#sets 445                       //  the number of sets (in other words, implicants) represented in a Z-TDD, where identical sets are not considered.
uncmp_size  999                 //  the number of literals with repetition in the DNF of all implicants

max|dtdd| 10169                 //  the maximum size of intermediate D-TDDs
time(GEN) 0.04  sec             //  the time to compute all implicants as a D-TDD from an input Z-TDD
|dtdd|  9673                    //  the number of internal nodes in a D-TDD

max|ztdd| 9609                  //  the maximum size of intermediate Z-TDDs
time(MIN) 0.12  sec             //  the time to restrict to prime implicants
|ztdd|  9609                    //  the number of internal nodes in an output Z-TDD
#sets 1908736                   //  the number of sets (in other words, prime implicants) represented in a Z-TDD
uncmp_size  363003904           //  the number of literals with repetition in the complete DNF of prime implicants

ztdd_to_dimacs  4264  byte      //  the memory size for a temporary work space to traverse a Z-TDD and output a DIMACS CNF file.
time(OUTPUT)  20.27 sec         //  the time to output a DIMACS CNF file that consists of all prime implicants
ut_average_collision  0.35      //  the measured value of average collisions in a chained-hash, which is used to maintain TDD nodes.
opcache_hit_rate  0.19          //  the measured value of the number of cache hits divided by the number of search call in operation cache.
opcache_overwrite_rate  0.00    //  the measured value of the number of times that cache entries are overwritten divided by the number of insert call in operation cache.
ut_mem_usage  2281713688        //  the memory size of a chained-hash of TDD nodes when the computation is over.

If the macro SIZE_LOG is defined, two logged data files are also outputed. See the comments described in tdd_gen.c and tdd_min.c.

We used total 99 CNF instances to measure performance of various methods, which were obtained from SATLIB, TG-Pro - A SAT-based ATPG System, and Hypergraph Dualization Repository. The complete list of used instances is this.

This software dbtdd is implemented by using CUDD library. Please check its license notice included in this software.