Maximum satisfiability (${\max }_t\#\{\text{clauses true under }t\}$)

Maximum satisfiability asks for a truth assignment maximizing the number of true clauses of a conjunctive normal form formula. The Boolean satisfiability problem asks whether all its clauses can be made true. Binary clause indicators give an integer programming formulation, and the literal-frequency greedy approximation for MAX-SAT guarantees at least half the optimum. Counts of clauses, rather than multiplicities of repeated literals within one clause, are relevant to this objective.

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\ge N_{+}/2\ge \mathrm{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.