{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:15Z","timestamp":1763468115542},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642335570"},{"type":"electronic","value":"9783642335587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33558-7_14","type":"book-chapter","created":{"date-parts":[[2012,10,3]],"date-time":"2012-10-03T02:32:47Z","timestamp":1349231567000},"page":"158-174","source":"Crossref","is-referenced-by-count":9,"title":["On Computing Minimal Equivalent Subformulas"],"prefix":"10.1007","author":[{"given":"Anton","family":"Belov","sequence":"first","affiliation":[]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A. Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res.\u00a040, 353\u2013373 (2011)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"14_CR2","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1137\/0215029","volume":"15","author":"G. Ausiello","year":"1986","unstructured":"Ausiello, G., D\u2019Atri, A., Sacc\u00e0, D.: Minimal representation of directed hypergraphs. SIAM J. Comput.\u00a015(2), 418\u2013431 (1986)","journal-title":"SIAM J. Comput."},{"key":"14_CR3","unstructured":"Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI, pp. 276\u2013281 (1993)"},{"key":"14_CR4","unstructured":"Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: FMCAD, pp. 37\u201340 (2011)"},{"key":"14_CR5","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation\u00a04, 75\u201397 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"14_CR6","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"14_CR7","unstructured":"Boufkhad, Y., Roussel, O.: Redundancy in random SAT formulas. In: AAAI, pp. 273\u2013278 (2000)"},{"issue":"2","key":"14_CR8","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J.W. Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS Journal on Computing\u00a03(2), 157\u2013168 (1991)","journal-title":"INFORMS Journal on Computing"},{"key":"14_CR9","unstructured":"Chmeiss, A., Krawczyk, V., Sais, L.: Redundancy in CSPs. In: ECAI, pp. 907\u2013908 (2008)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Choi, C.W., Lee, J.H.-M., Stuckey, P.J.: Removing propagation redundant constraints in redundant modeling. ACM Trans. Comput. Log. 8(4) (2007)","DOI":"10.1145\/1276920.1276925"},{"key":"14_CR11","unstructured":"de Siqueira, N.J.L., Puget, J.-F.: Explanation-based generalisation of failures. In: ECAI, pp. 339\u2013344 (1988)"},{"key":"14_CR12","unstructured":"Dechter, A., Dechter, R.: Removing redundancies in constraint networks. In: AAAI, pp. 105\u2013109 (1987)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"issue":"2","key":"14_CR14","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10878-008-9142-4","volume":"18","author":"C. Desrosiers","year":"2009","unstructured":"Desrosiers, C., Galinier, P., Hertz, A., Paroz, S.: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J. Comb. Optim.\u00a018(2), 124\u2013150 (2009)","journal-title":"J. Comb. Optim."},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-72397-4_6","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"O. Fourdrinoy","year":"2007","unstructured":"Fourdrinoy, O., Gr\u00e9goire, \u00c9., Mazure, B., Sa\u00efs, L.: Eliminating Redundant Clauses in SAT Instances. In: Van Hentenryck, P., Wolsey, L.A. (eds.) CPAIOR 2007. LNCS, vol.\u00a04510, pp. 71\u201383. Springer, Heidelberg (2007)"},{"key":"14_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-73580-9_23","volume-title":"Abstraction, Reformulation, and Approximation","author":"S.M. Gonz\u00e1lez","year":"2007","unstructured":"Gonz\u00e1lez, S.M., Meseguer, P.: Boosting MUS Extraction. In: Miguel, I., Ruml, W. (eds.) SARA 2007. LNCS (LNAI), vol.\u00a04612, pp. 285\u2013299. Springer, Heidelberg (2007)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-74970-7_24","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"\u00c9. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: MUST: Provide a Finer-Grained Explanation of Unsatisfiability. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 317\u2013331. Springer, Heidelberg (2007)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: ICTAI, pp. 74\u201383 (November 2008)","DOI":"10.1109\/ICTAI.2008.39"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-21034-1_18","volume-title":"The Semantic Web: Research and Applications","author":"S. Grimm","year":"2011","unstructured":"Grimm, S., Wissmann, J.: Elimination of Redundancy in Ontologies. In: Antoniou, G., Grobelnik, M., Simperl, E., Parsia, B., Plexousakis, D., De Leenheer, P., Pan, J. (eds.) ESWC 2011, Part I. LNCS, vol.\u00a06643, pp. 260\u2013274. Springer, Heidelberg (2011)"},{"issue":"1","key":"14_CR20","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0004-3702(93)90062-G","volume":"64","author":"P.L. Hammer","year":"1993","unstructured":"Hammer, P.L., Kogan, A.: Optimal compression of propositional horn knowledge bases: Complexity and approximation. Artif. Intell.\u00a064(1), 131\u2013145 (1993)","journal-title":"Artif. Intell."},{"key":"14_CR21","unstructured":"Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: ECAI, pp. 113\u2013117 (2006)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing Rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"14_CR23","unstructured":"Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167\u2013172 (2004)"},{"issue":"1","key":"14_CR24","doi-asserted-by":"crossref","first-page":"83","DOI":"10.3233\/FI-2011-429","volume":"109","author":"O. Kullmann","year":"2011","unstructured":"Kullmann, O.: Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure. Fundam. Inform.\u00a0109(1), 83\u2013119 (2011)","journal-title":"Fundam. Inform."},{"issue":"2","key":"14_CR25","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.artint.2004.11.002","volume":"163","author":"P. Liberatore","year":"2005","unstructured":"Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell.\u00a0163(2), 203\u2013232 (2005)","journal-title":"Artif. Intell."},{"issue":"1","key":"14_CR26","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":"14_CR27","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: ISMVL, pp. 9\u201314 (2010)","DOI":"10.1109\/ISMVL.2010.11"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"J. Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Lynce, I.: On Improving MUS Extraction Algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 159\u2013173. Springer, Heidelberg (2011)"},{"key":"14_CR29","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD, pp. 121\u2013128 (October 2010)"},{"issue":"5","key":"14_CR30","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1016\/j.ijar.2010.01.011","volume":"51","author":"M. Niepert","year":"2010","unstructured":"Niepert, M., Gucht, D.V., Gyssens, M.: Logical and algorithmic properties of stable conditional independence. Int. J. Approx. Reasoning\u00a051(5), 531\u2013543 (2010)","journal-title":"Int. J. Approx. Reasoning"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Piette, C.: Let the solver deal with redundancy. In: ICTAI, pp. 67\u201373 (2008)","DOI":"10.1109\/ICTAI.2008.38"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-04222-5_21","volume-title":"Frontiers of Combining Systems","author":"C. Piette","year":"2009","unstructured":"Piette, C., Hamadi, Y., Sa\u00efs, L.: Efficient Combination of Decision Procedures for MUS Computation. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 335\u2013349. Springer, Heidelberg (2009)"},{"issue":"2","key":"14_CR33","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K. Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell.\u00a0175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"issue":"3","key":"14_CR34","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-00768-2_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Scholl","year":"2009","unstructured":"Scholl, C., Disch, S., Pigorsch, F., Kupferschmid, S.: Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 383\u2013397. Springer, Heidelberg (2009)"},{"key":"14_CR36","doi-asserted-by":"crossref","unstructured":"To, S.T., Son, T.C., Pontelli, E.: On the use of prime implicates in conformant planning. In: AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7757"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"To, S.T., Son, T.C., Pontelli, E.: Conjunctive representations in contingent planning: Prime implicates versus minimal CNF formula. In: AAAI (2011)","DOI":"10.1609\/aaai.v25i1.8015"},{"key":"14_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-79719-7_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"H. Maaren van","year":"2008","unstructured":"van Maaren, H., Wieringa, S.: Finding Guaranteed MUSes\u00a0Fast. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 291\u2013304. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33558-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T01:43:29Z","timestamp":1687743809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33558-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642335570","9783642335587"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33558-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}