Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Maximum satisfiability problem
Résumé
In computational complexity theory, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. It is a generalization of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.
The conjunctive normal form formula
is not satisfiable: no matter which truth values are assigned to its two variables, at least one of its four clauses will be false.
However, it is possible to assign truth values in such a way as to make three out of four clauses true; indeed, every truth assignment will do this.
Therefore, if this formula is given as an instance of the MAX-SAT problem, the solution to the problem is the number three.
The MAX-SAT problem is OptP-complete, and thus NP-hard, since its solution easily leads to the solution of the boolean satisfiability problem, which is NP-complete.
It is also difficult to find an approximate solution of the problem, that satisfies a number of clauses within a guaranteed approximation ratio of the optimal solution. More precisely, the problem is APX-complete, and thus does not admit a polynomial-time approximation scheme unless P = NP.
More generally, one can define a weighted version of MAX-SAT as follows: given a conjunctive normal form formula with non-negative weights assigned to each clause, find truth values for its variables that maximize the combined weight of the satisfied clauses. The MAX-SAT problem is an instance of weighted MAX-SAT where all weights are 1.
Randomly assigning each variable to be true with probability 1/2 gives an expected 2-approximation. More precisely, if each clause has at least variables, then this yields a (1 − 2−)-approximation. This algorithm can be derandomized using the method of conditional probabilities.
MAX-SAT can also be expressed using an integer linear program (ILP). Fix a conjunctive normal form formula with variables 1, 2, .
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.