= Maximum satisfiability
{title2=$\max_t\#\{\text{clauses true under }t\}$}
= MAX-SAT
{c}
{synonym}
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.
Back to article page
