Arrêt de service programmé du vendredi 10 juin 16h jusqu’au lundi 13 juin 9h. Pour en savoir plus
Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Clause tableaux for maximum and minimum satisfiability

Abstract : The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving both MaxSAT and MinSAT, in that the minimum number of generated empty clauses provides an optimal MaxSAT solution and the maximum number provides an optimal MinSAT solution.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-u-picardie.archives-ouvertes.fr/hal-03636409
Contributeur : Louise Dessaivre Connectez-vous pour contacter le contributeur
Soumis le : dimanche 10 avril 2022 - 11:39:05
Dernière modification le : lundi 11 avril 2022 - 03:00:13

Identifiants

Collections

Citation

Josep Argelich, Chu Min Li, Felip Manya, Joan Ramon Soler. Clause tableaux for maximum and minimum satisfiability. LOGIC JOURNAL OF THE IGPL, 2021, 29 (1), pp.7-27. ⟨10.1093/jigpal/jzz025⟩. ⟨hal-03636409⟩

Partager

Métriques

Consultations de la notice

23