Week 12 - Max-SAT approximation algorithm

In this lecture we consider the a similar problem to the SAT problem.

Statement

Max-Satisfiability Problem (Max-SAT problem)

Provided with a boolean function in CNF with variables and clauses, where each variable only appears in a single literal in each clause. What is an assignment maximising the number of satisfied clauses?

Link to original

This is NP-hard.

Max-SAT is NP-hard

Statement

Lemma

Max-SAT is NP-hard

Proof

There is a many-one reduction from the SAT problem to max-SAT.

If we have an instance of the SAT problem plug it into max-SAT and if we get an assignment the satisfies all clauses return that, otherwise say no.

As SAT is NP-complete this gives that max-SAT is NP-hard.

Link to original

Therefore it is unlikely to find any algorithm that will solve the problem quickly. However we will look at using linear programming to approximate a solution.

Approximate algorithms

Let be a boolean function in CNF with clauses. Let denote the solution to the max-SAT problem for .

We want to construct an algorithm the on an input outputs where , this will be referred to as a -approximation algorithm.

Simple half-approximation algorithm

Suppose we have with variables for and clauses for .

Make random assignment

lets look at how many clauses this satisfies . We have expectation

however it will be easier to break it down further. Let

so we have

Suppose has literals that use distinct variables. For any literal, given our assignment, its probability of being true is . For to be true we just need one of these literals to be true. We have,

In summary we have

though this is in expectation - which means there is an assignment that has more than clauses satisfied.

We can in fact find this pretty easily.

Pseudocode

Name(f):
	Input: Boolean formula in CNF form f, with variables x_i and clauses c_j.
	Output: An assignment to x_i that satisified m/2 clauses.
1. Let C be the set of clauses and build assignment a : x_i |-> T/F.
2. For each x_i:
	1. Let A be all the clauses in C containing the x_i literal.
	2. Let B be all the clauses in C containing the not x_i literal.
	3. If A is bigger than or equal to B, set a(x_i) = T and remove A from C.
	4. Else set a(x_i) = F and remove B from C.
3. Return assignment a.

Link to original

A version of this algorithm works even better on the following problem.

Statement

Max- -exact-satisfiability problem

Provided with a boolean function in CNF with variables and clauses, where each variable only appears in a single literal in each clause and each clause has exactly litterals. What is an assignment maximising the number of satisfied clauses?

Link to original

If we calculate this expectation more exactly we can get clauses are satisfied.

For the case of it has been shown that doing any better than a -approximation algorithm is NP-hard.

Integer linear programming

Statement

Linear programme problem

Given a linear programme what is an that achieves an optimal solution if it exists.

Link to original

We can use Max-SAT to show this version of linear programming is NP-hard.

Integer linear programming is NP-hard

Statement

Lemma

integer linear programming is NP-hard.

Proof

We are going to find a Many-one reduction of Max-SAT to integer linear programming (ILP). Which as Max-SAT is NP-hard will give us integer linear programming is too.

Suppose we have an instance of the Max-SAT problem given by . Design an ILP with the variables for each variable in (with ) and for each clause in (with ).

Now add the following constraints,

this will relate to the variables and clauses being true or false.

To add constraints to reflect the clauses suppose contains positive literals involving variables and negative literals . So we have the clause

For each clause add the following constraint

this guarantees for integer points can only be 1 if for some or for some .

Lastly to define the reduction, we need to define the objective function This reduction takes time , as we need to go through each clause to convert them into functionals. So this takes polynomial time.

When provided with a solution to the ILP return the solution to the Max-SAT problem with true for all and false for all . This takes time so takes polynomial time.

Let be the max value of the constructed ILP and be the max value of Max-SAT. From Claim 1 we have . Equally Claim 2 gives us . This provides that and we have the solution of the contracted ILP if and only if we have a solution to the Max-SAT problem.

Claim 1

Claim 1

An assignment to the variables of is reversed transformed into a feasible point in the contracted ILP and the value of its objective function is the number of satisfied clauses.

Proof of Claim 1

Set and , 1 if true and 0 if false. This satisfies the bounds on the variables and they are integers. The clause constraint

is satisfied as if there is a literal making true the corresponding value of or is 1 allowing to be 1.

The objective function is the number of satisfied clauses by definition.

Claim 2

Claim 2

A feasible point in the constructed ILP is transformed into a valid assignment of the variables and the value of the objective function is less than or equal to the number of satisfied clauses.

Proof of Claim 2

We set with being True and being False. The clause constraint

guarantees that if this assignment doesn’t satisfy then as and

Therefore

and we get the required statement.

Link to original

However, what if we run the constructed ILP in the proof but don’t require the points to be integers? We know Linear programming problem can be solved in polynomial time can we use this to get an approximate solution to the max-SAT problem?

LP relaxation for max-SAT

Let and be optimal solutions to the constructed ILP for max-SAT. Whereas let and be optimal solutions to the constructed ILP for max-SAT where we drop the need to be an Integer solution.

Note as and are less constrained we have Next we are going to transform the point and into an integer point by using a random algorithm again. Set

we call this randomized rounding.

Let be the number of satisfied clauses in this assignment, with . We want to look at the expectation of for this we will need the following lemma.

Lemma 1

Then we can look at the expectation of

Giving us a -approximation algorithm to the problem - in expectation.

Proof of Lemma 1

For this we are going to use the AM-GM inequality. Break down the clause by its positive and negative literals

Then lets look at

Here comes a little bit of horrible functional analysis. For a fixed we claim

for .

First if both sides equate to and we are done. So assume .

Note for they are equal.

With respect to we have the second derivative of left hand side is

Whereas the right hand side is linear with respect to . Therefore we have the inequality we desire.

So we can continue

where this last step comes from the Taylor expansion for

with gives us the inequality above.

This completes the proof of the lemma.

Summary of the approach

In abstract we did the following.

• Take an NP-hard problem,
• Reduce it to ILP,
• Relax to linear programming and solve, and
• Randomize round that solution.

This is a general approach we can take to finding approximation algorithms for NP-hard problems.

Comparison of approaches for max-Ek-SAT

k	Simple	LP-based
1
2
3
k

The thing to note here is that each row is at least , so by taking the max of both algorithms we achieve a -approximation algorithm in expectation.