3-SAT

3-SAT is a variant of the satisfiability problem of propositional logic (from English satisfiability , SAT for short ).

It deals with the question of whether in conjunctive normal form present propositional formula that most 3 literals per clause contains, can be fulfilled. An example of such a formula: ${\ displaystyle F}$

{\ displaystyle F = ({\ overline {x_ {1}}} \ vee x_ ​​{2} \ vee x_ ​​{3}) \ wedge (x_ {2} \ vee {\ overline {x_ {3}}} \ vee x_ {4}) \ wedge (x_ {1} \ vee {\ overline {x_ {2}}})}

We are now looking for an assignment of variables up to with 0 or 1, for which F takes the value 1 (true). If there is such an assignment, F can be fulfilled, otherwise not. As with all NP-complete problems, it is “easy” to check a candidate for a solution for its validity, ie to determine whether a given assignment of the variable fulfills the formula. Finding a valid solution candidate is generally "difficult", since no method is known today to find a satisfactory assignment in polynomial time. ${\ displaystyle x_ {1}}$ ${\ displaystyle x_ {4}}$

All k -SAT problems for are NP-complete, 2-SAT is the complexity class NL , 1-SAT is the complexity class L . ${\ displaystyle k \ geq 3}$

The general satisfiability problem of propositional logic (SAT) can be reduced to 3-SAT polynomially , and thus 3-SAT is NP-complete by Cook's Theorem .

3-SAT can in turn u. a. reduce polynomially to the clique problem , the backpack problem and the directed Hamiltonian circle (DHC) , whereby these problems are also proven to be NP-difficult .

variants

Exact-3-SAT

Sometimes the definition of 3-SAT also requires that the clauses contain exactly three literals. This variant of the problem is also NP-complete, even if one additionally demands that all literals in a clause are different.

Max-3-SAT

It is not required here that every clause be true, but as many of them as possible. Even a random assignment of the variable yields the expected value that 7/8 of the clauses are fulfilled (because the probability that a certain clause is not fulfilled is only (1/2) ^ 3 - provided that literals are not multiple in a clause occur). The consequence of this is that every such 3-SAT problem can be fulfilled with fewer than 8 clauses.
Max-3-SAT is also NP-complete, since the reduction to the normal 3-SAT only consists in asking whether the total number of clauses can be fulfilled.

Not-All-Equal-3-SAT

It is 3-SAT, but only one assignment is accepted that results in at least one false and one true literal in each clause. Not-All-Equal-3-SAT is also NP-complete.

literature

Schöning, Uwe : Race for the fastest SAT algorithm ( GZIP ; 78 kB)
Jon Kleinberg , Éva Tardos . Algorithm design. Pearson International Edition, 2006. ISBN 0-321-37291-3 . Pages 724ff (MAX-3-SAT)