Last update: 2016-06-20

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.

- Latest version: dbtdd version 2.1.0, released on 20th Jun., 2016.
- Old versions: v1.1.0, v1.0.0, v2.0.0

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:

- Latest version: consensus version 1.0.0, released on 5th Aug., 2015.

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:

- dbtdd without "-p" option,
- combination of allsat solver and dbtdd with "-p" option (three implementations based on tdd, bdd+metaproduct, bdd+polarity),
- combination of allsat solver and consensus procedure.

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.

- T.Toda, Dualization of Boolean functions Using Ternary Decision Diagrams, in Proc. of 13th International Symposium on Artificial Intelligence and Mathematics (ISAIM2014), Florida, USA(2014).
- T.Toda, Fast Compression of Large-scale Hypergraphs for Solving Combinatorial Problems, in Proc. of Sixteenth International Conference on Discovery Science (DS2013), LNAI 8140, pp. 281--293, Singapore (2013).
- Crama, Y., and Hammer, P.: Boolean Functions: Theory, Algorithms, and Applications. Encyclopedia of Mathematics and its Applications. Cambridge University Press (2011).
- Bryant, R.E.: Graph-Based algorithm for Boolean function manipulation, IEEE Trans. Comput., Vol.35, pp.677-691 (1986)
- Minato, S.: Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems, 30th ACM/IEEE Design Automation Conference (DAC-93), Dallas, Texas, USA, June, pp.272-277 (1993)
- Knuth, D.E.: The Art of Computer Programming Volume 4a, Addison-Wesley Professional, New Jersey, USA (2011)
- T. Sasao, Ternary decision diagrams survey. In Proceedings of IEEE 27th International Symposium on Multiple-Valued Logic (ISMVL ’97), 241–250 (1997).
- K. Yasuoka, A new method to represent sets of products: ternary decision diagrams. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science E78-A:1722–1728 (1995).
- T.Toda, Hypergraph Transversal Computation with Binary Decision Diagrams, in Proc. of 12th International Symposium on Experimental Algorithms (SEA2013), LNCS 7933, pp.91-102, Rome, Italy (2013).
- Eiter, T., Makino, K., Gottlob, G.: Computational aspects of monotone dualization: A brief survey. Discrete Applied Mathematics 156 (2008) 2035–2049
- Eiter, T., Gottlob, G.: Hypergraph transversal computation and related problems in logic and AI. LNAI 2424 (2002) 549–564
- Coudert, O. and Madre: Implicit and incremental computation of primes and essential primes of Boolean functions, In Proc. of 29th ACM/IEEE Design Automation Conference, 1992.