Max-SAT random approximation algorithm

This is a naïve approximate solution to the Max-SAT problem. If the formula has variables and clauses this guarantees clauses will be satisfied by the assignment.

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.

Run time

We loop times having to look through a list of size at most . Therefore this takes .

Correctness

We show this by induction on the number of variables.

If we have a single variable, then all clauses are either or as we assume each variable only appears in a single literal in each clause. By picking the larger set of either or we guarantee our assignment satisfies more than half these clauses.

Assume we have proven that on variables our algorithm satisfies more than clauses.

Suppose we have formula with variables. Let be the set of all clauses that use only . Remove all literals from that involve to make with clauses.

Similarly to case there is an assignment that satisfies at least clauses as they just involve .

When we run our algorithm on we get an assignment that satisfies .

The steps that return this assignment are identical to that of running it on the first variables of . Therefore for .

In the last step we consider , we pick that maximises the number of left over unsatisfied clauses. This includes the clauses in where satisfies at least , therefore satisfies new clauses - as it is maximal.

Therefore the assignment satisfies

clauses and we have proved the induction case for .