Abstract
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. 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.
This research was supported in part by National Science Foundation Grant CCR-9101208.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Plaisted, D., and Greenbaum, S. A structure preserving clause form translation. Journal of Symbolic Computation, 2 (1986), 293–304.
Jackson, P., and Pais, J. Computing Prime Implicants. Proceedings of the 10th International Conference on Automated Deduction, Kaiserslautern, W. Germany, July, 1990. In Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 449, 543–557.
Jackson, P. Computing prime implicants incrementally. Proceedings of the 11th International Conference on Automated Deduction, Saratoga Springs, NY, June, 1992. In Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 607, 253–267.
Kean, A., and Tsiknis, G. An incremental method for generating prime implicants/implicates. Journal of Symbolic Computation 9 (1990), 185–206.
Murray, N.V., and Rosenthal, E. Inference with path resolution and semantic graphs. JACM 34,2 (April 1987), 225–254.
Murray, N.V., and Rosenthal, E. Paul dissolution: A strongly complete rule of inference. Proceedings of the 6th National Conference on Artificial Intelligence, Seattle, WA, July 12–17, 1987, 161–166.
Murray, N.V., and Rosenthal, E. Reexamining Intractability of Analytic Tableaux. Proceedings of the 1990 International Symposium on Symbolic and Algebraic Computation, Tokyo, Japan, Aug. 20–24, 1990, 52–59.
Murray, N.V., and Rosenthal, E. Dissolution: Making paths vanish. To appear, J.ACM.
Przymusinski, T.C. An algorithm to compute circumscription. Artificial Intelligence 38 (1989), 49–73.
Ramesh, A., Becker, G., and Murray, N.V. CNF and DNF considered harmful for computing prime implicants/implicates. Technical Report TR 93-2, SUNY at Albany, 1993.
Reiter, R. and de Kleer, J. Foundations of assumption-based truth maintenance systems: preliminary report. Proceedings of the 6th National Conference on Artificial Intelligence, Seattle, WA, July 12–17, 1987, 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 algorithms for generation of prime implicants. Journal of Complexity 8 (1992), 37–63.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramesh, A., Murray, N.V. (1993). Non-clausal deductive techniques for computing prime implicants and prime implicates. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_60
Download citation
DOI: https://doi.org/10.1007/3-540-56944-8_60
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56944-2
Online ISBN: 978-3-540-47830-0
eBook Packages: Springer Book Archive