Inférence et certificats pour le problème de satisfiabilité maximum - Aix-Marseille Université Accéder directement au contenu
Thèse Année : 2021

Inference and certificates for the maximum satisfiability problem

Inférence et certificats pour le problème de satisfiabilité maximum

Matthieu Py
  • Fonction : Auteur
  • PersonId : 1090438

Résumé

In this thesis, we are interested in the maximum satisfiability problem, or Max-SAT problem, which consists, given a Boolean formula in conjunctive normal form, in finding an assignment of the variables of the formula which allows to satisfy as many clauses as possible, or, equivalently, to falsify as few clauses as possible. The most widely used Max-SAT proof system is based on the Max-SAT resolution inference rule which is the adaptation for Max-SAT of the resolution rule used for the SAT problem. The resolution rule deduces a new clause from two opposing clauses, enabling to certify that a formula is unsatisfiable by gradually deducing new clauses until deducing a contradiction, represented in the form of an empty clause. The adaptation of such proofs, referred to as resolution refutations, for Max-SAT without considerably increasing its size is an open problem since the introduction of Max-SAT resolution. We propose in this thesis two methods to adapt any resolution resfutation into a valid refutation for Max-SAT, referred to as max-refutation. Another contribution is the construction of certificates to demonstrate the optimality of a solution for the Max-SAT problem. To generate such certificates, we use the max-refutations that we are now able to generate from the resolution refutations. Indeed, as a max-refutation certifies that we must falsify at least one clause of a formula, it is then possible to certify, using k max-refutations that we must falsify at least k clauses of the same formula. This sequence of max-refutations, coupled with an interpretation of the variables allowing to falsify exactly k clauses of the formula, is a certificate for the Max-SAT problem. Finally, we are interested in the problem which consists, given an initial formula and a given information (clause or formula), of inferring this information by Max-SAT-equivalence-preserving inference rules. As the max-resolution is incomplete for the inference in Max-SAT, we propose a new proof system as well as an algorithm allowing to infer, if possible, a given clause or formula.
Dans cette thèse, on s'intéresse au problème de satisfiabilité maximum, ou problème Max-SAT, qui consiste, étant donnée une formule propositionnelle sous forme normale conjonctive, à trouver une interprétation des variables de la formule permettant de satisfaire le plus de clauses possible, ou, de manière équivalente, de falsifier le moins de clauses possible. Le système de preuve le plus utilisé dans Max-SAT est basé sur la règle d'inférence par max-résolution qui est l'adaptation pour Max-SAT de la règle de résolution utilisée pour le problème SAT. La règle de résolution déduit une nouvelle clause à partir de deux clauses qui s'opposent, ce qui permet notamment de certifier qu'une formule est insatisfiable en déduisant progressivement de nouvelles clauses jusqu'à en déduire une contradiction, représentée sous la forme d'une clause vide (on parle alors de réfutation par résolution). L'adaptation des réfutations par résolution pour Max-SAT sans en augmenter considérablement la taille est un problème ouvert depuis l'introduction de la max-résolution. On propose dans cette thèse deux méthodes pour adapter n'importe quelle réfutation par résolution en réfutation valide pour Max-SAT, à laquelle on se réfère sous le terme max-réfutation. Une autre contribution de cette thèse est la construction de certificats qui permettent de démontrer l'optimalité d'une solution pour le problème Max-SAT. Pour générer de tels certificats, on utilise les max-réfutations que l'on est désormais capables de générer à partir des réfutations par résolution. Comme une max-réfutation permet de certifier qu'au moins une clause d'une formule doit être falsifiée, il est alors possible de certifier, en utilisant k max-réfutations, qu'au moins k clauses de cette même formule doivent être falsifiées. Cette séquence de max-réfutations, à laquelle on ajoute une interprétation des variables permettant de falsifier exactement k clauses de la formule, forme un certificat pour le problème Max-SAT. Enfin, on s'intéresse au problème qui consiste, étant donnée une formule initiale et une information donnée (clause ou formule), à inférer cette information par des règles d'inférence qui préservent l'équivalence Max-SAT. Comme la max-résolution est incomplète pour l'inférence dans Max-SAT, on propose un nouveau système de preuve ainsi qu'un algorithme permettant de construire n'importe quelle inférence de clauses ou de formules, ou de certifier qu'une telle inférence ne peut exister.
Fichier principal
Vignette du fichier
Manuscrit_de_these.pdf (1.16 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Licence : CC BY NC ND - Paternité - Pas d'utilisation commerciale - Pas de modification

Dates et versions

tel-03977443 , version 1 (07-02-2023)

Identifiants

  • HAL Id : tel-03977443 , version 1

Citer

Matthieu Py. Inférence et certificats pour le problème de satisfiabilité maximum. Informatique [cs]. Université d'Aix-Marseille (AMU), 2021. Français. ⟨NNT : 2021AIXM0631⟩. ⟨tel-03977443⟩
44 Consultations
71 Téléchargements

Partager

Gmail Facebook X LinkedIn More