{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T12:45:17Z","timestamp":1759063517572},"reference-count":35,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2019,8,27]],"date-time":"2019-08-27T00:00:00Z","timestamp":1566864000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"Project LOGISTAR"},{"name":"EU H2020 Research and Innovation Programme under","award":["769142"],"award-info":[{"award-number":["769142"]}]},{"name":"MINECO-FEDER projects RASO","award":["TIN2015-71799-C2-1-P\/2-P"],"award-info":[{"award-number":["TIN2015-71799-C2-1-P\/2-P"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,1,25]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving both MaxSAT and MinSAT, in that the minimum number of generated empty clauses provides an optimal MaxSAT solution and the maximum number provides an optimal MinSAT solution.<\/jats:p>","DOI":"10.1093\/jigpal\/jzz025","type":"journal-article","created":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T19:12:17Z","timestamp":1560366737000},"page":"7-27","source":"Crossref","is-referenced-by-count":8,"title":["Clause tableaux for maximum and minimum satisfiability"],"prefix":"10.1093","volume":"29","author":[{"given":"Josep","family":"Argelich","sequence":"first","affiliation":[{"name":"Departament d' Inform\u00e0tica i Enginyeria Industrial (DIEI), Universitat de Lleida, 25001 Lleida, Spain"}]},{"given":"Chu Min","family":"Li","sequence":"additional","affiliation":[{"name":"MIS, Universit\u00e9 de Picardie Jules Verne, 80039 Amiens, France"}]},{"given":"Felip","family":"Many\u00e0","sequence":"additional","affiliation":[{"name":"Artificial Intelligence Research Institute (IIIA, CSIC), 08193 Bellaterra, Spain"}]},{"given":"Joan Ramon","family":"Soler","sequence":"additional","affiliation":[{"name":"Artificial Intelligence Research Institute (IIIA, CSIC), 08193 Bellaterra, Spain"}]}],"member":"286","published-online":{"date-parts":[[2019,8,27]]},"reference":[{"key":"2021012207114110000_ref1","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1109\/ICTAI.2014.58","article-title":"Local Max-Resolution in branch and bound solvers for Max-SAT","volume-title":"26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, Limassol, Cyprus","author":"Abram\u00e9","year":"2014"},{"key":"2021012207114110000_ref2","first-page":"268","article-title":"On the resiliency of unit propagation to Max-Resolution","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI-2015, Buenos Aires, Argentina","author":"Abram\u00e9","year":"2015"},{"key":"2021012207114110000_ref3","first-page":"334","article-title":"A Max-SAT solver with lazy data structures","volume-title":"Proceedings of the 9th Ibero-American Conference on Artificial Intelligence, IBERAMIA 2004, Puebla, M\u00e9xico","author":"Alsinet"},{"key":"2021012207114110000_ref4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10732-015-9300-7","article-title":"Exploiting subproblem optimization in SAT-based MaxSAT algorithms","volume":"22","author":"Ans\u00f3tegui","year":"2016","journal-title":"Journal of Heuristics"},{"key":"2021012207114110000_ref5","first-page":"51","article-title":"A Max-SAT-based approach to constructing optimal covering arrays","volume-title":"Proceedings of the 16th International Conference of the Catalan Association for Artificial Intelligence, CCIA 2013, Vic, Spain","author":"Ans\u00f3tegui","year":"2013"},{"key":"2021012207114110000_ref6","first-page":"185","article-title":"A SAT-based approach to MinSAT","volume-title":"Proceedings of the 15th International Conference of the Catalan Association for Artificial Intelligence, CCIA-2012, Alacant, Spain","author":"Ans\u00f3tegui","year":"2012"},{"key":"2021012207114110000_ref7","doi-asserted-by":"crossref","first-page":"251","DOI":"10.3233\/SAT190047","article-title":"The first and second max-SAT evaluations","volume":"4","author":"Argelich","year":"2008","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"2021012207114110000_ref8","first-page":"17","article-title":"Clause branching in MaxSAT and MinSAT","volume-title":"Proceedings of the 21st International Conference of the Catalan Association for Artificial Intelligence,, CCIA 2018, Alt Empord\u00e0, Spain","author":"Argelich","year":"2018"},{"key":"2021012207114110000_ref9","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/11814948_24","article-title":"A complete calculus for Max-SAT","volume-title":"Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT-2006, Seattle, USA","author":"Bonet","year":"2006"},{"key":"2021012207114110000_ref10","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1016\/j.artint.2007.03.001","article-title":"Resolution for max-SAT","volume":"171","author":"Bonet","year":"2007","journal-title":"Artificial Intelligence"},{"key":"2021012207114110000_ref11","first-page":"186","article-title":"Solving MaxSAT with natural deduction","volume-title":"Proceedings of the 20th International Conference of the Catalan Association for Artificial Intelligence,, CCIA 2017, Deltebre, Spain","author":"Casas-Roma","year":"2017"},{"key":"2021012207114110000_ref12","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/978-94-017-1754-0_2","article-title":"Tableaux methods for classical propositional logic","volume-title":"Handbook of Tableau Methods","author":"D\u2019Agostino","year":"1999"},{"key":"2021012207114110000_ref13","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications of the ACM"},{"key":"2021012207114110000_ref14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"2021012207114110000_ref15","first-page":"252","article-title":"On solving the partial MAX-SAT problem","volume-title":"Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT-2006, Seattle, USA","author":"Zhaohui","year":"2006"},{"key":"2021012207114110000_ref16","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1016\/B978-044450813-3\/50005-9","article-title":"Tableaux and related methods","volume-title":"Handbook of Automated Reasoning","author":"H\u00e4hnle","year":"2001"},{"key":"2021012207114110000_ref17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1613\/jair.2347","article-title":"MiniMaxSAT: an efficient weighted max-SAT solver","volume":"31","author":"Heras","year":"2008","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2021012207114110000_ref18","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00881805","article-title":"Branching rules for satisfiability","volume":"15","author":"Hooker","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"2021012207114110000_ref19","doi-asserted-by":"crossref","first-page":"351","DOI":"10.3233\/AIC-150685","article-title":"Maximal falsifiability","volume":"29","author":"Ignatiev","year":"2016","journal-title":"AI Communications"},{"key":"2021012207114110000_ref20","first-page":"193","article-title":"Resolution in Max-SAT and its relation to local consistency in weighted CSPs","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI-2005, Edinburgh, Scotland","author":"Larrosa","year":"2005"},{"key":"2021012207114110000_ref21","first-page":"613","article-title":"MaxSAT, hard and soft constraints","volume-title":"Handbook of Satisfiability","author":"Li","year":"2009"},{"key":"2021012207114110000_ref22","first-page":"1959","article-title":"An exact inference scheme for MinSAT","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI-2015, Buenos Aires, Argentina","author":"Li","year":"2015"},{"key":"2021012207114110000_ref23","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/s10601-010-9097-9","article-title":"Resolution-based lower bounds in MaxSAT","volume":"15","author":"Li","year":"2010","journal-title":"Constraints"},{"key":"2021012207114110000_ref24","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1613\/jair.2215","article-title":"New inference rules for max-SAT","volume":"30","author":"Li","year":"2007","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2021012207114110000_ref25","first-page":"88","article-title":"A clause tableau calculus for MinSAT","volume-title":"Proceedings of the 19th International Conference of the Catalan Association for Artificial Intelligence, CCIA 2016, Barcelona, Spain","author":"Li","year":"2016"},{"key":"2021012207114110000_ref26","first-page":"766","article-title":"A clause tableaux calculus for MaxSAT","volume-title":"Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI-2016, New York, USA","author":"Li","year":"2016"},{"key":"2021012207114110000_ref27","first-page":"605","article-title":"Minimum satisfiability and its applications","volume-title":"Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI-2011, Barcelona, Spain","author":"Li","year":"2011"},{"key":"2021012207114110000_ref28","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1016\/j.artint.2012.05.004","article-title":"Optimizing with minimum satisfiability","volume":"190","author":"Li","year":"2012","journal-title":"Artificial Intelligence"},{"key":"2021012207114110000_ref29","first-page":"2334","article-title":"Exploiting inference rules to compute lower bounds for MAX-SAT solving","volume-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI-2007, Hyderabad, India","author":"Lin","year":"2007"},{"key":"2021012207114110000_ref30","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-319-63516-3_3","article-title":"Parallel maximum satisfiability","volume-title":"Handbook of Parallel Constraint Reasoning","author":"Lynce","year":"2018"},{"key":"2021012207114110000_ref31","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/978-3-642-02777-2_45","article-title":"Algorithms for weighted Boolean optimization","volume-title":"Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, SAT-2009, Swansea, UK","author":"Manquinho","year":"2009"},{"key":"2021012207114110000_ref32","first-page":"164","article-title":"A MaxSAT-based approach to the team composition problem in a classroom","volume-title":"Autonomous Agents and Multiagent Systems\u2014AAMAS 2017 Workshops, Visionary Papers, S\u00e3o Paulo, Brazil","author":"Many\u00e0","year":"2017"},{"key":"2021012207114110000_ref33","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","article-title":"Incremental cardinality constraints for MaxSAT","volume-title":"Principles and Practice of Constraint Programming\u201420th International Conference, CP, Lyon, France","author":"Martins","year":"2014"},{"key":"2021012207114110000_ref34","first-page":"2717","article-title":"Maximum satisfiability using core-guided MaxSAT resolution","author":"Narodytska","year":"2014","journal-title":"Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, Qu\u00e9bec City, Canada"},{"key":"2021012207114110000_ref35","article-title":"First-Order Logic","author":"Smullyan","year":"1995"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/1\/7\/35933737\/jzz025.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/1\/7\/35933737\/jzz025.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,23]],"date-time":"2021-01-23T17:57:41Z","timestamp":1611424661000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/29\/1\/7\/5544641"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,27]]},"references-count":35,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2019,8,27]]},"published-print":{"date-parts":[[2021,1,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzz025","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2021,2]]},"published":{"date-parts":[[2019,8,27]]}}}