Solution (source code)

= Solution

Use the usual nonempty-<clause> convention and normalize repeated <literals> within a <clause>; tautologies are always satisfied. If empty <clauses> are admitted, discard them first: they contribute nothing to any assignment or to the optimum. Let $m$ be the resulting number of <clause> occurrences.

Assign independent fair truth values. A singleton <clause> is satisfied with <probability> $1/2$, a proper two-variable <clause> with <probability> $3/4$, and a tautology with <probability> one. By <linearity of expectation>, the expected number satisfied is at least $m/2$, hence at least $\mathrm{OPT}/2$.

To derandomize, use the <method of conditional probabilities>. After some variables have been fixed, let $F$ be the conditional expected number of satisfied <clauses>. For the next variable the two <conditional expectations> $F_0,F_1$ satisfy $F=(F_0+F_1)/2$. Fix the value with the larger expectation. This never decreases $F$. When all variables have been fixed, $F$ is the actual integer number of satisfied <clauses>, so
$$
\boxed{\text{the algorithm satisfies at least }m/2\ge\mathrm{OPT}/2\text{ clauses}.}
$$
Compute each <conditional expectation> by summing the <probabilities> of the <clauses>. Each has at most two variables, so its contribution is computed in constant time; scanning all <clauses> for each variable gives $O(nm)$ arithmetic operations. This is a polynomial-time <approximation algorithm> with <approximation ratio> $1/2$.