{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:00Z","timestamp":1760061660086,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642390708"},{"type":"electronic","value":"9783642390715"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_19","type":"book-chapter","created":{"date-parts":[[2013,6,24]],"date-time":"2013-06-24T01:23:17Z","timestamp":1372036997000},"page":"250-266","source":"Crossref","is-referenced-by-count":8,"title":["Quantified Maximum Satisfiability:"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Ignatiev","sequence":"first","affiliation":[]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-02777-2_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"C. Ans\u00f3tegui","year":"2009","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 427\u2013440. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: A new algorithm for weighted partial MaxSAT. In: AAAI Conference on Artificial Intelligence. AAAI (2010)","key":"19_CR2","DOI":"10.1609\/aaai.v24i1.7545"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"Practical Aspects of Declarative Languages","author":"J. Bailey","year":"2005","unstructured":"Bailey, J., Stuckey, P.J.: Discovery of Minimal Unsatisfiable Subsets of Constraints Using Hitting Set Dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol.\u00a03350, pp. 174\u2013186. Springer, Heidelberg (2005)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-22110-1_12","volume-title":"Computer Aided Verification","author":"V. Balabanov","year":"2011","unstructured":"Balabanov, V., Jiang, J.H.R.: Resolution proofs and skolem functions in QBF evaluation and applications. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 149\u2013164. Springer, Heidelberg (2011)"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V. Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.H.R.: Unified qbf certification and its applications. Formal Methods in System Design\u00a041(1), 45\u201365 (2012)","journal-title":"Formal Methods in System Design"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02591796","volume":"30","author":"E. Balas","year":"1984","unstructured":"Balas, E., Mazzola, J.: Nonlinear 0\u20131 programming: I. Linearization techniques. Mathematical Programming\u00a030, 1\u201321 (1984), http:\/\/dx.doi.org\/10.1007\/BF02591796 , 10.1007, doi:10.1007\/BF02591796","journal-title":"Mathematical Programming"},{"issue":"2","key":"19_CR7","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.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-540-85958-1_31","volume-title":"Principles and Practice of Constraint Programming","author":"M. Benedetti","year":"2008","unstructured":"Benedetti, M., Lallouet, A., Vautard, J.: Quantified constraint optimization. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol.\u00a05202, pp. 463\u2013477. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"19_CR9","first-page":"59","volume":"7","author":"D.L. Berre","year":"2010","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT\u00a07(2-3), 59\u201364 (2010)","journal-title":"JSAT"},{"issue":"1","key":"19_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1080\/0952813021000026795","volume":"15","author":"E. Birnbaum","year":"2003","unstructured":"Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell.\u00a015(1), 25\u201346 (2003)","journal-title":"J. Exp. Theor. Artif. Intell."},{"unstructured":"B\u00fcning, H.K., Bubeck, U.: Theory of quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 735\u2013760. IOS Press (2009)","key":"19_CR11"},{"issue":"1","key":"19_CR12","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10817-007-9067-0","volume":"39","author":"H.K. B\u00fcning","year":"2007","unstructured":"B\u00fcning, H.K., Subramani, K., Zhao, X.: Boolean Functions as Models for Quantified Boolean Formulas. J. Autom. Reasoning\u00a039(1), 49\u201375 (2007)","journal-title":"J. Autom. Reasoning"},{"unstructured":"Chen, H., Janota, M., Marques-Silva, J.: QBF-based Boolean function bi-decomposition. In: Design, Automation & Test in Europe Conference, pp. 816\u2013819 (2012)","key":"19_CR13"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-28629-5_16","volume-title":"Mathematical Foundations of Computer Science 2004","author":"H. Chen","year":"2004","unstructured":"Chen, H., P\u00e1l, M.: Optimization, games, and quantified constraint satisfaction. In: Fiala, J., Koubek, V., Kratochv\u00edl, J. (eds.) MFCS 2004. LNCS, vol.\u00a03153, pp. 239\u2013250. Springer, Heidelberg (2004)"},{"issue":"5","key":"19_CR15","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"unstructured":"Condon, A., Feigenbaum, J., Lund, C., Shor, P.W.: Probabilistically checkable debate systems and nonapproximability of PSPACE-hard functions. Chicago J. Theor. Comput. Sci. (1995)","key":"19_CR16"},{"key":"19_CR17","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":"19_CR18","first-page":"17","volume":"4","author":"R. Fortet","year":"1960","unstructured":"Fortet, R.: Applications de l\u2019alg\u00e8bre de Boole en recherche op\u00e9rationnelle. Revue Fran\u00e7aise d\u2019Informatique et de Recherche Op\u00e9rationnelle\u00a04, 17\u201326 (1960)","journal-title":"Revue Fran\u00e7aise d\u2019Informatique et de Recherche Op\u00e9rationnelle"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z. Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"unstructured":"Gupta, A.: Learning Abstractions for Model Checking. Ph.D. thesis, Carnegie Mellon University (June 2006)","key":"19_CR20"},{"doi-asserted-by":"crossref","unstructured":"Hammer, P., Rudeanu, S.: Boolean Methods in Operations Research and Related Areas. Springer (1968)","key":"19_CR21","DOI":"10.1007\/978-3-642-85823-9"},{"issue":"2","key":"19_CR22","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1109\/3477.752801","volume":"29","author":"B. Han","year":"1999","unstructured":"Han, B., Lee, S.J.: Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics, Part B\u00a029(2), 281\u2013286 (1999)","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part B"},{"doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search for maximum satisfiability. In: AAAI Conference on Artificial Intelligence. AAAI (2011)","key":"19_CR23","DOI":"10.1007\/978-3-642-31612-8_22"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M. Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"issue":"4","key":"19_CR26","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s10601-008-9058-8","volume":"14","author":"M.H. Liffiton","year":"2009","unstructured":"Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., Sakallah, K.A.: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints\u00a014(4), 415\u2013442 (2009)","journal-title":"Constraints"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11499107_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.H. Liffiton","year":"2005","unstructured":"Liffiton, M.H., Sakallah, K.A.: On Finding All Minimally Unsatisfiable Subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 173\u2013186. Springer, Heidelberg (2005)"},{"issue":"1","key":"19_CR28","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"},{"unstructured":"Lynce, I., Marques-Silva, J.P.: On Computing Minimum Unsatisfiable Cores. In: SAT (2004)","key":"19_CR29"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-02777-2_45","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"V. Manquinho","year":"2009","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 495\u2013508. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications (invited paper). In: ISMVL, pp. 9\u201314. IEEE Computer Society (2010)","key":"19_CR31","DOI":"10.1109\/ISMVL.2010.11"},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/11499107_40","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Mneimneh","year":"2005","unstructured":"Mneimneh, M., Lynce, I., Andraus, Z., Marques-Silva, J., Sakallah, K.: A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 467\u2013474. Springer, Heidelberg (2005)"},{"key":"19_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-Based Certificate Extraction for QBF - (Tool Presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 430\u2013435. Springer, Heidelberg (2012)"},{"issue":"1","key":"19_CR34","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.\u00a032(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"issue":"3","key":"19_CR35","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/582475.582484","volume":"33","author":"M. Schaefer","year":"2002","unstructured":"Schaefer, M., Umans, C.: Completeness in the polynomial-time hierarchy: a compendium. SIGACT News\u00a033(3), 32\u201349 (2002)","journal-title":"SIGACT News"},{"issue":"1","key":"19_CR36","first-page":"75","volume":"17","author":"C. Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., K\u00fcchlin, W.: Formal methods for the validation of automotive product configuration data. AI EDAM\u00a017(1), 75\u201397 (2003)","journal-title":"AI EDAM"},{"doi-asserted-by":"crossref","unstructured":"Yu, Y., Malik, S.: Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice. In: Asia and South Pacific Design Automation Conference, pp. 1047\u20131051 (2005)","key":"19_CR37","DOI":"10.1145\/1120725.1120821"},{"doi-asserted-by":"crossref","unstructured":"Zhang, J., Li, S., Shen, S.: Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In: Australian Conference on Artificial Intelligence, pp. 847\u2013856 (2006)","key":"19_CR38","DOI":"10.1007\/11941439_89"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,2]],"date-time":"2023-07-02T14:45:19Z","timestamp":1688309119000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}