3-Satisfiability Decision Problem

Definition

3-Satisfiability Problem

The 3-SAT problem is a specific form of the SAT where every clause consists of exactly 3 literals, where every literal is bound to a different variable.

Example:

Note: Sometimes, 3-SAT refers to the sub-problem of SAT where each clause has at most 3 literals.

Trivial Exponential Barrier

Problems in P can be solved in polynomial time

where is the input size.

For NP-complete problems, no polynomial-time algorithm is known. Examples include SAT, 3-SAT, independent set, 3-colouring, and vertex cover.

The basic deterministic way to solve such problems is exhaustive search. For a Boolean formula with variables, try all truth assignments. This gives a running time of about

up to the cost of checking each assignment. For problems with three choices per variable or object, a similarly trivial search may give

These bounds are encoding-dependent because is the input size under the chosen encoding.

For 3-SAT, the trivial branching algorithm assigns one variable at a time. Each variable gives two branches: true and false. This produces a full binary search tree of depth and hence leaves.

The exact-algorithm question is whether one can break this trivial exponential barrier. For 3-SAT, one can do better than by branching more carefully than simply choosing an arbitrary unassigned variable.

Breaking the Exponential Barrier

The basic branching algorithm chooses one variable and creates two subinstances. For 3-SAT, one can branch on a whole clause instead.

Let be a clause. Since this is 3-SAT, contains at most three literals, and these literals use distinct variables.

• If has one literal, then it is a unit clause. Unit propagation fixes that literal.
• If has two literals over variables , then there are only three satisfying assignments for .
• If has three literals over variables , then there are only seven satisfying assignments for .

Thus one branching step removes , , or variables and creates at most , , or subinstances, respectively. The numbers come from excluding the assignments that do not satisfy the chosen clause:

• a unit clause has satisfying assignment;
• a 2-literal clause has satisfying assignments;
• a 3-literal clause has satisfying assignments.

Let be the number of variables assigned in branches on clauses of size , and let be the number of variables assigned in branches on clauses of size .

A branch on a 3-literal clause assigns 3 variables and creates at most 7 subinstances. Thus such assigned variables correspond to branching steps, contributing a factor .

Variables counted by

If the algorithm branches on four 3-literal clauses, then it assigns variables through such branches. Hence , and these branches contribute

leaves.

A branch on a 2-literal clause assigns 2 variables and creates at most 3 subinstances. Thus such assigned variables correspond to branching steps, contributing a factor .

Variables counted by

If the algorithm branches on five 2-literal clauses, then it assigns variables through such branches. Hence , and these branches contribute

leaves.

Multiplying the two contributions, the number of leaves is at most

Since , this is bounded by

So 3-SAT can be solved exactly and deterministically in time

where is the number of variables. This already breaks the trivial branching bound.

The O-star notation suppresses polynomial factors. Thus means for some constant .