{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T21:56:29Z","timestamp":1769723789098,"version":"3.49.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030802226","type":"print"},{"value":"9783030802233","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_33","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"488-498","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Proof Builder for Max-SAT"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Py","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed Sami","family":"Cherif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Djamal","family":"Habet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"33_CR1","doi-asserted-by":"publisher","first-page":"89","DOI":"10.3233\/SAT190104","volume":"9","author":"A Abram\u00e9","year":"2015","unstructured":"Abram\u00e9, A., Habet, D.: Ahmaxsat: description and evaluation of a branch and bound max-SAT solver. J. Satisfiability Boolean Model. Comput. 9, 89\u2013128 (2015)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Alexey Ignatiev, A.M., Marques-Silva, J.: RC2: an efficient maxsat solver. J. Satisfiability Boolean Model. Comput. 11(1), 53\u201364 (2019)","DOI":"10.3233\/SAT190116"},{"key":"33_CR3","unstructured":"Andres, B., Kaufmann, B., Matheis, O., Schaub, T.: Unsatisfiability-based optimization in clasp. In: Technical Communications of The Twenty-eighth International Conference on Logic Programming (ICLP 2012) 17 (01 2012)"},{"key":"33_CR4","unstructured":"Bacchus, F., J\u00e4rvisalo, M., Martins, R.: MaxSAT Evaluation (2020). https:\/\/maxsat-evaluations.github.io\/2020\/"},{"key":"33_CR5","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s00493-004-0036-5","volume":"24","author":"E Ben-sasson","year":"2004","unstructured":"Ben-sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of tree-like and general resolution. Combinatorica 24, 585\u2013603 (2004)","journal-title":"Combinatorica"},{"key":"33_CR6","unstructured":"Biere, A.: Booleforce. http:\/\/fmv.jku.at\/booleforce\/"},{"key":"33_CR7","unstructured":"Biere, A.: TraceCheck. http:\/\/fmv.jku.at\/tracecheck\/"},{"issue":"2\u20134","key":"33_CR8","doi-asserted-by":"publisher","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. J. Satisfiability Boolean Model. Comput. 4(2\u20134), 75\u201397 (2008)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-030-51825-7_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"ML Bonet","year":"2020","unstructured":"Bonet, M.L., Levy, J.: Equivalence between systems stronger than resolution. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 166\u2013181. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_13"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11814948_24","volume-title":"Theory and Applications of Satisfiability Testing","author":"ML Bonet","year":"2006","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: A complete calculus for max-SAT. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 240\u2013251. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_24"},{"key":"33_CR11","doi-asserted-by":"publisher","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\u00e0b, F.: Resolution for Max-SAT. Artif. Intell. 171, 606\u2013618 (2007)","journal-title":"Artif. Intell."},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Almeida, D., Gr\u00e9goire, \u00c9.: Model-based diagnosis with default information implemented through MAX-SAT technology. In: IEEE 13th International Conference on Information Reuse & Integration, pp. 33\u201336. IEEE (2012)","DOI":"10.1109\/IRI.2012.6302987"},{"key":"33_CR13","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). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_19"},{"key":"33_CR14","first-page":"363","volume":"2003","author":"S de Givry","year":"2003","unstructured":"de Givry, S., Larrosa, J., Meseguer, P., Schiex, T.: Solving max-sat as weighted csp. Principles Pract. Constraint Program. - CP 2003, 363\u2013376 (2003)","journal-title":"Principles Pract. Constraint Program. - CP"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"941","DOI":"10.1007\/978-3-642-33558-7_67","volume-title":"Principles and Practice of Constraint Programming","author":"J Guerra","year":"2012","unstructured":"Guerra, J., Lynce, I.: Reasoning over biological networks using maximum satisfiability. In: Milano, M. (ed.) CP 2012. LNCS, pp. 941\u2013956. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33558-7_67"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Hertel, A., Urquhart, A.: Algorithms and complexity results for input and unit resolution. J. Satisfiability Boolean Model. Comput. 6, 141\u2013164 (2009)","DOI":"10.3233\/SAT190066"},{"key":"33_CR17","unstructured":"Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of Structure in Complexity Theory. Tenth Annual IEEE Conference (1995)"},{"key":"33_CR18","unstructured":"K\u00fcegel, A.: Improved exact solver for the weighted max-sat problem. In: POS-10. Pragmatics of SAT. EPiC Series in Computing, vol. 8, pp. 15\u201327. EasyChair (2012)"},{"key":"33_CR19","unstructured":"Larrosa, J., Heras, F.: Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In: IJCAI International Joint Conference on Artificial Intelligence - IJCAI 2005, pp. 193\u2013198 (01 2005)"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Larrosa, J., Rollon, E.: Augmenting the power of (Partial) MaxSat resolution with extension. In: Proceedings of the AAAI Conference on Artificial Intelligence (2020)","DOI":"10.1609\/aaai.v34i02.5516"},{"key":"33_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-030-51825-7_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"J Larrosa","year":"2020","unstructured":"Larrosa, J., Rollon, E.: Towards a better understanding of (Partial Weighted) MaxSAT proof systems. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 218\u2013232. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_16"},{"key":"33_CR22","unstructured":"Li, C.M., Many\u00e0, F., Soler, J.R.: A Clause Tableau Calculus for MaxSAT. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, pp. 766\u2013772 (2016)"},{"key":"33_CR23","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1613\/jair.2215","volume":"30","author":"CM Li","year":"2007","unstructured":"Li, C.M., Many\u00e0, F., Planes, J.: New inference rules for Max-SAT. J. Artif. Intell. Res. (JAIR) 30, 321\u2013359 (2007)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"33_CR24","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0060630","volume-title":"Symposium on Automatic Demonstration","author":"DW Loveland","year":"1970","unstructured":"Loveland, D.W.: A linear format for resolution. In: Laudet, M., Lacombe, D., Nolin, L., Sch\u00fctzenberger, M. (eds.) Symposium on Automatic Demonstration. LNM, vol. 125, pp. 147\u2013162. Springer, Heidelberg (1970). https:\/\/doi.org\/10.1007\/BFb0060630"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications (invited paper). In: 2010 40th IEEE International Symposium on Multiple-Valued Logic, pp. 9\u201314 (2010)","DOI":"10.1109\/ISMVL.2010.11"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Theory and Applications of Satisfiability Testing - SAT 2014\u201317th International Conference. Lecture Notes in Computer Science, vol. 8561, pp. 438\u2013445 (2014)","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 2717\u20132723 (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"33_CR28","doi-asserted-by":"crossref","unstructured":"Py, M., Cherif, M.S., Habet, D.: Towards bridging the gap between sat and max-sat refutations. In: 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI), pp. 137\u2013144 (2020)","DOI":"10.1109\/ICTAI50040.2020.00032"},{"key":"33_CR29","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, 23\u201341 (1965)","journal-title":"J. Assoc. Comput. Mach."},{"key":"33_CR30","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2307\/421131","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symbolic Logic 1, 425\u2013467 (1995)","journal-title":"Bull. Symbolic Logic"},{"key":"33_CR31","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1137\/090772897","volume":"40","author":"A Urquhart","year":"2011","unstructured":"Urquhart, A.: A near-optimal separation of regular and general resolution. SIAM J. Comput. 40, 107\u2013121 (2011)","journal-title":"SIAM J. Comput."},{"key":"33_CR32","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1109\/TCAD.2003.811450","volume":"22","author":"H Xu","year":"2003","unstructured":"Xu, H., Rutenbar, R.A., Sakallah, K.A.: Sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 22, 814\u2013820 (2003)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T09:44:52Z","timestamp":1672652692000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}