随机算法 (Fall 2011)/Max-SAT

From EtoneWiki
Jump to: navigation, search

MAX-SAT

Suppose that we have a number of boolean variables . A literal is either a variable itself or its negation . A logic expression is a conjunctive normal form (CNF) if it is written as the conjunction(AND) of a set of clauses, where each clause is a disjunction(OR) of literals. For example:

The satisfiability (SAT) problem is that given as input a CNF formula decide whether the CNF is satisfiable, i.e. there exists an assignment of variables to the values of true and false so that all clauses are true. SAT is the first problem known to be NP-complete (the Cook-Levin theorem).

We consider the the optimization version of SAT, which ask for an assignment that the number of satisfied clauses is maximized.

Problem (MAX-SAT)
Given a conjunctive normal form (CNF) formula of clauses defined on boolean variables , find a truth assignment to the boolean variables that maximizes the number of satisfied clauses.

The Probabilistic Method

A straightforward way to solve Max-SAT is to uniformly and independently assign each variable a random truth assignment. The following theorem is proved by the probabilistic method.

Theorem
For any set of clauses, there is a truth assignment that satisfies at least clauses.
Proof.
For each variable, independently assign a random value in with equal probability. For the th clause, let be the random variable which indicates whether the th clause is satisfied. Suppose that there are literals in the clause. The probability that the clause is satisfied is
.

Let be the number of satisfied clauses. By the linearity of expectation,

Therefore, there exists an assignment such that at least clauses are satisfied.

Note that this gives a randomized algorithm which returns a truth assignment satisfying at least clauses in expectation. There are totally clauses, thus the optimal solution is at most , which means that this simple randomized algorithm is a -approximation algorithm for the MAX-CUT problem.

LP Relaxation + Randomized Rounding

For a clause , let be the set of indices of the variables that appear in the uncomplemented form in clause , and let be the set of indices of the variables that appear in the complemented form in clause . The Max-SAT problem can be formulated as the following integer linear programing.

Each in the programing indicates the truth assignment to the variable , and each indicates whether the claus is satisfied. The inequalities ensure that a clause is deemed to be true only if at least one of the literals in the clause is assigned the value 1.

The integer linear programming is relaxed to the following linear programming:

Let and be the fractional optimal solutions to the above linear programming. Clearly, is an upper bound on the optimal number of satisfied clauses, i.e. we have

.

Apply a very natural randomized rounding scheme. For each , independently

Correspondingly, each is assigned to TRUE independently with probability .

Lemma
Let be a clause with literals. The probability that it is satisfied by randomized rounding is at least
.
Proof.
Without loss of generality, we assume that all variables appear in in the uncomplemented form, and we assume that
.

The complemented cases are symmetric.

Clause remains unsatisfied by randomized rounding only if every one of , , is assigned to FALSE, which corresponds to that every one of , , is rounded to 0. This event occurs with probability . Therefore, the clause is satisfied by the randomized rounding with probability

.

By the linear programming constraints,

.

Then the value of is minimized when all are equal and . Thus, the probability that is satisfied is

,

where the last inequality is due to the concaveness of the function of variable .

For any , it holds that . Therefore, by the linearity of expectation, the expected number of satisfied clauses by the randomized rounding, is at least

.

The inequality is due to the fact that are the optimal fractional solutions to the relaxed LP, thus are no worse than the optimal integral solutions.

Choose a better solution

For any instance of the Max-SAT, let be the expected number of satisfied clauses when each variable is independently set to TRUE with probability ; and let be the expected number of satisfied clauses when we use the linear programming followed by randomized rounding.

We will show that on any instance of the Max-SAT, one of the two algorithms is a -approximation algorithm.

Theorem
Proof.
It suffices to show that . Letting denote the set of clauses that contain literals, we know that

By the analysis of randomized rounding,

Thus

An easy calculation shows that for any , so that we have