= Literal-frequency greedy approximation for MAX-SAT
{title2=$G\geq\operatorname{OPT}/2$}
In the residual unsatisfied formula, choose a <Boolean literal> contained in the largest number $a$ of clauses and make it true. Its opposite occurs in at most $a$ clauses, since it too was an eligible literal. The step permanently satisfies $a$ clauses; only clauses containing the opposite can become empty, so it loses at most $a$ clauses. Delete satisfied clauses and false literals and repeat. No satisfied clause or newly empty clause is counted twice. Summing gives total lost nonempty clauses at most total satisfied clauses $G$. All initially nonempty clauses are eventually in one of these classes, so $G\geq N_+/2\geq\operatorname{OPT}/2$. Initial empty clauses can never be satisfied and are excluded from $N_+$. This proves the <approximation algorithm> guarantee even with tautological clauses or repeated literals.
Back to article page
