{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T12:50:09Z","timestamp":1759063809694,"version":"3.37.3"},"reference-count":39,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T00:00:00Z","timestamp":1571788800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"EU H2020 Research and Innovation Programme","award":["769142"],"award-info":[{"award-number":["769142"]}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["TIN2015-71799-C2-1-P"],"award-info":[{"award-number":["TIN2015-71799-C2-1-P"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]}],"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 logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy proposed here. We then describe an exact variable elimination algorithm for MinSAT based on that rule. Finally, we show how the results for Boolean MinSAT can be extended to solve the MinSAT problem of the multiple-valued clausal forms known as signed conjunctive normal form formulas.<\/jats:p>","DOI":"10.1093\/jigpal\/jzz028","type":"journal-article","created":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T19:10:51Z","timestamp":1560798651000},"page":"28-44","source":"Crossref","is-referenced-by-count":3,"title":["A resolution calculus for MinSAT"],"prefix":"10.1093","volume":"29","author":[{"given":"Chu-Min","family":"Li","sequence":"first","affiliation":[{"name":"School of Computer Science, Huazhong University of Science and Technology, 430074 Wuhan, China and MIS, Universit\u00e9 de Picardie Jules Verne, 80080 Amiens, France"}]},{"given":"Fan","family":"Xiao","sequence":"additional","affiliation":[{"name":"School of Computer Science, Huazhong University of Science and Technology, 430074 Wuhan, China"}]},{"given":"Felip","family":"Many\u00e0","sequence":"additional","affiliation":[{"name":"Artificial Intelligence Research Institute (IIIA, CSIC), 08193 Bellaterra, Spain"}]}],"member":"286","published-online":{"date-parts":[[2019,10,23]]},"reference":[{"key":"2021012207114135500_ref1","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":"2021012207114135500_ref2","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-540-30498-2_34","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","year":"2004"},{"key":"2021012207114135500_ref3","first-page":"22","article-title":"A complete resolution calculus for Signed Max-SAT","volume-title":"Proceedings of the 37th International Symposium on Multiple-Valued Logic (ISMVL), Oslo, Norway","author":"Ans\u00f3tegui","year":"2007"},{"key":"2021012207114135500_ref4","first-page":"167","article-title":"Inference rules for high-order consistency in weighted CSP","volume-title":"Proceedings of the 22nd AAAI Conference on Artificial Intelligence, AAAI 2007, Vancouver, Canada","author":"Ans\u00f3tegui","year":"2007"},{"key":"2021012207114135500_ref5","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1002\/9780470612309.ch19","article-title":"The logic behind weighted CSP","volume-title":"Trends in Constraint Programming","author":"Ans\u00f3tegui","year":"2007"},{"key":"2021012207114135500_ref6","first-page":"32","article-title":"The logic behind weighted CSP","volume-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI-2007, Hyderabad, India","author":"Ans\u00f3tegui","year":"2007"},{"key":"2021012207114135500_ref7","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.ins.2012.12.004","article-title":"Resolution procedures for multiple-valued optimization","volume":"227","author":"Ans\u00f3tegui","year":"2013","journal-title":"Information Sciences"},{"key":"2021012207114135500_ref8","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":"2021012207114135500_ref9","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":"2021012207114135500_ref10","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":"2021012207114135500_ref11","first-page":"133","article-title":"MinSAT versus MaxSAT for optimization problems","volume-title":"Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming, CP 2013, Uppsala, Sweden","author":"Argelich","year":"2013"},{"key":"2021012207114135500_ref12","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1006\/jsco.1995.1021","article-title":"Resolution-based theorem proving for many-valued logics","volume":"19","author":"Baaz","year":"1995","journal-title":"Journal of Symbolic Computation"},{"key":"2021012207114135500_ref13","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-94-011-4040-9_3","article-title":"The SAT problem of signed CNF formulas","volume-title":"Labelled Deduction","author":"Beckert","year":"2000"},{"key":"2021012207114135500_ref14","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":"2021012207114135500_ref15","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":"2021012207114135500_ref16","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":"Z."},{"key":"2021012207114135500_ref17","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0452-6_5","article-title":"Advanced many-valued logic","volume-title":"Handbook of Philosophical Logic","author":"H\u00e4hnle","year":"2001"},{"key":"2021012207114135500_ref18","doi-asserted-by":"crossref","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","article-title":"Short conjunctive normal forms in finitely-valued logics","volume":"4","author":"H\u00e4hnle","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"2021012207114135500_ref19","first-page":"69","article-title":"Deduction in many-valued logics: a survey","volume":"4","author":"H\u00e4hnle","year":"1997","journal-title":"Mathware and Soft Computing"},{"key":"2021012207114135500_ref20","first-page":"68","article-title":"New inference rules for efficient Max-SAT solving","volume-title":"Proceedings of the National Conference on Artificial Intelligence, AAAI-2006, Boston\/MA, USA","author":"Heras","year":"2006"},{"key":"2021012207114135500_ref21","first-page":"103","article-title":"On reducing maximum independent set to minimum satisfiability","volume-title":"Proc 17th International Conference on Theory and Applications of Satisfiability Testing, SAT, Vienna, Austria","author":"Ignatiev","year":"2014"},{"key":"2021012207114135500_ref22","first-page":"164","article-title":"On tackling the limits of resolution in SAT solving","volume-title":"Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing, SAT, Melbourne, Australia","author":"Ignatiev","year":"2017"},{"key":"2021012207114135500_ref23","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":"2021012207114135500_ref24","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1016\/j.artint.2007.05.006","article-title":"A logical approach to efficient max-SAT solving","volume":"172","author":"Larrosa","year":"2008","journal-title":"Artificial Intelligence"},{"key":"2021012207114135500_ref25","first-page":"613","article-title":"MaxSAT, hard and soft constraints","volume-title":"Handbook of Satisfiability","author":"Li","year":"2009"},{"key":"2021012207114135500_ref26","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":"2021012207114135500_ref27","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":"2021012207114135500_ref28","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":"2021012207114135500_ref29","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":"2021012207114135500_ref30","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":"2021012207114135500_ref31","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":"2021012207114135500_ref32","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":"2021012207114135500_ref33","first-page":"495","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":"Vasco","year":"2009"},{"key":"2021012207114135500_ref34","first-page":"307","article-title":"The 2-SAT problem in signed CNF formulas","volume":"5","author":"Many\u00e0","year":"2000","journal-title":"Multiple-Valued Logic: An International Journal"},{"key":"2021012207114135500_ref35","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, Revised Selected Papers","author":"Many\u00e0"},{"year":"2014","author":"Martins","key":"2021012207114135500_ref36"},{"key":"2021012207114135500_ref37","doi-asserted-by":"crossref","first-page":"237","DOI":"10.3233\/FI-1994-2135","article-title":"Adapting classical inference techniques to multiple-valued logics using signed formulas","volume":"21","author":"V.","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"2021012207114135500_ref38","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":"2021012207114135500_ref39","first-page":"455","article-title":"A new encoding from MinSAT into MaxSAT","volume-title":"Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming, CP 2012, Qu\u00e9bec City, QC, Canada","author":"Zhu"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/1\/28\/35933772\/jzz028.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/1\/28\/35933772\/jzz028.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,23]],"date-time":"2021-01-23T17:57:47Z","timestamp":1611424667000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/29\/1\/28\/5602375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,23]]},"references-count":39,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2019,10,23]]},"published-print":{"date-parts":[[2021,1,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzz028","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2021,2]]},"published":{"date-parts":[[2019,10,23]]}}}