Inference and certificates for the maximum satisfiability problem

Dans cette thèse, on s'intéresse au problème de satisfiabilité maximum (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. 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, ce qui permet de certifier qu'une formule est insatisfiable en déduisant de nouvelles clauses jusqu'à en déduire une contradiction, représentée par la clause vide (on parle de réfutation par résolution). L'adaptation des réfutations par résolution en réfutations valides pour Max-SAT (appelées max-réfutations) sans en augmenter considérablement la taille est un problème ouvert depuis l'introduction de la max-résolution. On propose ici deux méthodes pour adapter n'importe quelle réfutation par résolution en max-réfutation. Une autre contribution est la construction de certificats qui permettent de démontrer l'optimalité d'une solution pour le problème Max-SAT, générés en utilisant les max-réfutations calculées à partir des réfutations par résolution. Enfin, on s'intéresse à comment inférer, à partir d'une formule initiale, une information donnée (clause ou formule) par des règles d'inférence qui préservent l'équivalence Max-SAT. On propose alors 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 existerIn this thesis, we are interested in the maximum satisfiability problem (Max-SAT), 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. 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. 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 formul