Maximal Satisfiability

The objective function is given by reformulating the statement of the problem - we want to minimize the number of clauses that are not true.

Recall that the Boolean expression is in CNF, so a clause is satisfied if and only if it contains at least one true literal.

Representing the problem as a sequence of decisions.  There are (at least) two ways:
    1.  List all the literals in some order, l1, l2, l3, etc.  At the i-th stage of the algorithm, decide whether li is True or False
    2.  List all the clauses in some order,  c1, c2, c3, etc.  At the i-th stage of the algorithm, choose a literal in ci and assign it the value True or False (if any of ci's literals are still unassigned).  If ci is now satisfied, or if ci contains no more unassigned literals, move on to ci+1.

Let's think about Method 2.  (Method 1 is much simpler, so we should learn more by studying Method 2.)

Global upper bound:  Note that we can always satisfy at least 1 clause.  Therefore if n is the number of clauses, n-1 is a valid initial value for the global upper bound on the number of unsatisfied clauses.  Actually, I think it is true that we can always satisfy at least n/2 of the clauses, but I don't have a proof of this so I'll stick with n-1 as the initial upper bound.  Actually, I think I see a way to prove that n/2 idea using induction on the maximum number of literals in any of the clauses ....

Ok, back to the problem at hand.

Lower bound function:  Let S be a partial solution, in which we have already dealt with clauses c1, c2, ..., ci, and we are in the process of dealing with ci+1.  Some of these clauses we may have been able to satisfy, and some we may not (all of their literals may have already been assigned the value False).  These unsatisfied clauses will still be unsatisfied in any solution that expands on S, so clearly the lower bound on the best solution expanding on S should include the number of clauses not satisfied so far.  Can we do better?  Of course we can.  We can scan the clauses that still remain to be resolved (ci+1, ci+2, ... cn) - if any of them contain only literals that have already been assigned the value False, then we will not be able to satisfy them when we reach them (this is similar to the knapsack problem in which we looked ahead at the remaining items and ruled out those which were too big to fit in the remaining knapsack space - our past choices limit our future options).

So we can define L(S) = "number of clauses among {c1, c2, ... ci} that are not satisfied" + "number of clauses among {ci+1, ... cn} that cannot be satisfied because all their literals have already been assigned False"

Upper bound function: Let S be defined as above.  Certainly the upper bound function must contain all the costs accumulated so far (i.e. 1 point for each clause among {c1, ... ci} that is not satisfied).  Pessimistically, we might consider the possibility that none of the remaining n-i clauses will be satisfied.  This is certainly a valid upper bound, and would give us U(S) = "number of clauses among {c1, c2, ... ci} that are not satisfied" + n - i

But remember that any solution gives a valid upper bound on the best solution - so we can try to improve on the pessimistic estimate by going through the remaining clauses in order and in each one where we can, pick an unassigned literal and assign it the value True.  This is quick and easy, and as long as we propagate the assignments forward through the rest of the clauses we will not get into trouble.  If we want to be a bit more sophisticated, we can count the number of times each unassigned literal appears in the remaining clauses and assign the most frequent literal the value True - this will satisfy as many clauses as possible with one assignment.  We can then apply the same idea to any clauses that are still unresolved, and so on until we have constructed a complete assignment.  This is of course nothing more than a Greedy heuristic, and while we cannot expect it to give us the optimal solution, we can at least hope that it gives us a fairly good one.

So we can define U(S) = "number of clauses among {c1, c2, ... ci} that are not satisfied" + "number of clauses among {ci+1, ... cn} that remain unsatisfied after we apply the Greedy heuristic"

That's it, we don't need anything else.