We know that SAT is NP-complete so it is unlikely that we’ll find a polynomial-time algorithm to solve it. Can we approximately solve it? Let’s first look at the optimization version of SAT so that we are always outputting something. Here is the definition of the Max-SAT problem:
Input: Boolean formula in CNF with variables and clauses
Output: assignment maximizing the number of clauses satisfied.
Setting satisfies 4 of the 5 clauses, and there is no assignment satisfying all 5.
Clearly, SAT and hence Max-SAT is NP-hard. Therefore we cannot hope to efficiently find an optimal assignment. Can we find an approximately optimal solution? In particular, for an input formula let denote the maximum number of satisfied clauses. In the above example, and .
Can we construct an algorithm A which finds an assignment satisfying clauses where ? And it achieves this guarantee of being within a factor of optimal for every input . We call A a -approximation algorithm.
We will first see a very simple randomized algorithm which is a -approximation algorithm for Max-SAT. Then we will use linear programming to construct a -approximation algorithm. Finally, by combining these two algorithms we’ll achieve a -approximation algorithm.
First we give a very simple algorithm for Max-SAT. The algorithm sets each variable to be True independently with probability 1/2 and False with probability 1/2. I then outputs the resulting assignment. Since this is a randomized algorithm we look at its “expected”
Let be the number of satisfied clauses. Also, for , let
It is easy to see that . By linearity of expectation
Consider a clause with variables,
It follows that the simple algorithm satisfies half of the clauses in expectation (regardless of the max # of clauses satisfiable). Moreover, if there are exactly literals in every clause, then it satisfies clauses.
Integer Linear Programing
Integer Linear Programming (ILP) is a linear program where the variables are restricted to integer values.
First we show that ILP is NP-hard by reducing Max SAT -> ILP as follows.
Consider input for Max SAT with variables & clauses .
For variable in SAT input , create variable for our ILP instance. Restrict where corresponds to and corresponds to .
For clause , create variable where corresponds to satisfied corresponds to unsatisfied
Further, let variables in in positive form, and variables in in negative form. For example, if . Create a constraint
for each clause .
Finally, the ILP maximizes
Solving this ILP will give a solution to Max SAT.
To see this, note that for the constraint
to get we need at least 1 positive literal having &/or at least 1 negative literal with . Also, since we maximize we’ll set = 1 if possible.
Consider the following LP which changes constraints of the form to
max subject to:
This is a LP so we can solve it in poly-time.
This is a “relaxation” of the original ILP in the following sense: any solution to the ILP is also a solution to the LP
Hence, objective value for optimal of ILP is less than or equal to objective value for optimal of LP
where is optimal solution for the LP.
We want to then create a solution for the ILP which is close to the optimal for the ILP. How do we measure close to the ILP optimal? By saying it’s close to the LP optimal.
Take . Set
This method is called randomized rounding.
Let’s look at expected # of satisfied clauses.
Lemma: For clause with literals, is satisified)
Assuming the lemma, we show that the algorithm gives a constant approximation factor.
Note, for since
Hence, for .
Let = # of satisfied clauses.
where has variables.
Recall, the most optimal # of satisfied clauses
So in expectation we satisfy times the maximum # of satisfied clauses.
This is a – expected approximation algorithm, and we can find such an assignment using the method of conditional expectations.
Proof of lemma: Fix . We may assume that all of the variables in are in positive form, so say
The LP constraint is then:
Clause is unsatisfied if every for is rounded to 0.
This happens with probability
Recall the arithmetic mean-geometric mean inequality AM – FM
In our case
since from (*) on last page.
so is concave
To show for all we just need to check at and .
is satisfied) = by AM – GM
Recall, our old algorithm achieves on clauses of size & this new algolrithm achieves
The new algorithm is better for and the old algorithm is better for
Best of Two Algorithm:
Better approach: run both algorithms and take the better of the 2 solutions.
Let = expected number of clauses satisfied by old algorithm and = expected number for new algorithm
In other words, we have a – approximation algorithm.
(can use method of conditional expectation to derandomize)
So it suffices to show
Let = set of clauses with literals.
Need to show: for all .