Abstract
We define a non-clausal MaxSAT tableau calculus. Given a multiset of propositional formulas \(\phi \), we prove that the calculus is sound in the sense that if the minimum number of contradictions derived among the branches of a completed tableau for \(\phi \) is m, then the minimum number of unsatisfied formulas in \(\phi \) is m. We also prove that it is complete in the sense that if the minimum number of unsatisfied formulas in \(\phi \) is m, then the minimum number of contradictions among the branches of any completed tableau for \(\phi \) is m. Moreover, we describe how to extend the proposed calculus to deal with hard and weighted soft formulas.
This work was supported by Project LOGISTAR from the EU H2020 Research and Innovation Programme under Grant Agreement No. 769142, MINECO-FEDER projects RASO (TIN2015-71799-C2-1-P) and Generalitat de Catalunya SGR 172.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We use multisets of formulas instead of sets of formulas because duplicated formulas cannot be collapsed into one formula because then the minimum number of unsatisfied formulas might not be preserved.
References
Abramé, 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–107 (2014)
Abramé, 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–274 (2015)
Argelich, J., Li, C.M., Manyà, 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–26. IOS Press (2018)
Argelich, J., Li, C.M., Manyà, F., Soler, J.R.: Clause tableaux for maximum and minimum satisfiability. Logic J. IGPL (2019). https://doi.org/10.1093/jigpal/jzz025
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–73 (2015)
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–6572 (2018)
Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artif. Intell. 171(8–9), 240–251 (2007)
Casas-Roma, J., Huertas, A., Manyà, 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–195. IOS Press (2017)
D’Agostino, M.: Tableaux methods for classical propositional logic. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 45–123. Springer, Dordrecht (1999). https://doi.org/10.1007/978-94-017-1754-0_2
D’Almeida, D., Grégoire, É.: 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–36 (2012)
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ébec City, QC, Canada, pp. 941–956 (2012)
Hähnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100–178. Elsevier and MIT Press (2001)
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–73 (2006)
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–183. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_11
Jabbour, S., Mhadhbi, N., Raddaoui, B., Sais, L.: A SAT-based framework for overlap** 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–798 (2017)
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–198. Morgan Kaufmann (2005)
Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. J. Artif. Intell. Res. 30, 321–359 (2007)
Li, C.M., Manyà, 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–772 (2016)
Li, C.M., Manyà, 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–137 (2019)
Li, C.M., Zhu, Z., Manyà, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32–44 (2012)
Manyà, 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–173. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-71679-4_11
Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3–4), 317–343 (2011)
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–19 (2007)
Smullyan, R.: First-Order Logic. Dover Publications, New York (1995). Second corrected edition, First published 1968 by Springer-Verlag
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–820 (2003)
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–1852 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Li, C.M., Manyà, F., Soler, J.R. (2019). A Tableau Calculus for Non-clausal Maximum Satisfiability. In: Cerrito, S., Popescu, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2019. Lecture Notes in Computer Science(), vol 11714. Springer, Cham. https://doi.org/10.1007/978-3-030-29026-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-29026-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29025-2
Online ISBN: 978-3-030-29026-9
eBook Packages: Computer ScienceComputer Science (R0)