= Integer programming formulation of satisfiability
{title2=$\sum_{\ell\in C_i}L_\ell(t)\geq1$}
Encode each truth value by $t_k\in\{0,1\}$. A positive <Boolean literal> has value $t_k$ and its negation has value $1-t_k$. The sum of literal values in a clause is at least one exactly when that clause is true. Thus the displayed inequalities, with objective zero, express <Boolean satisfiability> as a binary <integer programming> feasibility problem. For <maximum satisfiability>, introduce $q_i\in\{0,1\}$ with $q_i\leq\sum_{\ell\in C_i}L_\ell(t)$ and maximize $\sum_iq_i$. False clauses force zero indicators; true clauses permit indicators one, and maximization selects all of them. Hence the optimal objective equals the maximum number of true clauses.
Back to article page
