Table of Contents
My website is moved to http://www.disc.lab.uec.ac.jp/toda/index-en.html .
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
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.
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
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:
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
Usage of this function is described in
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
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.