Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

A resolution calculus for MinSAT

Abstract : The logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy proposed here. We then describe an exact variable elimination algorithm for MinSAT based on that rule. Finally, we show how the results for Boolean MinSAT can be extended to solve the MinSAT problem of the multiple-valued clausal forms known as signed conjunctive normal form formulas.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-u-picardie.archives-ouvertes.fr/hal-03636410
Contributeur : Louise DESSAIVRE Connectez-vous pour contacter le contributeur
Soumis le : dimanche 10 avril 2022 - 11:39:06
Dernière modification le : mardi 30 août 2022 - 16:58:22

Identifiants

Collections

Citation

Chu-Min Li, Fan Xiao, Felip Manya. A resolution calculus for MinSAT. Logic Journal of the IGPL, Oxford University Press (OUP), 2021, 29 (1), pp.28-44. ⟨10.1093/jigpal/jzz028⟩. ⟨hal-03636410⟩

Partager

Métriques

Consultations de la notice

27