Maximum Satisfiability

Abstract

The Boolean satisfiability problem (SAT) is the problem of deciding, given a Boolean expression in variables x 1 , · · · , x n , whether some assignment of the variables makes the expression true. SAT is historically notable because it was the first problem proven to be NP-complete. (Before this point, the idea of NP-completeness had been formulated, but no one had proven that there actually existed any NP-complete problems.) We will consider not arbitrary Boolean expressions but only expressions in conjunctive normal form (CNF), i.e. of the form ((A 11 ∨ A 12 ∨ · · ·) ∧ (A 21 ∨ A 22 ∨ · · ·) ∧ · · ·) where each literal A ij is either a single variable or its negation, and each clause does not contain more than one literal associated with a single variable. In the MAX-SAT variation of SAT, we do not require that all the disjunctive clauses be satisfied. Instead, we want find an assignment which maximizes the number of satisfied clauses.