{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T23:34:32Z","timestamp":1763681672566,"version":"3.45.0"},"reference-count":22,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T00:00:00Z","timestamp":1763596800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,11,25]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>In this paper we provide a new tableau characterization for the Weighted Partial Regular MinSat and Weighted Partial Regular MaxSat problems, which are, respectively, variants of the Minimum and Maximum Satisfiability problems. Our characterization has the advantage of constructing tableaux with fewer nodes compared to those built with known characterizations. We address the problems for the case of formulas in non-clausal form. We also discuss how our results can be adapted to the other versions of these problems.<\/jats:p>","DOI":"10.1093\/jigpal\/jzaf058","type":"journal-article","created":{"date-parts":[[2025,7,17]],"date-time":"2025-07-17T10:06:24Z","timestamp":1752746784000},"source":"Crossref","is-referenced-by-count":0,"title":["New tableau characterizations for non-clausal regular MinSAT and MaxSAT problems"],"prefix":"10.1093","volume":"33","author":[{"given":"Guido","family":"Fiorino","sequence":"first","affiliation":[{"name":"DISCO , Univ. degli Studi di Milano-Bicocca, Viale Sarca, 336, 20126, Milano, Italy"}]}],"member":"286","published-online":{"date-parts":[[2025,11,20]]},"reference":[{"key":"2025112018102409500_ref1","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10732-022-09495-3","article-title":"Incomplete MaxSat approaches for combinatorial testing","volume":"28","author":"Ans\u00f3tegui","year":"2022","journal-title":"J Heuristics"},{"key":"2025112018102409500_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-4040-9_3","article-title":"The SAT problem of signed CNF formulas","author":"Beckert","year":"2000","journal-title":"Labelled Deduction. Applied Logic Series, vol 17"},{"key":"2025112018102409500_ref3","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1613\/jair.1.12670","article-title":"Constraint solving approaches to the business-to-business meeting scheduling problem","volume":"74","author":"Bofill","year":"2022","journal-title":"J Artif Intell Res"},{"key":"2025112018102409500_ref4","first-page":"214","article-title":"Between sat and csp: propositional satisfaction problems and clausal CSPs","volume-title":"Proceedings, European Conference on Artificial Intelligence (ECAI)","author":"Castell","year":"1998"},{"key":"2025112018102409500_ref5","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1109\/ISMVL60454.2024.00035","article-title":"A tableau calculus for non-clausal regular MaxSAT","volume-title":"2024 IEEE 54th International Symposium on Multiple-Valued Logic (ISMVL)","author":"Coll","year":"2024"},{"key":"2025112018102409500_ref6","first-page":"278","article-title":"A complete tableau calculus for non-clausal regular minsat","volume-title":"Artificial Intelligence Research and Development - Proceedings of the 26th International Conference of the Catalan Association for Artificial Intelligence, CCIA 2024, Barcelona, Spain, 2-4 October 2024, volume 390 of Frontiers in Artificial Intelligence and Applications","author":"Coll","year":"2024"},{"key":"2025112018102409500_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2023.109010","article-title":"MaxSat resolution for regular propositional logic","volume":"162","author":"Coll","year":"2023","journal-title":"Int J Approx Reason"},{"key":"2025112018102409500_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.cogsys.2024.101319","article-title":"Complete tableau calculi for regular MaxSat and regular MinSat","volume":"90","author":"Coll","year":"2025","journal-title":"Cogn Syst Res"},{"key":"2025112018102409500_ref9","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/IRI.2012.6302987","article-title":"Model-based diagnosis with default information implemented through MaxSat technology","volume-title":"2012 IEEE 13th International Conference on Information Reuse & Integration (IRI)","author":"d\u2019Almeida","year":"2012"},{"key":"2025112018102409500_ref10","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1093\/jigpal\/jzab012","article-title":"New tableau characterizations for non-clausal MaxSat problem","volume":"30","author":"Fiorino","year":"2022","journal-title":"Log J IGPL"},{"key":"2025112018102409500_ref11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-022-09653-z","article-title":"Linear depth deduction with subformula property for intuitionistic epistemic logic","volume":"67","author":"Fiorino","year":"2023","journal-title":"J Automated Reason"},{"key":"2025112018102409500_ref12","article-title":"Intuitionistic logic","volume-title":"Model Theory and Forcing","author":"Fitting","year":"1969"},{"key":"2025112018102409500_ref13","doi-asserted-by":"publisher","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":"J Log Comput"},{"key":"2025112018102409500_ref14","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/3-540-44957-4_19","article-title":"Model generation theorem proving with finite interval constraints","volume-title":"Computational Logic \u2014 CL 2000","author":"H\u00e4hnle","year":"2000"},{"key":"2025112018102409500_ref15","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0743-1066(92)90007-P","article-title":"Theory of generalized annotated logic programming and its applications","volume":"12","author":"Kifer","year":"1992","journal-title":"J Log Program"},{"key":"2025112018102409500_ref16","first-page":"766","article-title":"A clause tableau calculus for MaxSat","volume-title":"Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016","author":"Li","year":"2016"},{"key":"2025112018102409500_ref17","first-page":"88","article-title":"A clause tableau calculus for minsat","volume-title":"Artificial Intelligence Research and Development - Proceedings of the 19th International Conference of the Catalan Association for Artificial Intelligence, Barcelona, Catalonia, Spain, October 19-21, 2016, volume 288 of Frontiers in Artificial Intelligence and Applications","author":"Li","year":"2016"},{"key":"2025112018102409500_ref18","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/978-3-030-29026-9_4","article-title":"A tableau calculus for non-clausal maximum satisfiability","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, volume 11714 of Lecture Notes in Computer Science","author":"Li","year":"2019"},{"key":"2025112018102409500_ref19","first-page":"jzz028","article-title":"A resolution calculus for MinSAT","volume":"10","author":"Li","year":"2021","journal-title":"Log J IGPL"},{"key":"2025112018102409500_ref20","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10472-011-9233-2","article-title":"Boolean lexicographic optimization: algorithms and applications","volume":"62","author":"Marques-Silva","year":"2011","journal-title":"Ann Math Artif Intell"},{"key":"2025112018102409500_ref21","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/FAMCAD.2007.26","article-title":"Improved design debugging using maximum satisfiability","volume-title":"Formal Methods in Computer Aided Design (FMCAD\u201907)","author":"Safarpour","year":"2007"},{"key":"2025112018102409500_ref22","first-page":"1846","article-title":"MAXSAT heuristics for cost optimal planning","volume-title":"Proceedings of the 26th AAAI Conference on Artificial Intelligence, July 22-26, 2012, Toronto, Ontario, Canada","author":"Zhang","year":"2012"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/6\/jzaf058\/65419024\/jzaf058.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/6\/jzaf058\/65419024\/jzaf058.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T23:10:30Z","timestamp":1763680230000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/doi\/10.1093\/jigpal\/jzaf058\/8332296"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,20]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,11,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzaf058","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2025,12]]},"published":{"date-parts":[[2025,11,20]]},"article-number":"jzaf058"}}