×

Translation among CNFs, characteristic models and ordered binary decision diagrams. (English) Zbl 1173.68719

Summary: We consider translation among Conjunctive Normal Forms (CNFs), characteristic models, and Ordered Binary Decision Diagrams (OBDDs) of Boolean functions. It is shown in this paper that Horn OBDDs can be translated into their Horn CNFs in polynomial time. As for the opposite direction, the problem can be solved in polynomial time if the ordering of variables in the resulting OBDD is specified as an input. In case that such ordering is not specified and the resulting OBDD must be of minimum size, its decision version becomes NP-complete. Similar results are also obtained for the translation in both directions between characteristic models and OBDDs. We emphasize here that the above results hold on any class of functions having a basis of polynomial size.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

ROBDD
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Angluin, D.; Frazier, M.; Pitt, L., Learning conjunctions of Horn clauses, Machine Learning, 9, 147-164 (1992) · Zbl 0766.68107
[2] Bioch, J. C.; Ibaraki, T., Complexity of identification and dualization of positive Boolean functions, Inform. and Comput., 123, 1, 50-63 (1995) · Zbl 1096.68633
[3] Brace, K. S.; Rundell, R. L.; Bryant, R. E., Efficient implementation of a BDD package, (Proc. 27th ACM/IEEE DAC (1990)), 40-45
[4] Bryant, R. E., Graph-based algorithms for Boolean function manipulation, IEEE Trans. Comput., C-35, 8, 677-691 (1986) · Zbl 0593.94022
[5] Bshouty, N. H., Exact learning Boolean functions via the monotone theory, Inform. and Comput., 123, 146-153 (1995) · Zbl 1096.68634
[6] Coudert, O., Doing two-level logic minimization 100 times faster, (Proc. 6th ACM/SIAM SODA (1995)), 112-118 · Zbl 0858.94035
[7] Eiter, T.; Gottlob, G., Identifying the minimal transversals of a hypergraph and related problems, SIAM J. Comput., 24, 6, 1278-1304 (1995) · Zbl 0842.05070
[8] Fredman, M. L.; Khachiyan, L., On the complexity of dualization of monotone disjunctive normal forms, J. Algorithms, 21, 3, 618-628 (1996) · Zbl 0864.68038
[9] Horiyama, T.; Ibaraki, T., Ordered binary decision diagrams as knowledge-bases, Artificial Intelligence, 136, 189-213 (2002) · Zbl 0995.68105
[10] Iwama, K.; Nozoe, M.; Yajima, S., Optimizing OBDDs is still intractable for monotone functions, (Proc. MFCS. Proc. MFCS, Lecture Notes in Comput. Sci., 1450 (1998), Springer: Springer Berlin), 625-635 · Zbl 1031.68539
[11] Jacobi, R.; Trullemans, A.-M., Generating prime and irredundant covers for binary decision diagrams, (Proc. EDAC’92 (March 1992)), 104-108
[12] Jain, J.; Narayan, A.; Fujita, M.; Sangiovanni-Vincentelli, A., Formal verification of combinational circuits, (Proc. VLSI Design (1997))
[13] Kautz, H. A.; Kearns, M. J.; Selman, B., Reasoning with characteristic models, (Proc. AAAI-93 (1993)), 34-39
[14] Kautz, H. A.; Kearns, M. J.; Selman, B., Horn approximations of empirical data, Artificial Intelligence, 74, 129-245 (1995) · Zbl 1014.03514
[15] Kavvadias, D.; Stavropoulos, E. G., Evaluation of an algorithm for the transversal hypergraph problem, (Proc. WAE’99. Proc. WAE’99, Lecture Notes in Comput. Sci., 1668 (1999), Springer: Springer Berlin), 72-84
[16] Khardon, R., Translating between Horn representations and their characteristic models, J. Artificial Intelligence Res., 3, 349-372 (1995) · Zbl 0900.68197
[17] Khardon, R.; Roth, D., Reasoning with models, Artificial Intelligence, 87, 187-213 (1996) · Zbl 1506.68149
[18] Minato, S., Fast generation of prime-irredundant covers from binary decision diagrams, IEICE Trans. Fundamentals, E76-A, 6, 967-973 (1993)
[19] Minato, S.; Ishiura, N.; Yajima, S., Shared binary decision diagram with attributed edges for efficient Boolean function manipulation, (Proc. 27th ACM/IEEE DAC (1990)), 52-57
[20] Tani, S.; Hamaguchi, K.; Yajima, S., The complexity of the optimal variable ordering problems of a shared binary decision diagram, IEICE Trans. Inf. Syst., E79-D, 4, 271-281 (1996)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.