Maximum satisfiability problem
The maximum satisfiability problem, usually abbreviated MAX-SAT, is an optimization form of the Boolean satisfiability problem. An instance consists of a Boolean formula expressed in conjunctive normal form, together with the objective of finding an assignment that satisfies the largest possible number of its clauses. Whereas ordinary satisfiability asks whether every clause can be satisfied simultaneously, MAX-SAT assigns a numerical optimum even when the formula is inconsistent.
The problem occupies a central position in the study of combinatorial optimization. Its restricted forms capture several standard optimization problems, while its weighted and partial forms provide direct representations of constraint systems containing preferences, penalties, and requirements of unequal importance.
Mathematical formulation
Let
[ F=C_1\land C_2\land\cdots\land C_m ]
be a conjunctive-normal-form formula over Boolean variables (x_1,\ldots,x_n). Each clause (C_i) is a disjunction of literals, where a literal is either a variable or its negation. For an assignment (\alpha), the unweighted MAX-SAT objective is
[ \operatorname{sat}F(\alpha) =\sum{i=1}^{m}\mathbf{1}[C_i(\alpha)=\mathrm{true}], ]
where the indicator contributes one precisely when the corresponding clause is satisfied. The optimum is therefore
[ \operatorname{OPT}(F) =\max_{\alpha\in{0,1}^{n}}\operatorname{sat}_F(\alpha). ]
Clauses are treated as members of a multiset, so repeated clauses make separate contributions to the objective. An empty clause is never satisfied and consequently contributes a fixed amount to the unavoidable cost.
An equivalent minimization formulation counts falsified clauses:
[ \operatorname{cost}_F(\alpha) =m-\operatorname{sat}_F(\alpha). ]
This form is often called Min-UNSAT. It also permits an interpretation in terms of clause deletion: the minimum cost equals the smallest number of clauses whose removal leaves a satisfiable formula. This interpretation concerns deletion of constraints rather than the Hamming distance between assignments.
The associated decision problem receives an integer threshold (k) and asks whether at least (k) clauses can be satisfied. Membership in NP follows because an assignment and its objective value can be checked in polynomial time. Ordinary SAT reduces to this decision problem by setting (k=m), so the decision form is NP-complete, while the optimization form is NP-hard.
Principal variants
In weighted MAX-SAT, every clause (C_i) has a nonnegative weight (w_i), and the objective becomes
[ \max_{\alpha}\sum_{i=1}^{m}w_i\mathbf{1}[C_i(\alpha)=\mathrm{true}]. ]
Integer weights can represent repeated clauses compactly, although arbitrary weights also support penalty models that do not arise naturally through duplication. The complementary minimization objective is the total weight of the falsified clauses.
Partial MAX-SAT separates the formula into hard clauses and soft clauses. Every feasible assignment must satisfy all hard clauses, while optimization applies only to the soft clauses. An instance with inconsistent hard clauses has no feasible assignment, independently of the soft-clause objective. Weighted partial MAX-SAT combines this distinction with weights on the soft clauses and is frequently represented as a pseudo-Boolean optimization problem.
Restriction by clause length produces several distinct complexity classes. MAX-2-SAT permits no more than two literals in each clause and remains NP-hard, despite ordinary 2-satisfiability being solvable in polynomial time. By contrast, clauses containing at most one literal yield an elementary optimization problem whose conflicts occur only between positive and negative occurrences of the same variable.
MAX-3-SAT restricts clauses to at most three literals. A related promise form, often called E3-MAX-SAT, requires every clause to contain exactly three distinct literals. The distinction matters in approximation analysis because unit clauses and binary clauses have different satisfaction probabilities from clauses of length three.
Approximation structure
A uniformly random assignment satisfies a clause of length (\ell) with probability
[ 1-2^{-\ell}. ]
Consequently, every nonempty clause is satisfied with probability at least one half, and linearity of expectation gives an expected objective value of at least half the total clause weight. The argument does not require independence among the events that different clauses are satisfied. Its randomized construction can be converted into a deterministic approximation algorithm through the method of conditional expectation.
A stronger general guarantee follows from a linear programming relaxation. Fractional variables represent marginal truth values, while a fractional clause variable is bounded by the sum of the fractional values of its literals. Independent randomized rounding satisfies a clause with probability equal to one minus the product of the probabilities that all its literals are false. Comparing this probability with the fractional clause value produces an approximation ratio of
[ 1-\frac{1}{e}. ]
This analysis applies to nonnegative clause weights because both the relaxation and the expectation are linear in those weights. More elaborate rounding methods exploit clause length and correlations between variables, but the linear relaxation exposes the basic relationship between fractional coverage and Boolean satisfaction.
For E3-MAX-SAT, a uniformly random assignment satisfies each clause with probability (7/8). The resulting expected ratio is exact for the natural random-assignment analysis. Johan Håstad’s work on probabilistically checkable proofs established that, for every fixed (\varepsilon>0), distinguishing satisfiable instances from instances whose optimum is at most a (7/8+\varepsilon) fraction of all clauses is NP-hard. Thus, subject to (P\ne NP), the elementary probability (7/8) also marks the approximation threshold for this promise setting.
Early systematic approximation analyses by David S. Johnson treated MAX-SAT within a broader class of discrete optimization problems. Later results connected its approximation thresholds to the algebraic tests used in PCP constructions, thereby relating local clause predicates to global limits on polynomial-time approximation.
Exact optimization
Exact MAX-SAT methods generally maintain both a feasible objective value and a bound on the best value still attainable in an unexplored region of the assignment space. In a branch-and-bound formulation, branching fixes a variable, simplifies affected clauses, and divides the remaining assignments between two subproblems. A branch terminates when its upper bound cannot exceed the best complete assignment already found.
The minimization view supports lower bounds on the number or weight of clauses that must remain false. A collection of pairwise clause-disjoint inconsistent subformulas forces at least one falsified clause from each member of the collection. Because the collections share no clauses, their separate contributions can be added without counting the same unavoidable violation twice.
The systematic incorporation of this packing argument into MAX-SAT branch-and-bound analysis was formalized by You Watanabe in 1995. Her formulation extracted disjoint contradictions generated by unit propagation and converted their total weight into a lower bound for the current search node. The rule preserved exactness because it altered neither the assignments represented by the node nor the objective values of complete assignments; it only certified a minimum cost that every such assignment incurred.
Clause learning extends the same general principle by recording implications derived from conflicts. In a pure satisfiability solver, a learned clause prevents repetition of an inconsistent partial assignment. In a MAX-SAT solver, the derivation must additionally preserve the optimum or account explicitly for the cost of relaxing the conflicting clauses. Max-SAT resolution supplies inference rules designed for this objective-preserving transformation.
SAT-based and core-guided formulations
A MAX-SAT instance can be reduced to a sequence of ordinary SAT queries by introducing a relaxation variable (r_i) for each soft clause:
[ C_i\lor r_i. ]
Setting (r_i) to true permits the associated clause to be violated. A cardinality constraint then limits the number of enabled relaxation variables. In the unweighted case, the condition
[ \sum_i r_i\leq b ]
asks whether an assignment exists that falsifies at most (b) soft clauses. Encodings based on sorting networks, sequential counters, or totalizers translate this bound into conjunctive normal form, after which successive SAT calls determine the smallest feasible value of (b).
Core-guided algorithms instead begin with a bound that permits no soft-clause violations. When the resulting formula is unsatisfiable, the SAT solver returns an unsatisfiable core, which is a subset of clauses that cannot all hold simultaneously. Relaxation variables are then attached to selected soft clauses in the core, together with a constraint requiring the search to account for at least one violation. Repeated cores progressively expose the portion of the objective responsible for inconsistency.
Weighted instances require the core calculation to respect unequal penalties. A standard transformation splits weights so that the minimum weight represented in a core is charged once, while any residual weight remains associated with additional copies or derived constraints. The resulting procedure can be interpreted as a dual process: each core certifies an unavoidable cost, while each feasible assignment supplies an upper bound on the minimum falsified weight.
Applications as a representation language
MAX-SAT serves as a representation language whenever Boolean requirements admit controlled violation. In constraint satisfaction, hard clauses encode conditions that define feasibility, while soft clauses measure departures from preferred configurations. Weighted clauses translate those departures into an additive objective, making the logical model compatible with standard optimization criteria.
The same representation supports discrete inference when candidate decisions are Boolean and local interactions can be written as clauses. The optimum then identifies an assignment with minimum aggregate penalty rather than asserting that the original constraints are jointly consistent. This distinction is significant in noisy or overconstrained models because ordinary satisfiability reports only the absence of a fully satisfying assignment, whereas MAX-SAT quantifies the least remaining inconsistency.