Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

A Tableau Calculus for Non-clausal Maximum Satisfiability

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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-u-picardie.archives-ouvertes.fr/hal-03636422
Contributeur : Louise DESSAIVRE Connectez-vous pour contacter le contributeur
Soumis le : dimanche 10 avril 2022 - 11:39:18
Dernière modification le : vendredi 5 août 2022 - 11:22:18

Identifiants

Collections

Citation

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⟩

Partager

Métriques

Consultations de la notice

16