Abstract
In this paper, a new approach for enumerating the set prime implicants (PI) of a Boolean formula in conjunctive normal form (CNF) is proposed. It is based on an encoding of the input formula as a new one whose models correspond to the set of prime implicants of the original theory. This first PI enumeration approach is then enhanced by an original use of the boolean functions or gates usually involved in many CNF instances encoding real-world problems. Experimental evaluation on several classes of CNF instances shows the feasibility of our proposed framework.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Acuña, V., Milreu, P.V., Cottret, L., Marchetti-Spaccamela, A., Stougie, L., Sagot, M.-F.: Algorithms and complexity of enumerating minimal precursor sets in genome-wide metabolic networks. Bioinformatics 28(19), 2474–2483 (2012)
Audemard, G., Saïs, L.: Circuit based encoding of CNF formula. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 16–21. Springer, Heidelberg (2007)
Boufkhad, Y., Gregoire, E., Marquis, P., Sais, L.: Tractable cover compilations. In: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 122–127 (1997)
Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun. 10(3-4), 137–150 (1997)
Castell, T.: Computation of prime implicates and prime implicants by a variant of the Davis and Putnam procedure. In: ICTAI, pp. 428–429 (1996)
Coudert, O., Madre, J.: Fault tree analysis: 1020 prime implicants and beyond. In: Reliability and Maintainability Symposium, pp. 240–245 (January 1993)
Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. (JAIR) 17, 229–264 (2002)
de Kleer, J., Mackworth, A.K., Reiter, R.: Characterizing diagnoses. In: Proceedings of the 8th National Conference on Artificial Intelligence (AAAI 1990), pp. 324–330 (1990)
Déharbe, D., Fontaine, P., Berre, D.L., Mazure, B.: Computing prime implicants. In: FMCAD, pp. 46–52 (2013)
del Val, A.: Tractable databases: How to make propositional unit resolution complete through compilation. In: Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR 1994), Bonn, Germany, May 24-27, pp. 551–561 (1994)
Dutuit, Y., Rauzy, A.: Exact and truncated computations of prime implicants of coherent and non-coherent fault trees within Aralia. Reliability Engineering and System Safety 58(2), 127–144 (1997)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: 20th International Conference on VLSI Design (VLSI Design 2007), Sixth International Conference on Embedded Systems (ICES 2007), Bangalore, India, January 6-10, pp. 37–42 (2007)
Ginsberg, M.: A circumscriptive theorem prover. In: Reinfrank, M., Ginsberg, M.L., de Kleer, J., Sandewall, E. (eds.) Non-Monotonic Reasoning 1988. LNCS, vol. 346, pp. 100–114. Springer, Heidelberg (1988)
Grégoire, É., Ostrowski, R., Mazure, B., Saïs, L.: Automatic extraction of functional dependencies. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 122–132. Springer, Heidelberg (2005)
Gurvich, V., Khachiyan, L.: On generating the irredundant conjunctive and disjunctive normal forms of monotone boolean functions. Discrete Applied Mathematics 96-97(1), 363–373 (1999)
Heras, F., Larrosa, J., de Givry, S., Schiex, T.: 2006 and 2007 Max-SAT evaluations: Contributed instances. JSAT 4(2-4), 239–250 (2008)
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008)
Manquinho, V.M., Flores, P., Marques-Silva, J., Oliveira, A.L.: Prime implicant computation using satisfiability algorithms. In: Proc. of the IEEE International Conference on Tools with Artificial Intelligence, pp. 232–239 (1997)
Manquinho, V.M., Oliveira, A.L., Marques-Silva, J.: Models and algorithms for computing minimum-size prime implicants. In: Proc. International Workshop on Boolean Problems, IWBP 1998 (1998)
Marques-Silva, J.: On computing minimum size prime implicants. In: International Workshop on Logic Synthesis (1997)
Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI (2013)
McCluskey Jr., E.J.: Minimization of boolean functions. Bell System Technical Journal 35(6), 1417–1444 (1956)
Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 86–101. Springer, Heidelberg (2013)
Ostrowski, R., Grégoire, É., Mazure, B., Saïs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 185–199. Springer, Heidelberg (2002)
Palopoli, L., Pirri, F., Pizzuti, C.: Algorithms for selective enumeration of prime implicants. Artificial Intelligence 111(1-2), 41–72 (1999)
Pizzuti, C.: Computing prime implicants by integer programming. In: Proceedings of the 8th International Conference on Tools with Artificial Intelligence, ICTAI, pp. 332–336. IEEE Computer Society, Washington, DC (1996)
Quine, W.: On cores and prime implicants of truth functions. American Mathematical Monthly, 755–760 (1959)
Quine, W.V.: The problem of simplifying truth functions. The American Mathematical Monthly 59(8), 521–531 (1952)
Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 31–45. Springer, Heidelberg (2004)
Roy, J.A., Markov, I.L., Bertacco, V.: Restoring circuit structure from SAT instances. In: IWLS, Temecula Creek, CA, pp. 361–368 (June 2004)
Schrag, R.: Compilation for critically constrained knowledge bases. In: Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference (AAAI 1996), pp. 510–515 (1996)
Slavkovik, M., Agotnes, T.: A judgment set similarity measure based on prime implicants. In: Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2014 (to appear, 2014)
Tison, P.: Generalized consensus theory and applications to the minimization of boolean circuits. IEEE Transactions on Computers 16(4), 446–456 (1967)
Tseitin, G.: On the complexity of derivations in the propositional calculus. In: Slesenko, H. (ed.) Structures in Constructives Mathematics and Mathematical Logic, Part II, pp. 115–125 (1968)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Jabbour, S., Marques-Silva, J., Sais, L., Salhi, Y. (2014). Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form. In: Fermé, E., Leite, J. (eds) Logics in Artificial Intelligence. JELIA 2014. Lecture Notes in Computer Science(), vol 8761. Springer, Cham. https://doi.org/10.1007/978-3-319-11558-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-11558-0_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11557-3
Online ISBN: 978-3-319-11558-0
eBook Packages: Computer ScienceComputer Science (R0)