The MaxSAT Problem in the Real-Valued MV-Algebra

0583783 - ÚI 2024 RIV CH eng C - Konferenční příspěvek (zahraniční konf.)
Haniková, Zuzana - Manya, F. - Vidal, A.
The MaxSAT Problem in the Real-Valued MV-Algebra.
Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2023 Proceedings. Cham: Springer, 2023 - (Ramanayake, R.; Urban, J.), s. 386-404. Lecture Notes in Computer Science, 14278. ISBN 978-3-031-43512-6. ISSN 0302-9743.
[TABLEAUX 2023: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods /32./. Prague (CZ), 18.09.2024-21.09.2024]
Grant ostatní: AV ČR(CZ) CSIC-20-12
Program: Bilaterální spolupráce
Institucionální podpora: RVO:67985807
Klíčová slova: Maximum satisfiability * Satisfiability * Łukasiewicz logic * MV-algebra
Obor OECD: Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
https://link.springer.com/chapter/10.1007/978-3-031-43513-3_21

This work addresses the maximum satisfiability (MaxSAT) problem for a multiset of arbitrary formulas of the language of propositional Łukasiewicz logic over the MV-algebra whose universe is the real interval [0,1]. First, we reduce the MaxSAT problem to the SAT problem over the same algebra. This solution method sets a benchmark for other approaches, allowing a classification of the MaxSAT problem in terms of metric reductions introduced by Krentel. We later define an alternative analytic method with preprocessing in terms of a Tseitin transformation of the input, followed by a reduction to a system of linear constraints, in analogy to the earlier approaches of Hähnle and Olivetti. We discuss various aspects of these approaches to solving the problem.
Trvalý link: https://hdl.handle.net/11104/0351788