{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:22:38Z","timestamp":1748406158092,"version":"3.41.0"},"reference-count":74,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,5,24]],"date-time":"2015-05-24T00:00:00Z","timestamp":1432425600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10601-015-9195-9","type":"journal-article","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T08:09:46Z","timestamp":1432368586000},"page":"277-302","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Quantified maximum satisfiability"],"prefix":"10.1007","volume":"21","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","published-online":{"date-parts":[[2015,5,24]]},"reference":[{"key":"9195_CR1","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., & Sakallah, K.A. (2006). Refinement strategies for verification methods based on datapath abstraction. In ASP-DAC (pp. 19\u201324). doi: 10.1145\/1118299.1118306 .","DOI":"10.1145\/1118299.1118306"},{"key":"9195_CR2","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., & Sakallah, K.A. (2008). Reveal: a formal verification tool for verilog designs. In LPAR (pp. 343\u2013352). doi: 10.1007\/978-3-540-89439-1_25 .","DOI":"10.1007\/978-3-540-89439-1_25"},{"key":"9195_CR3","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., & Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In SAT (pp. 427\u2013440).","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"9195_CR4","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., & Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In AAAI.","DOI":"10.1609\/aaai.v24i1.7545"},{"key":"9195_CR5","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3tegui","year":"2013","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., & Levy, J. (2013). SAT-based MaxSAT algorithms. Artificial Intelligence, 196, 77\u2013105.","journal-title":"Artificial Intelligence"},{"key":"9195_CR6","unstructured":"Ansotegui, C., Gomes, C.P., & Selman, B. (2005). The Achilles\u2019 heel of QBF. In AAAI (pp. 275\u2013281)."},{"key":"9195_CR7","doi-asserted-by":"crossref","unstructured":"Bailey, J., & Stuckey, P.J. (2005). Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In PADL (pp. 174\u2013186).","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"9195_CR8","doi-asserted-by":"crossref","unstructured":"Balabanov, V., & Jiang, J.H.R. (2011). Resolution proofs and Skolem functions in QBF evaluation and applications. In G. Gopalakrishnan, S. Qadeer (Eds.), CAV (pp. 149\u2013164).","DOI":"10.1007\/978-3-642-22110-1_12"},{"issue":"1","key":"9195_CR9","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., & Jiang, J.H.R. (2012). Unified QBF certification and its applications. Formal Methods in System Design, 41(1), 45\u201365.","journal-title":"Formal Methods in System Design"},{"key":"9195_CR10","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Widl, M., & Jiang, J.H.R. (2014). QBF resolution systems and their proof complexities. In C. Sinz, U. Egly (Eds.), SAT (pp. 154\u2013169). Springer.","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"9195_CR11","doi-asserted-by":"crossref","unstructured":"Belov, A., Janota, M., Lynce, I., & Marques-Silva, J. (2012). On computing minimal equivalent subformulas. In M. Milano (Ed.), CP (Vol. 7514, pp. 158\u2013174). Springer.","DOI":"10.1007\/978-3-642-33558-7_14"},{"key":"9195_CR12","doi-asserted-by":"crossref","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. (2014). Algorithms for computing minimal equivalent subformulas. Artificial Intelligence, 216, 309\u2013326. doi: 10.1016\/j.artint.2014.07.011 .","journal-title":"Artificial Intelligence"},{"issue":"2","key":"9195_CR13","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. (2012). Towards efficient MUS extraction. AI Communication, 25(2), 97\u2013116.","journal-title":"AI Communication"},{"key":"9195_CR14","doi-asserted-by":"crossref","unstructured":"Belov, A., Morgado, A., & Marques-Silva, J. (2013). SAT-based preprocessing for MaxSAT. In LPAR (pp. 96\u2013111). doi: 10.1007\/978-3-642-45221-5_7 .","DOI":"10.1007\/978-3-642-45221-5_7"},{"key":"9195_CR15","doi-asserted-by":"crossref","unstructured":"Benedetti, M., Lallouet, A., & Vautard, J. (2008). Quantified constraint optimization. In CP (pp. 463\u2013477).","DOI":"10.1007\/978-3-540-85958-1_31"},{"issue":"2-3","key":"9195_CR16","first-page":"59","volume":"7","author":"DL Berre","year":"2010","unstructured":"Berre, D.L., & Parrain, A. (2010). The Sat4j library, release 2.2. JSAT, 7(2-3), 59\u20136.","journal-title":"JSAT"},{"issue":"1","key":"9195_CR17","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1080\/0952813021000026795","volume":"15","author":"E Birnbaum","year":"2003","unstructured":"Birnbaum, E., & Lozinskii, E.L. (2003). Consistent subsets of inconsistent systems: structure and behaviour. Journal of Experimental & Theoretical Artificial Intelligence, 15(1), 25\u201346.","journal-title":"Journal of Experimental & Theoretical Artificial Intelligence"},{"key":"9195_CR18","unstructured":"Chen, H., Janota, M., & Marques-Silva, J. (2012). QBF-based Boolean function bi-decomposition. In DATE (pp. 816\u2013819)."},{"key":"9195_CR19","doi-asserted-by":"crossref","unstructured":"Chen, H., & P\u00e1l, M. (2004). Optimization, games, and quantified constraint satisfaction. In Mathematical foundations of computer science (pp. 239\u2013250).","DOI":"10.1007\/978-3-540-28629-5_16"},{"issue":"5","key":"9195_CR20","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2003). Counterexample-guided abstraction refinement for symbolic model checking. Journal of ACM, 50(5), 752\u2013794.","journal-title":"Journal of ACM"},{"key":"9195_CR21","doi-asserted-by":"crossref","unstructured":"Condon, A., Feigenbaum, J., Lund, C., & Shor, P.W. (1995). Probabilistically checkable debate systems and nonapproximability of PSPACE-hard functions. Chicago Journal of Theoretical Computer Science, 1995.","DOI":"10.4086\/cjtcs.1995.004"},{"key":"9195_CR22","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2003). An extensible SAT-solver. In SAT (pp. 502\u2013518)."},{"key":"9195_CR23","doi-asserted-by":"crossref","unstructured":"Egly, U., Lonsing, F., & Widl, M. (2013). Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In K. L. McMillan, A. Middeldorp, A. Voronkov (Eds.), LPAR (Vol. 8312, pp. 291\u2013308). Springer.","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"9195_CR24","doi-asserted-by":"crossref","unstructured":"Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In A. Biere, C. P. Gomes (Eds.), SAT, lecture notes in computer science (Vol. 4121, pp. 252\u2013265). Springer.","DOI":"10.1007\/11814948_25"},{"key":"9195_CR25","doi-asserted-by":"crossref","unstructured":"Goldberg, E.I., & Novikov, Y. (2003). Verification of proofs of unsatisfiability for CNF formulas. In DATE (pp. 10,886\u201310,891). IEEE Computer Society.","DOI":"10.1109\/DATE.2003.1253718"},{"key":"9195_CR26","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., & Bacchus, F. (2010). Exploiting QBF duality on a circuit representation. AAAI.","DOI":"10.1609\/aaai.v24i1.7548"},{"key":"9195_CR27","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., & Bacchus, F. (2013). Recovering and utilizing partial duality in QBF. In SAT (pp. 83\u201399). doi: 10.1007\/978-3-642-39071-5_8 .","DOI":"10.1007\/978-3-642-39071-5_8"},{"key":"9195_CR28","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Seidl, M., & Biere, A. (2013). Bridging the gap between dual propagation and CNF-based QBF solving. In DATE (pp. 811\u2013814).","DOI":"10.7873\/DATE.2013.172"},{"key":"9195_CR29","unstructured":"Gupta, A. (2006). Learning abstractions for model checking, Ph.D. thesis, Carnegie Mellon University."},{"issue":"2","key":"9195_CR30","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1109\/3477.752801","volume":"29","author":"B Han","year":"1999","unstructured":"Han, B., & Lee, S.J. (1999). Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics: Part B, 29(2), 281\u2013286.","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics: Part B"},{"key":"9195_CR31","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., & Marques-Silva, J. (2011). Core-guided binary search algorithms for maximum satisfiability. In W. Burgard, D. Roth (Eds.), AAAI. AAAI Press.","DOI":"10.1609\/aaai.v25i1.7822"},{"key":"9195_CR32","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., & Biere, A. (2014). A unified proof system for QBF preprocessing. In S. Demri, D. Kapur, C. Weidenbach (Eds.), IJCAR (Vol. 8562, pp. 91\u2013106).","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"9195_CR33","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Janota, M., & Marques-Silva, J. (2013). Quantified maximum satisfiability: A core-guided approach. In M. J\u00e4rvisalo, A. Van Gelder (Eds.), SAT (Vol. 7962, pp. 250\u2013266). Springer.","DOI":"10.1007\/978-3-642-39071-5_19"},{"key":"9195_CR34","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I., & Marques-Silva, J. (2014). Progression in maximum satisfiability. In ECAI (pp. 453\u2013458). doi: 10.3233\/978-1-61499-419-0-453 .","DOI":"10.3233\/978-1-61499-419-0-453"},{"key":"9195_CR35","doi-asserted-by":"crossref","unstructured":"Jain, H., Kroening, D., Sharygina, N., & Clarke, E.M. (2005). Word level predicate abstraction and refinement for verifying RTL verilog. In DAC (pp. 445\u2013450). doi: 10.1145\/1065579.1065697 .","DOI":"10.1145\/1065579.1065697"},{"key":"9195_CR36","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., & Marques-Silva, J. (2013). On QBF proofs and preprocessing. In K.L. McMillan, A. Middeldorp, A. Voronkov (Eds.), LPAR (Vol. 8312, pp. 473\u2013489). Springer.","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"9195_CR37","doi-asserted-by":"crossref","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., & Clarke, E.M. (2012). Solving QBF with counterexample guided refinement. In A. Cimatti, R. Sebastiani (Eds.), SAT (Vol. 7317, pp. 114\u2013128). Springer.","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"9195_CR38","doi-asserted-by":"crossref","unstructured":"Janota, M., & Marques-Silva, J. (2011). Abstraction-based algorithm for 2QBF. In SAT (pp. 230\u2013244).","DOI":"10.1007\/978-3-642-21581-0_19"},{"key":"9195_CR39","unstructured":"Kleine B\u00fcning, H., & Bubeck, U. (2009). Theory of quantified Boolean formulas. In A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of satisfiability, frontiers in artificial intelligence and applications (Vol. 185, pp. 735\u2013760). IOS Press."},{"issue":"1","key":"9195_CR40","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., & Fl\u00f6gel, A. (1995). Resolution for quantified Boolean formulas. Information and Computation, 117(1), 12\u201318.","journal-title":"Information and Computation"},{"issue":"1","key":"9195_CR41","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10817-007-9067-0","volume":"39","author":"H Kleine B\u00fcning","year":"2007","unstructured":"Kleine B\u00fcning, H., Subramani, K., & Zhao, X. (2007). Boolean functions as models for quantified Boolean formulas. Journal of Automated Reasoning, 39(1), 49\u201375.","journal-title":"Journal of Automated Reasoning"},{"key":"9195_CR42","doi-asserted-by":"crossref","unstructured":"Klieber, W., Sapra, S., Gao, S., & Clarke, E.M. (2010). A non-prenex, non-clausal QBF solver with game-state learning. In SAT (pp. 128\u2013142). doi: 10.1007\/978-3-642-14186-7_12 .","DOI":"10.1007\/978-3-642-14186-7_12"},{"issue":"1","key":"9195_CR43","doi-asserted-by":"crossref","first-page":"83","DOI":"10.3233\/FI-2011-429","volume":"109","author":"O Kullmann","year":"2011","unstructured":"Kullmann, O. (2011). Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure. Fundamental and Information, 109(1), 83\u2013119.","journal-title":"Fundamental and Information"},{"issue":"2","key":"9195_CR44","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/j.artint.2004.11.002","volume":"163","author":"P Liberatore","year":"2005","unstructured":"Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artificial Intelligence, 163(2), 203\u2013232.","journal-title":"Artificial Intelligence"},{"issue":"4","key":"9195_CR45","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/s10601-008-9058-8","volume":"14","author":"MH Liffiton","year":"2009","unstructured":"Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., & Sakallah, K.A. (2009). A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints, 14(4), 415\u2013442.","journal-title":"Constraints"},{"key":"9195_CR46","doi-asserted-by":"crossref","unstructured":"Liffiton, M.H., & Sakallah, K.A. (2005). On finding all minimally unsatisfiable subformulas. In SAT (pp. 173\u2013186).","DOI":"10.1007\/11499107_13"},{"issue":"1","key":"9195_CR47","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., & Sakallah, K.A. (2008). Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal of Automated Reasoning, 40(1), 1\u201333.","journal-title":"Journal of Automated Reasoning"},{"key":"9195_CR48","doi-asserted-by":"crossref","unstructured":"Lonsing, F., & Egly, U. (2014). Incremental QBF solving. In CP (pp. 514\u2013530).","DOI":"10.1007\/978-3-319-10428-7_38"},{"key":"9195_CR49","unstructured":"Lynce, I., & Marques-Silva, J.P. (2004). On computing minimum unsatisfiable cores. In SAT."},{"key":"9195_CR50","doi-asserted-by":"crossref","unstructured":"Manquinho, V.M., Marques-Silva, J., & Planes, J. (2009). Algorithms for weighted Boolean optimization. In SAT (pp. 495\u2013508).","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"9195_CR51","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J. (2010). Minimal unsatisfiability: models, algorithms and applications (invited paper). In ISMVL (pp. 9\u201314). IEEE Computer Society.","DOI":"10.1109\/ISMVL.2010.11"},{"key":"9195_CR52","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., & Belov, A. (2013). On computing minimal correction subsets. In IJCAI."},{"key":"9195_CR53","doi-asserted-by":"crossref","unstructured":"Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J.P., & Sakallah, K.A. (2005). A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In SAT (pp. 467\u2013474).","DOI":"10.1007\/11499107_40"},{"key":"9195_CR54","doi-asserted-by":"crossref","unstructured":"Morgado, A., Dodaro, C., & Marques-Silva, J. (2014). Core-guided MaxSAT with soft cardinality constraints. In CP (pp. 564\u2013573). doi: 10.1007\/978-3-319-10428-7_41 .","DOI":"10.1007\/978-3-319-10428-7_41"},{"issue":"4","key":"9195_CR55","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M.H., Planes, J., & Marques-Silva, J. (2013). Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints, 18 (4), 478\u2013534.","journal-title":"Constraints"},{"key":"9195_CR56","doi-asserted-by":"crossref","unstructured":"Narodytska, N., & Bacchus, F. (2014). Maximum satisfiability using core-guided MaxSAT resolution. In AAAI (pp. 2717\u20132723).","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"9195_CR57","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., & Biere, A. (2012). Resolution-based certificate extraction for QBF - (tool presentation). In A. Cimatti, R. Sebastiani (Eds.), SAT (Vol. 7317, pp. 430\u2013435). Springer."},{"key":"9195_CR58","doi-asserted-by":"crossref","unstructured":"N\u00f6hrer, A., Biere, A., & Egyed, A. (2012). Managing SAT inconsistencies with HUMUS. In VAMOS (pp. 83\u201391).","DOI":"10.1145\/2110147.2110157"},{"issue":"3","key":"9195_CR59","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., & Greenbaum, S. (1986). A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3), 293\u2013304. doi: 10.1016\/S0747-7171(86)80028-1 .","journal-title":"Journal of Symbolic Computation"},{"key":"9195_CR60","unstructured":"Reimer, S., Sauer, M., Marin, P., & Becker, B. (2014). QBF with soft variables. ECEASST 70."},{"issue":"1","key":"9195_CR61","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57\u201395.","journal-title":"Artificial Intelligence"},{"key":"9195_CR62","unstructured":"Roussel, O., & Manquinho, V. (2009). Pseudo-Boolean and cardinality constraints. In A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of satisfiability, frontiers in artificial intelligence and applications (Vol. 185, pp. 695\u2013733). IOS Press."},{"key":"9195_CR63","doi-asserted-by":"crossref","unstructured":"Ryvchin, V., & Strichman, O. (2011). Faster extraction of high-level minimal unsatisfiable cores. In SAT (pp. 174\u2013187).","DOI":"10.1007\/978-3-642-21581-0_15"},{"issue":"3","key":"9195_CR64","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/582475.582484","volume":"33","author":"M Schaefer","year":"2002","unstructured":"Schaefer, M., & Umans, C. (2002). Completeness in the polynomial-time hierarchy: a compendium. SIGACT News, 33(3), 32\u201349.","journal-title":"SIGACT News"},{"issue":"1","key":"9195_CR65","first-page":"75","volume":"17","author":"C Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., & K\u00fcchlin, W. (2003). Formal methods for the validation of automotive product configuration data. AI EDAM, 17(1), 75\u201397.","journal-title":"AI EDAM"},{"key":"9195_CR66","doi-asserted-by":"crossref","unstructured":"Stuckey, P.J. (2013). There are no CNF problems. In SAT (pp. 19\u201321). doi: 10.1007\/978-3-642-39071-5_3 .","DOI":"10.1007\/978-3-642-39071-5_3"},{"key":"9195_CR67","doi-asserted-by":"crossref","unstructured":"Stuckey, P.J., Sulzmann, M., & Wazny, J. (2003). Interactive type debugging in Haskell. In ACM SIGPLAN workshop on Haskell (pp. 72\u201383). ACM.","DOI":"10.1145\/871895.871903"},{"key":"9195_CR68","unstructured":"Tseitin, G.S. (1968). On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115\u2013125."},{"key":"9195_CR69","doi-asserted-by":"crossref","unstructured":"Van Gelder, A. (2012). Contributions to the theory of practical quantified Boolean formula solving. In M. Milano (Ed.), CP (Vol. 7514, pp. 647\u2013663). Springer.","DOI":"10.1007\/978-3-642-33558-7_47"},{"key":"9195_CR70","doi-asserted-by":"crossref","unstructured":"Yu, Y., & Malik, S. (2005). Validating the result of a quantified Boolean formula (QBF) solver: theory and practice. In ASP-DAC (pp. 1047\u20131051).","DOI":"10.1145\/1120725.1120821"},{"key":"9195_CR71","doi-asserted-by":"crossref","unstructured":"Zhang, J., Li, S., & Shen, S. (2006). Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In AUS-AI (pp. 847\u2013856).","DOI":"10.1007\/11941439_89"},{"key":"9195_CR72","unstructured":"Zhang, L. (2006). Solving QBF by combining conjunctive and disjunctive normal forms. In AAAI (pp. 143\u2013150)."},{"key":"9195_CR73","doi-asserted-by":"crossref","unstructured":"Zhang, L., & Malik, S. (2002). Conflict driven learning in a quantified Boolean satisfiability solver. In ICCAD (pp. 442\u2013449).","DOI":"10.1145\/774572.774637"},{"key":"9195_CR74","unstructured":"Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In DATE (pp. 10,880\u201310,885). IEEE Computer Society."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9195-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-015-9195-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9195-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T02:43:12Z","timestamp":1748400192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-015-9195-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,24]]},"references-count":74,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["9195"],"URL":"https:\/\/doi.org\/10.1007\/s10601-015-9195-9","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2015,5,24]]}}}