 Maximum satisfiability

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.