{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:08:53Z","timestamp":1748664533353,"version":"3.41.0"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243177"},{"type":"electronic","value":"9783319243184"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_30","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T05:42:56Z","timestamp":1441950176000},"page":"423-433","source":"Crossref","is-referenced-by-count":0,"title":["SAT-Based Horn Least Upper Bounds"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Menc\u00eda","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Previti","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013)"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Davies, J., Tsimpoukelli, M., Katsirelos, G.: Relaxation search: a simple way of managing optional clauses. In: AAAI, pp. 835\u2013841 (2014)","DOI":"10.1609\/aaai.v28i1.8849"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/978-3-319-09284-3_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Belov","year":"2014","unstructured":"Belov, A., Heule, M.J.H., Marques-Silva, J.: MUS extraction using clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 48\u201357. Springer, Heidelberg (2014)"},{"key":"30_CR4","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/j.artint.2014.07.011","volume":"216","author":"A Belov","year":"2014","unstructured":"Belov, A., Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing minimal equivalent subformulas. Artif. Intell. 216, 309\u2013326 (2014)","journal-title":"Artif. Intell."},{"issue":"2","key":"30_CR5","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"issue":"1","key":"30_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF02136172","volume":"18","author":"R Ben-Eliyahu","year":"1996","unstructured":"Ben-Eliyahu, R., Dechter, R.: On computing minimal models. Ann. Math. Artif. Intell. 18(1), 3\u201327 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"30_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"key":"30_CR8","unstructured":"Boufkhad, Y.: Algorithms for propositional KB approximation. In: AAAI, pp. 280\u2013285 (1998)"},{"key":"30_CR9","unstructured":"Boufkhad, Y., Gr\u00e9goire, \u00c9., Marquis, P., Mazure, B., Sais, L.: Tractable cover compilations. In: IJCAI, pp. 122\u2013127 (1997)"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173\u2013180 (2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"30_CR11","unstructured":"Cadoli, M.: Semantical and computational aspects of Horn approximations. In: IJCAI, pp. 39\u201345 (1993)"},{"issue":"3\u20134","key":"30_CR12","first-page":"137","volume":"10","author":"M Cadoli","year":"1997","unstructured":"Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun. 10(3\u20134), 137\u2013150 (1997)","journal-title":"AI Commun."},{"key":"30_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1613\/jair.664","volume":"13","author":"M Cadoli","year":"2000","unstructured":"Cadoli, M., Donini, F.M., Liberatore, P., Schaerf, M.: Space efficiency of propositional knowledge representation formalisms. J. Artif. Intell. Res. (JAIR) 13, 1\u201331 (2000)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"1\u20132","key":"30_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0004-3702(00)00010-2","volume":"119","author":"M Cadoli","year":"2000","unstructured":"Cadoli, M., Scarcello, F.: Semantical and computational aspects of Horn approximations. Artif. Intell. 119(1\u20132), 1\u201317 (2000)","journal-title":"Artif. Intell."},{"key":"30_CR15","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":"30_CR16","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"30_CR17","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) 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"30_CR18","unstructured":"del Val, A.: An analysis of approximate knowledge compilation. In: IJCAI, pp. 830\u2013836 (1995)"},{"issue":"1\u20132","key":"30_CR19","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/j.artint.2004.01.003","volume":"162","author":"A Val del","year":"2005","unstructured":"del Val, A.: First order LUB approximations: characterization and algorithms. Artif. Intell. 162(1\u20132), 7\u201348 (2005)","journal-title":"Artif. Intell."},{"issue":"3","key":"30_CR20","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"WF Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Lagniez, J.M., Mazure, B.: An experimentally efficient method for (MSS, coMSS) partitioning. In: AAAI, pp. 2666\u20132673 (2014)","DOI":"10.1609\/aaai.v28i1.9118"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I., Marques-Silva, J.: Progression in maximum satisfiability. In: ECAI, pp. 453\u2013458 (2014)","DOI":"10.3233\/978-1-61499-419-0-453"},{"issue":"2","key":"30_CR23","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0743-1066(87)90014-8","volume":"4","author":"A Itai","year":"1987","unstructured":"Itai, A., Makowsky, J.A.: Unification as a complexity measure for logic programming. J. Log. Program. 4(2), 105\u2013117 (1987)","journal-title":"J. Log. Program."},{"issue":"2","key":"30_CR24","doi-asserted-by":"crossref","first-page":"161","DOI":"10.3233\/AIC-140640","volume":"28","author":"M Janota","year":"2015","unstructured":"Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing backbones of propositional formulae. AI Commun. 28(2), 161\u2013177 (2015)","journal-title":"AI Commun."},{"key":"30_CR25","unstructured":"Junker, U.: QuickXplain: preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167\u2013172 (2004)"},{"key":"30_CR26","unstructured":"Kautz, H.A., Selman, B.: An empirical evaluation of knowledge compilation by theory approximation. In: AAAI, pp. 155\u2013161 (1994)"},{"key":"30_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-39071-5_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J-M Lagniez","year":"2013","unstructured":"Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed Up MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276\u2013292. Springer, Heidelberg (2013)"},{"key":"30_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-540-72788-0_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"M Langlois","year":"2007","unstructured":"Langlois, M., Sloan, R.H., Tur\u00e1n, G.: Horn upper bounds and renaming. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 80\u201393. Springer, Heidelberg (2007)"},{"issue":"1","key":"30_CR29","first-page":"1","volume":"7","author":"M Langlois","year":"2009","unstructured":"Langlois, M., Sloan, R.H., Tur\u00e1n, G.: Horn upper bounds and renaming. JSAT 7(1), 1\u201315 (2009)","journal-title":"JSAT"},{"key":"30_CR30","unstructured":"Marques-Silva, J., Heras, F., Janota, F., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI (2013)"},{"key":"30_CR31","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I.: Efficient autarkies. In: ECAI, pp. 603\u2013608 (2014)","DOI":"10.3233\/978-1-61499-419-0-603"},{"key":"30_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-39799-8_39","volume-title":"Computer Aided Verification","author":"J Marques-Silva","year":"2013","unstructured":"Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 592\u2013607. Springer, Heidelberg (2013)"},{"key":"30_CR33","unstructured":"Marquis, P.: Knowledge compilation using theory prime implicates. In: IJCAI, pp. 837\u2013845 (1995)"},{"key":"30_CR34","doi-asserted-by":"crossref","unstructured":"Marquis, P.: Consequence finding algorithms. In: Handbook of Defeasible Reasoning and Uncertainty Management Systems, pp. 41\u2013145 (2000)","DOI":"10.1007\/978-94-017-1737-3_3"},{"key":"30_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"R Martins","year":"2014","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver\u2019. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Heidelberg (2014)"},{"key":"30_CR36","unstructured":"Menc\u00eda, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: IJCAI, pp. 1973\u20131979 (2015)"},{"issue":"1","key":"30_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M Minoux","year":"1988","unstructured":"Minoux, M.: LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Inf. Process. Lett. 29(1), 1\u201312 (1988)","journal-title":"Inf. Process. Lett."},{"key":"30_CR38","doi-asserted-by":"crossref","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD, pp. 197\u2013200 (2013)","DOI":"10.1109\/FMCAD.2013.6679410"},{"key":"30_CR39","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI, pp. 2717\u20132723 (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"issue":"1\u20132","key":"30_CR40","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. Artif. Intell. 111(1\u20132), 41\u201372 (1999)","journal-title":"Artif. Intell."},{"key":"30_CR41","unstructured":"Previti, A., Ignatiev, A., Morgado, A., Marques-Silva, J.: Prime compilation of non-clausal formulae. In: IJCAI, pp. 1980\u20131987 (2015)"},{"issue":"1","key":"30_CR42","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"issue":"4","key":"30_CR43","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10601-010-9095-y","volume":"15","author":"ED Rosa","year":"2010","unstructured":"Rosa, E.D., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints 15(4), 485\u2013515 (2010)","journal-title":"Constraints"},{"issue":"1\u20134","key":"30_CR44","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/BF01530750","volume":"11","author":"R Rymon","year":"1994","unstructured":"Rymon, R.: An SE-tree-based prime implicant generation algorithm. Ann. Math. Artif. Intell. 11(1\u20134), 351\u2013366 (1994)","journal-title":"Ann. Math. Artif. Intell."},{"key":"30_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-540-73580-9_26","volume-title":"Abstraction, Reformulation, and Approximation","author":"P Schachte","year":"2007","unstructured":"Schachte, P., S\u00f8ndergaard, H.: Boolean approximation revisited. In: Miguel, I., Ruml, W. (eds.) SARA 2007. LNCS (LNAI), vol. 4612, pp. 329\u2013343. Springer, Heidelberg (2007)"},{"issue":"9\u201310","key":"30_CR46","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1016\/j.artint.2010.03.003","volume":"174","author":"P Schachte","year":"2010","unstructured":"Schachte, P., S\u00f8ndergaard, H., Whiting, L., Henshall, K.: Information loss in knowledge compilation: A comparison of boolean envelopes. Artif. Intell. 174(9\u201310), 585\u2013596 (2010)","journal-title":"Artif. Intell."},{"key":"30_CR47","unstructured":"Schrag, R.: Compilation for critically constrained knowledge bases. In: AAAI, pp. 510\u2013515 (1996)"},{"key":"30_CR48","unstructured":"Selman, B., Kautz, H.A.: Knowledge compilation using Horn approximations. In: AAAI, pp. 904\u2013909 (1991)"},{"issue":"2","key":"30_CR49","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/226643.226644","volume":"43","author":"B Selman","year":"1996","unstructured":"Selman, B., Kautz, H.A.: Knowledge compilation and theory approximation. J. ACM 43(2), 193\u2013224 (1996)","journal-title":"J. ACM"},{"key":"30_CR50","unstructured":"Simon, L., del Val, A.: Efficient consequence finding. In: IJCAI, pp. 359\u2013370 (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:26:48Z","timestamp":1748618808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}