CNF and DNF Considered Harmful for Computing Prime Implicants/Implicates
Tóm tắt
Several methods to compute the prime implicants and the prime implicates of a negation normal form (NNF) formula are developed and implemented. An algorithm PI is introduced that is an extension to negation normal form of an algorithm given by Jackson and Pais. A correctness proof of the PI algorithm is given. The PI algorithm alone is sufficient in a computational sense. However, it can be combined with path dissolution, and it is shown empirically that this is often an advantage. None of these variations rely on conjunctive normal form or on disjunctive normal form. A class of formulas is described for which reliance on CNF or on DNF results in an exponential increase in the time required to compute prime implicants/implicates. The possibility of avoiding this problem with efficient structure preserving clause form translations is examined briefly and appears unfavorable.
Tài liệu tham khảo
Jackson, P. and Pais, J.: Computing prime implicants, Proceedings of the 10th International Conference on Automated Deductions, Kaiserslautern, Germany, 1990, in Lecture Notes in Artificial Intelligence, Vol. 449, Springer-Verlag, 1990, pp. 543–557.
Jackson, P.: Computing prime implicants incrementally, Proceedings of the 11th International Conference on Automated Deduction, Saratoga Springs, NY, 1992, in Lecture Notes in Artificial Intelligence, Vol. 607, Springer-Verlag, 1992, pp. 253–267.
Kean, A. and Tsiknis, G.: An incremental method for generating prime implicants/implicates, J. Symbolic Computation 9(1990), 185–206.
Murray, N. V. and Rosenthal, E.: Inference with path resolution and semantic graphs, J. ACM 34(2) (1987), 225–254.
Murray, N. V. and Rosenthal, E.: Path dissolution: A strongly complete rule of inference, in Proceedings of the 6th National Conference on Artificial Intelligence, Seattle, WA, July 12–17, 1987, pp. 161–166.
Murray, N. V. and Rosenthal, E.: Reexamining intractability of analytic tableaux, in Proceedings of the 1990 International Symposium on Symbolic and Algebraic Computation, Tokyo, Japan, 1990, pp. 52–59.
Murray, N. V. and Rosenthal, E.: Dissolution: Making paths vanish, J. ACM 40(3) (1993), 504–535.
Nelson, R. J.: Simplest normal truth functions, J. Symbolic Logic 20(1995), 105–108.
Plaisted, D. and Greenbaum, S.: A structure preserving clause form translation, J. Symbolic Computation 2(1986), 293–304.
Przymusinski, T. C.: An algorithm to compute circumscription, Artificial Intelligence 38(1989), 49–73.
Reiter, R. and de Kleer, J.: Foundations of assumption-based truth maintenance systems: preliminary report, in Proceedings of the 6th National Conference on Artificial Intelligence, Seattle, WA, 1987, pp. 183–188.
Slagle, J. R., Chang, C. L. and Lee, R. C. T.: A new algorithm for generating prime implicants, IEEE transactions on Computers C-19(4) (1970), 304–310.
Strzemecki, T.: Polynomial-time algorithm for generation of prime implicants, J. Complexity 8(1992), 37–63.