{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T04:43:06Z","timestamp":1789879386262,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642237850","type":"print"},{"value":"9783642237867","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23786-7_32","type":"book-chapter","created":{"date-parts":[[2011,8,31]],"date-time":"2011-08-31T03:58:42Z","timestamp":1314763122000},"page":"414-428","source":"Crossref","is-referenced-by-count":9,"title":["On Deciding MUS Membership with QBF"],"prefix":"10.1007","author":[{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"Cadoli, M., Lenzerini, M.: The complexity of closed world reasoning and circumscription. In: AAAI Conference on Artificial Intelligence, pp. 550\u2013555 (1990)"},{"issue":"2","key":"32_CR2","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."},{"issue":"2","key":"32_CR3","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(93)90073-3","volume":"114","author":"T. Eiter","year":"1993","unstructured":"Eiter, T., Gottlob, G.: Propositional circumscription and extended closed-world reasoning are $\\Pi^P_2$ -complete. Theor. Comput. Sci.\u00a0114(2), 231\u2013245 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"32_CR4","unstructured":"Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate quantified Boolean formulae. In: AAAI\/IAAI, pp. 285\u2013290 (2000)"},{"key":"32_CR5","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: An effective preprocessor for QBF pre-reasoning. In: 2nd International Workshop on Quantification in Constraint Programming, QiCP (2008)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: International Conference on Tools with Artificial Intelligence, pp. 74\u201383 (November 2008)","DOI":"10.1109\/ICTAI.2008.39"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-02959-2_7","volume-title":"Automated Deduction \u2013 CADE-22","author":"E. Gr\u00e9goire","year":"2009","unstructured":"Gr\u00e9goire, E., Mazure, B., Piette, C.: Does this set of clauses overlap with at least one MUS? In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 100\u2013115. Springer, Heidelberg (2009)"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: Counterexample guided abstraction refinement algorithm for propositional circumscription. In: Proceeding of the 12th European Conference on Logics in Artificial Intelligence, JELIA (2010)","DOI":"10.1007\/978-3-642-15675-5_18"},{"key":"32_CR9","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, Simon (eds.) [23]"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-20895-9_30","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: cmMUS: a circumscription-based tool for MUS membership testing. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol.\u00a06645, pp. 266\u2013271. Springer, Heidelberg (2011)"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: An application of matroid theory to the SAT problem. In: IEEE Conference on Computational Complexity, pp. 116\u2013124 (2000)","DOI":"10.1109\/CCC.2000.856741"},{"key":"32_CR12","unstructured":"Kullmann, O.: Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability. ECCC 14(055) (2007)"},{"issue":"2","key":"32_CR13","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":"32_CR14","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":"32_CR15","unstructured":"Lifschitz, V.: Some results on circumscription. In: NMR, pp. 151\u2013164 (1984)"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, Simon (eds.) [23]","DOI":"10.1007\/978-3-642-21581-0_14"},{"issue":"1-2","key":"32_CR17","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J. McCarthy","year":"1980","unstructured":"McCarthy, J.: Circumscription - a form of non-monotonic reasoning. Artif. Intell.\u00a013(1-2), 27\u201339 (1980)","journal-title":"Artif. Intell."},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: Switching and Automata Theory (1972)","DOI":"10.1109\/SWAT.1972.29"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Minker, J.: On indefinite databases and the closed world assumption. In: Conference on Automated Deduction, pp. 292\u2013308 (1982)","DOI":"10.1007\/BFb0000066"},{"key":"32_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/11564751_34","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"B. O\u2019Callaghan","year":"2005","unstructured":"O\u2019Callaghan, B., O\u2019Sullivan, B., Freuder, E.C.: Generating corrective explanations for interactive constraint satisfaction. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 445\u2013459. Springer, Heidelberg (2005)"},{"issue":"1","key":"32_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","volume":"37","author":"C.H. Papadimitriou","year":"1988","unstructured":"Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci.\u00a037(1), 2\u201313 (1988)","journal-title":"J. Comput. Syst. Sci."},{"key":"32_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-85958-1_29","volume-title":"Principles and Practice of Constraint Programming","author":"A. Papadopoulos","year":"2008","unstructured":"Papadopoulos, A., O\u2019Sullivan, B.: Relaxations for compiled over-constrained problems. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol.\u00a05202, pp. 433\u2013447. Springer, Heidelberg (2008)"},{"key":"32_CR23","volume-title":"The 14th International Conference on Theory and Applications of Satisfiability Testing (SAT)","year":"2011","unstructured":"Sakallah, K.A., Simon, L. (eds.): The 14th International Conference on Theory and Applications of Satisfiability Testing (SAT). Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2013 CP 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23786-7_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T12:37:08Z","timestamp":1560515828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23786-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237850","9783642237867"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23786-7_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}