A Tableau Calculus for Non-clausal Maximum Satisfiability - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

A Tableau Calculus for Non-clausal Maximum Satisfiability

(1) , (2) ,
1
2

Résumé

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.
Fichier non déposé

Dates et versions

hal-03636422 , version 1 (10-04-2022)

Identifiants

Citer

Chu Min Li, Felip Manya, Joan Ramon Soler. A Tableau Calculus for Non-clausal Maximum Satisfiability. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2019, Sep 2019, London, United Kingdom. pp.58-73, ⟨10.1007/978-3-030-29026-9\_4⟩. ⟨hal-03636422⟩

Collections

U-PICARDIE MIS
16 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook Twitter LinkedIn More