{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:49Z","timestamp":1784837809700,"version":"3.55.0"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_11","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"164-183","source":"Crossref","is-referenced-by-count":16,"title":["On Tackling the Limits of Resolution in SAT Solving"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Ignatiev","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antonio","family":"Morgado","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-21581-0_7","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"I Ab\u00edo","year":"2011","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: BDDs for pseudo-boolean constraints \u2013 revisited. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 61\u201375. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21581-0_7"},{"key":"11_CR2","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.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"key":"11_CR3","unstructured":"Ans\u00f3tegui, C., Didier, F., Gab\u00e0s, J.: Exploiting the structure of unsatisfiable cores in MaxSAT. In: IJCAI, pp. 283\u2013289 (2015)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167\u2013180. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_18"},{"issue":"2","key":"11_CR5","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-30201-8_9","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"A Atserias","year":"2004","unstructured":"Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint propagation as a proof system. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 77\u201391. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30201-8_9"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"11_CR8","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). doi: 10.1007\/978-3-642-39071-5_23"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45193-8_8"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-02777-2_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"O Bailleux","year":"2009","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 181\u2013194. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_19"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: FOCS, pp. 274\u2013282 (1996)","DOI":"10.1109\/SFCS.1996.548486"},{"issue":"2\u20133","key":"11_CR12","first-page":"59","volume":"7","author":"DL Berre","year":"2010","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2\u20133), 59\u201364 (2010)","journal-title":"JSAT"},{"issue":"2\u20134","key":"11_CR13","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"11_CR14","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Balint, A., Belov, A., Heule, M., J\u00e4rvisalo, M. (eds.) Proceedings of SAT Competition 2013, vol. B-2013-1, pp. 51\u201352. Department of Computer Science Series of Publications B, University of Helsinki (2013)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Biere, A.: Lingeling essentials, a tutorial on design and implementation aspects of the SAT solver lingeling. In: Pragmatics of SAT Workshop, p. 88 (2014)","DOI":"10.29007\/jhd7"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-09284-3_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Biere","year":"2014","unstructured":"Biere, A., Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285\u2013301. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_22"},{"key":"11_CR17","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"issue":"8\u20139","key":"11_CR18","doi-asserted-by":"crossref","first-page":"606","DOI":"10.1016\/j.artint.2007.03.001","volume":"171","author":"ML Bonet","year":"2007","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: Resolution for Max-SAT. Artif. Intell. 171(8\u20139), 606\u2013618 (2007)","journal-title":"Artif. Intell."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Beatty, D., Brace, K., Cho, K., Sheffler, T.: COSMOS: a compiled simulator for MOS circuits. In: DAC, pp. 9\u201316 (1987)","DOI":"10.1145\/37888.37890"},{"issue":"4","key":"11_CR20","doi-asserted-by":"crossref","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"SR Buss","year":"1987","unstructured":"Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Log. 52(4), 916\u2013927 (1987)","journal-title":"J. Symb. Log."},{"issue":"3","key":"11_CR21","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(88)90072-2","volume":"62","author":"SR Buss","year":"1988","unstructured":"Buss, S.R., Tur\u00e1n, G.: Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci. 62(3), 311\u2013317 (1988)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"11_CR22","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1142\/S0218213001000611","volume":"10","author":"P Chatalic","year":"2001","unstructured":"Chatalic, P., Simon, L.: Multiresolution for SAT checking. Int. J. Artif. Intell. Tools 10(4), 451\u2013481 (2001)","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"4","key":"11_CR23","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. J. ACM 35(4), 759\u2013768 (1988)","journal-title":"J. ACM"},{"issue":"5","key":"11_CR24","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.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-17511-4_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Codish","year":"2010","unstructured":"Codish, M., Zazon-Ivry, M.: Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 154\u2013172. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_10"},{"issue":"4","key":"11_CR26","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"SA Cook","year":"1976","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. ACM SIGACT News 8(4), 28\u201332 (1976)","journal-title":"ACM SIGACT News"},{"issue":"1","key":"11_CR27","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"issue":"1","key":"11_CR28","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"WJ Cook","year":"1987","unstructured":"Cook, W.J., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discrete Appl. Math. 18(1), 25\u201338 (1987)","journal-title":"Discrete Appl. Math."},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-23786-7_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"J Davies","year":"2011","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225\u2013239. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23786-7_19"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-39071-5_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166\u2013181. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39071-5_13"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-40627-0_21","volume-title":"Principles and Practice of Constraint Programming","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247\u2013262. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40627-0_21"},{"issue":"3","key":"11_CR32","doi-asserted-by":"crossref","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":"11_CR33","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24605-3_37"},{"issue":"1\u20134","key":"11_CR34","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. JSAT 2(1\u20134), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"11_CR35","unstructured":"Jan Elffers\u2019 personal webpage. http:\/\/www.csc.kth.se\/~elffers"},{"key":"11_CR36","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. 4121, pp. 252\u2013265. Springer, Heidelberg (2006). doi: 10.1007\/11814948_25"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-45620-1_15","volume-title":"Automated Deduction\u2014CADE-18","author":"E Goldberg","year":"2002","unstructured":"Goldberg, E.: Testing satisfiability of CNF formulas by computing a stable set of points. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 161\u2013180. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45620-1_15"},{"issue":"1","key":"11_CR38","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/s10472-005-0420-x","volume":"43","author":"E Goldberg","year":"2005","unstructured":"Goldberg, E.: Testing satisfiability of CNF formulas by computing a stable set of points. Ann. Math. Artif. Intell. 43(1), 65\u201389 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"key":"11_CR39","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"15","key":"11_CR40","doi-asserted-by":"crossref","first-page":"1277","DOI":"10.1016\/j.artint.2010.07.008","volume":"174","author":"J Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277\u20131284 (2010)","journal-title":"Artif. Intell."},{"key":"11_CR41","unstructured":"IBM ILOG: CPLEX optimizer 12.7.0 (2016). http:\/\/www-01.ibm.com\/software\/commerce\/optimization\/cplex-optimizer"},{"key":"11_CR42","unstructured":"Ignatiev, A. Morgado, A., Marques-Silva, J.: On tackling the limits of resolution in SAT solving. CoRR, abs\/1705.01477 (2017). https:\/\/arxiv.org\/abs\/1705.01477"},{"key":"11_CR43","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-11558-0_11","volume-title":"Logics in Artificial Intelligence","author":"S Jabbour","year":"2014","unstructured":"Jabbour, S., Marques-Silva, J., Sais, L., Salhi, Y.: Enumerating prime implicants of propositional formulae in conjunctive normal form. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 152\u2013165. Springer, Cham (2014). doi: 10.1007\/978-3-319-11558-0_11"},{"key":"11_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-22438-6_26","volume-title":"Automated Deduction \u2013 CADE-23","author":"D Jovanovi\u0107","year":"2011","unstructured":"Jovanovi\u0107, D., Moura, L.: Cutting to the chase solving linear integer arithmetic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 338\u2013353. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_26"},{"issue":"1","key":"11_CR45","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovic","year":"2013","unstructured":"Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reason. 51(1), 79\u2013108 (2013)","journal-title":"J. Autom. Reason."},{"issue":"1\/2","key":"11_CR46","first-page":"95","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. JSAT 8(1\/2), 95\u2013100 (2012)","journal-title":"JSAT"},{"issue":"2\u20133","key":"11_CR47","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1016\/j.artint.2007.05.006","volume":"172","author":"J Larrosa","year":"2008","unstructured":"Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2\u20133), 204\u2013233 (2008)","journal-title":"Artif. Intell."},{"key":"11_CR48","doi-asserted-by":"crossref","unstructured":"Manquinho, V.M., Flores, P.F., Silva, J.P.M., Oliveira, A.L.: Prime implicant computation using satisfiability algorithms. In: ICTAI, pp. 232\u2013239 (1997)","DOI":"10.1109\/TAI.1997.632261"},{"key":"11_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-319-48758-8_22","volume-title":"Logics in Artificial Intelligence","author":"J Marques-Silva","year":"2016","unstructured":"Marques-Silva, J., Ignatiev, A., Menc\u00eda, C., Pe\u00f1aloza, R.: Efficient reasoning for inconsistent horn formulae. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 336\u2013352. Springer, Cham (2016). doi: 10.1007\/978-3-319-48758-8_22"},{"key":"11_CR50","unstructured":"Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR, abs\/0712.1097 (2007). https:\/\/arxiv.org\/abs\/0712.1097"},{"key":"11_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531\u2013548. Springer, Cham (2014). doi: 10.1007\/978-3-319-10428-7_39"},{"key":"11_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_33"},{"issue":"1","key":"11_CR53","doi-asserted-by":"crossref","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":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-10428-7_41","volume-title":"Principles and Practice of Constraint Programming","author":"A Morgado","year":"2014","unstructured":"Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564\u2013573. Springer, Cham (2014). doi: 10.1007\/978-3-319-10428-7_41"},{"issue":"4","key":"11_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.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478\u2013534 (2013)","journal-title":"Constraints"},{"key":"11_CR56","first-page":"129","volume":"9","author":"A Morgado","year":"2015","unstructured":"Morgado, A., Ignatiev, A., Marques-Silva, J.: MSCG: robust core-guided MaxSAT solving. JSAT 9, 129\u2013134 (2015)","journal-title":"JSAT"},{"key":"11_CR57","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":"3","key":"11_CR58","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"SIGLOG News"},{"key":"11_CR59","doi-asserted-by":"crossref","unstructured":"Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H.: Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In: ICTAI, pp. 9\u201317 (2013)","DOI":"10.1109\/ICTAI.2013.13"},{"issue":"2","key":"11_CR60","doi-asserted-by":"crossref","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. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"11_CR61","unstructured":"Previti, A. Ignatiev, A. Morgado, A., Marques-Silva, J.: Prime compilation of non-clausal formulae. In: IJCAI, pp. 1980\u20131988 (2015)"},{"key":"11_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-46011-X_8","volume-title":"Developments in Language Theory","author":"AA Razborov","year":"2002","unstructured":"Razborov, A.A.: Proof complexity of pigeonhole principles. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 100\u2013116. Springer, Heidelberg (2002). doi: 10.1007\/3-540-46011-X_8"},{"key":"11_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/11560548_19","volume-title":"Correct Hardware Design and Verification Methods","author":"J-W Roorda","year":"2005","unstructured":"Roorda, J.-W., Claessen, K.: A new SAT-based algorithm for symbolic trajectory evaluation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 238\u2013253. Springer, Heidelberg (2005). doi: 10.1007\/11560548_19"},{"key":"11_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-319-40970-2_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"P Saikko","year":"2016","unstructured":"Saikko, P., Berg, J., J\u00e4rvisalo, M.: LMHS: a SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539\u2013546. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_34"},{"issue":"4","key":"11_CR65","doi-asserted-by":"crossref","first-page":"417","DOI":"10.2178\/bsl\/1203350879","volume":"13","author":"N Segerlind","year":"2007","unstructured":"Segerlind, N.: The complexity of propositional proofs. Bul. Symb. Logic 13(4), 417\u2013481 (2007)","journal-title":"Bul. Symb. Logic"},{"key":"11_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005). doi: 10.1007\/11564751_73"},{"key":"11_CR67","doi-asserted-by":"crossref","unstructured":"Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: POS@SAT, pp. 2\u201314 (2010)","DOI":"10.29007\/g7ss"},{"key":"11_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_24"},{"issue":"1","key":"11_CR69","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (1987)","journal-title":"J. ACM"},{"issue":"2","key":"11_CR70","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63\u201369 (1998)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:59:52Z","timestamp":1750798792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}