{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T00:49:07Z","timestamp":1763686147943},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030290252"},{"type":"electronic","value":"9783030290269"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29026-9_4","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T23:10:06Z","timestamp":1566429006000},"page":"58-73","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Tableau Calculus for Non-clausal Maximum Satisfiability"],"prefix":"10.1007","author":[{"given":"Chu Min","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felip","family":"Many\u00e0","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joan Ramon","family":"Soler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"key":"4_CR1","first-page":"92","volume-title":"Lecture Notes in Computer Science","author":"Andr\u00e9 Abram\u00e9","year":"2014","unstructured":"Abram\u00e9, A., Habet, D.: Efficient application of max-sat resolution on inconsistent subsets. In: Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, CP, Lyon, France, pp. 92\u2013107 (2014)"},{"key":"4_CR2","unstructured":"Abram\u00e9, A., Habet, D.: On the resiliency of unit propagation to Max-Resolution. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI, Buenos Aires, Argentina, pp. 268\u2013274 (2015)"},{"key":"4_CR3","unstructured":"Argelich, J., Li, C.M., Many\u00e0, F., Soler, J.R.: Clause branching in MaxSAT and MinSAT. In: Proceedings of the 21st International Conference of the Catalan Association for Artificial Intelligence, Roses, Spain. Frontiers in Artificial Intelligence and Applications, vol. 308, pp. 17\u201326. IOS Press (2018)"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Argelich, J., Li, C.M., Many\u00e0, F., Soler, J.R.: Clause tableaux for maximum and minimum satisfiability. Logic J. IGPL (2019). https:\/\/doi.org\/10.1093\/jigpal\/jzz025","DOI":"10.1093\/jigpal\/jzz025"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-18008-3_5","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"Miquel Bofill","year":"2015","unstructured":"Bofill, M., Garcia, M., Suy, J., Villaret, M.: MaxSAT-based scheduling of B2B meetings. In: Proceedings of the12th International Conference on Integration of AI and OR Techniques in Constraint Programming, CPAIOR, Barcelona, Spain, pp. 65\u201373 (2015)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Bonet, M.L., Buss, S., Ignatiev, A., Marques-Silva, J., Morgado, A.: MaxSAT resolution with the dual rail encoding. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence, AAAI, New Orleans, Louisiana, USA, pp. 6565\u20136572 (2018)","DOI":"10.1609\/aaai.v32i1.12204"},{"issue":"8\u20139","key":"4_CR7","first-page":"240","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), 240\u2013251 (2007)","journal-title":"Artif. Intell."},{"key":"4_CR8","unstructured":"Casas-Roma, J., Huertas, A., Many\u00e0, F.: Solving MaxSAT with natural deduction. In: Proceedings of the 20th International Conference of the Catalan Association for Artificial Intelligence, Deltebre, Spain. Frontiers in Artificial Intelligence and Applications, vol. 300, pp. 186\u2013195. IOS Press (2017)"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-94-017-1754-0_2","volume-title":"Handbook of Tableau Methods","author":"M D\u2019Agostino","year":"1999","unstructured":"D\u2019Agostino, M.: Tableaux methods for classical propositional logic. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 45\u2013123. Springer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-017-1754-0_2"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Almeida, D., Gr\u00e9goire, \u00c9.: Model-based diagnosis with default information implemented through MAX-SAT technology. In: Proceedings of the IEEE 13th International Conference on Information Reuse & Integration, IRI, Las Vegas, NV, USA, pp. 33\u201336 (2012)","DOI":"10.1109\/IRI.2012.6302987"},{"key":"4_CR11","first-page":"941","volume-title":"Lecture Notes in Computer Science","author":"Jo\u00e3o Guerra","year":"2012","unstructured":"Guerra, J., Lynce, I.: Reasoning over biological networks using maximum satisfiability. In: Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming, CP, Qu\u00e9bec City, QC, Canada, pp. 941\u2013956 (2012)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100\u2013178. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"4_CR13","unstructured":"Heras, F., Larrosa, J.: New inference rules for efficient Max-SAT solving. In: Proceedings of the National Conference on Artificial Intelligence, AAAI-2006, Boston\/MA, USA, pp. 68\u201373 (2006)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-319-66263-3_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"A Ignatiev","year":"2017","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: On tackling the limits of resolution in SAT solving. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 164\u2013183. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_11"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Jabbour, S., Mhadhbi, N., Raddaoui, B., Sais, L.: A SAT-based framework for overlapping community detection in networks. In: Proceedings of the 21st Pacific-Asia Conference on Advances in Knowledge Discovery and Data Mining, Part II, PAKDD, Jeju, South Korea, pp. 786\u2013798 (2017)","DOI":"10.1007\/978-3-319-57529-2_61"},{"key":"4_CR16","unstructured":"Larrosa, J., Heras, F.: Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In: Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI-2005, Edinburgh, Scotland, pp. 193\u2013198. Morgan Kaufmann (2005)"},{"key":"4_CR17","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. 30, 321\u2013359 (2007)","journal-title":"J. Artif. Intell. Res."},{"key":"4_CR18","unstructured":"Li, C.M., Many\u00e0, F., Soler, J.R.: A clause tableaux calculus for MaxSAT. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI-2016, New York, USA, pp. 766\u2013772 (2016)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Li, C.M., Many\u00e0, F., Soler, J.R.: Clausal form transformation in MaxSAT. In: Proceedings of the 49th IEEE International Symposium on Multiple-Valued Logic, ISMVL, Fredericton, Canada, pp. 132\u2013137 (2019)","DOI":"10.1109\/ISMVL.2019.00031"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1016\/j.artint.2012.05.004","volume":"190","author":"CM Li","year":"2012","unstructured":"Li, C.M., Zhu, Z., Many\u00e0, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32\u201344 (2012)","journal-title":"Artif. Intell."},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-319-71679-4_11","volume-title":"Autonomous Agents and Multiagent Systems","author":"F Many\u00e0","year":"2017","unstructured":"Many\u00e0, F., Negrete, S., Roig, C., Soler, J.R.: A MaxSAT-based approach to the team composition problem in a classroom. In: Sukthankar, G., Rodriguez-Aguilar, J.A. (eds.) AAMAS 2017. LNCS (LNAI), vol. 10643, pp. 164\u2013173. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71679-4_11"},{"issue":"3\u20134","key":"4_CR22","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10472-011-9233-2","volume":"62","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Argelich, J., Gra\u00e7a, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3\u20134), 317\u2013343 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A.G., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Proceedings of 7th International Conference on Formal Methods in Computer-Aided Design, FMCAD, Austin, Texas, USA, pp. 13\u201319 (2007)","DOI":"10.1109\/FMCAD.2007.4401977"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Smullyan, R.: First-Order Logic. Dover Publications, New York (1995). Second corrected edition, First published 1968 by Springer-Verlag","DOI":"10.1007\/978-3-642-86718-7"},{"issue":"6","key":"4_CR25","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. CAD Integr. Circuits Syst. 22(6), 814\u2013820 (2003)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, L., Bacchus, F.: MAXSAT heuristics for cost optimal planning. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, Ontario, Canada, pp. 1846\u20131852 (2012)","DOI":"10.1609\/aaai.v26i1.8373"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29026-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,26]],"date-time":"2022-09-26T02:37:46Z","timestamp":1664159866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29026-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290252","9783030290269"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29026-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tableaux2019.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"58% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}