{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T21:06:48Z","timestamp":1772831208652,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319115573","type":"print"},{"value":"9783319115580","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11558-0_11","type":"book-chapter","created":{"date-parts":[[2014,9,16]],"date-time":"2014-09-16T02:22:39Z","timestamp":1410834159000},"page":"152-165","source":"Crossref","is-referenced-by-count":12,"title":["Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form"],"prefix":"10.1007","author":[{"given":"Said","family":"Jabbour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lakhdar","family":"Sais","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yakoub","family":"Salhi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"19","key":"11_CR1","doi-asserted-by":"publisher","first-page":"2474","DOI":"10.1093\/bioinformatics\/bts423","volume":"28","author":"V. Acu\u00f1a","year":"2012","unstructured":"Acu\u00f1a, 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\u00a028(19), 2474\u20132483 (2012)","journal-title":"Bioinformatics"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-72788-0_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"G. Audemard","year":"2007","unstructured":"Audemard, G., Sa\u00efs, L.: Circuit based encoding of CNF formula. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 16\u201321. Springer, Heidelberg (2007)"},{"key":"11_CR3","unstructured":"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\u2013127 (1997)"},{"issue":"3-4","key":"11_CR4","first-page":"137","volume":"10","author":"M. Cadoli","year":"1997","unstructured":"Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun.\u00a010(3-4), 137\u2013150 (1997)","journal-title":"AI Commun."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Castell, T.: Computation of prime implicates and prime implicants by a variant of the Davis and Putnam procedure. In: ICTAI, pp. 428\u2013429 (1996)","DOI":"10.1109\/TAI.1996.560739"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Coudert, O., Madre, J.: Fault tree analysis: 1020 prime implicants and beyond. In: Reliability and Maintainability Symposium, pp. 240\u2013245 (January 1993)","DOI":"10.1109\/RAMS.1993.296849"},{"key":"11_CR7","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A. Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. (JAIR)\u00a017, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"11_CR8","unstructured":"de Kleer, J., Mackworth, A.K., Reiter, R.: Characterizing diagnoses. In: Proceedings of the 8th National Conference on Artificial Intelligence (AAAI 1990), pp. 324\u2013330 (1990)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Fontaine, P., Berre, D.L., Mazure, B.: Computing prime implicants. In: FMCAD, pp. 46\u201352 (2013)","DOI":"10.1109\/FMCAD.2013.6679390"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013561 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"},{"issue":"2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0951-8320(97)00034-3","volume":"58","author":"Y. Dutuit","year":"1997","unstructured":"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\u00a058(2), 127\u2013144 (1997)","journal-title":"Reliability Engineering and System Safety"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"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\u201342 (2007)","DOI":"10.1109\/VLSID.2007.81"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-50701-9_22","volume-title":"Non-Monotonic Reasoning","author":"M. Ginsberg","year":"1988","unstructured":"Ginsberg, M.: A circumscriptive theorem prover. In: Reinfrank, M., Ginsberg, M.L., de Kleer, J., Sandewall, E. (eds.) Non-Monotonic Reasoning 1988. LNCS, vol.\u00a0346, pp. 100\u2013114. Springer, Heidelberg (1988)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/11527695_10","volume-title":"Theory and Applications of Satisfiability Testing","author":"\u00c9. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, \u00c9., Ostrowski, R., Mazure, B., Sa\u00efs, L.: Automatic extraction of functional dependencies. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 122\u2013132. Springer, Heidelberg (2005)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Gurvich, V., Khachiyan, L.: On generating the irredundant conjunctive and disjunctive normal forms of monotone boolean functions. Discrete Applied Mathematics 96-97(1), 363\u2013373 (1999)","DOI":"10.1016\/S0166-218X(99)00099-2"},{"issue":"2-4","key":"11_CR17","first-page":"239","volume":"4","author":"F. Heras","year":"2008","unstructured":"Heras, F., Larrosa, J., de Givry, S., Schiex, T.: 2006 and 2007 Max-SAT evaluations: Contributed instances. JSAT\u00a04(2-4), 239\u2013250 (2008)","journal-title":"JSAT"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"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\u2013239 (1997)","DOI":"10.1109\/TAI.1997.632261"},{"key":"11_CR20","unstructured":"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)"},{"key":"11_CR21","unstructured":"Marques-Silva, J.: On computing minimum size prime implicants. In: International Workshop on Logic Synthesis (1997)"},{"key":"11_CR22","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI (2013)"},{"issue":"6","key":"11_CR23","doi-asserted-by":"publisher","first-page":"1417","DOI":"10.1002\/j.1538-7305.1956.tb03835.x","volume":"35","author":"E.J. McCluskey Jr.","year":"1956","unstructured":"McCluskey Jr., E.J.: Minimization of boolean functions. Bell System Technical Journal\u00a035(6), 1417\u20131444 (1956)","journal-title":"Bell System Technical Journal"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-39611-3_13","volume-title":"Hardware and Software: Verification and Testing","author":"A. Morgado","year":"2013","unstructured":"Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol.\u00a07857, pp. 86\u2013101. Springer, Heidelberg (2013)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-46135-3_13","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"R. Ostrowski","year":"2002","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sa\u00efs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 185\u2013199. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0004-3702(99)00035-1","volume":"111","author":"L. Palopoli","year":"1999","unstructured":"Palopoli, L., Pirri, F., Pizzuti, C.: Algorithms for selective enumeration of prime implicants. Artificial Intelligence\u00a0111(1-2), 41\u201372 (1999)","journal-title":"Artificial Intelligence"},{"key":"11_CR27","first-page":"332","volume-title":"Proceedings of the 8th International Conference on Tools with Artificial Intelligence, ICTAI","author":"C. Pizzuti","year":"1996","unstructured":"Pizzuti, C.: Computing prime implicants by integer programming. In: Proceedings of the 8th International Conference on Tools with Artificial Intelligence, ICTAI, pp. 332\u2013336. IEEE Computer Society, Washington, DC (1996)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Quine, W.: On cores and prime implicants of truth functions. American Mathematical Monthly, 755\u2013760 (1959)","DOI":"10.1080\/00029890.1959.11989404"},{"issue":"8","key":"11_CR29","doi-asserted-by":"publisher","first-page":"521","DOI":"10.2307\/2308219","volume":"59","author":"W.V. Quine","year":"1952","unstructured":"Quine, W.V.: The problem of simplifying truth functions. The American Mathematical Monthly\u00a059(8), 521\u2013531 (1952)","journal-title":"The American Mathematical Monthly"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"11_CR31","unstructured":"Roy, J.A., Markov, I.L., Bertacco, V.: Restoring circuit structure from SAT instances. In: IWLS, Temecula Creek, CA, pp. 361\u2013368 (June 2004)"},{"key":"11_CR32","unstructured":"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\u2013515 (1996)"},{"key":"11_CR33","unstructured":"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)"},{"issue":"4","key":"11_CR34","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1109\/PGEC.1967.264648","volume":"16","author":"P. Tison","year":"1967","unstructured":"Tison, P.: Generalized consensus theory and applications to the minimization of boolean circuits. IEEE Transactions on Computers\u00a016(4), 446\u2013456 (1967)","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"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\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11558-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:54:53Z","timestamp":1746377693000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-11558-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319115573","9783319115580"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11558-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}