Maximum satisfiability problem
The maximum satisfiability problem (commonly abbreviated as Max-SAT) is a fundamental optimization problem in computational complexity theory and artificial intelligence, where one is given a Boolean formula in conjunctive normal form (CNF)—a conjunction of clauses, each being a disjunction of literals (variables or their negations)—and the goal is to find a truth assignment to the variables that maximizes the number of satisfied clauses (those evaluating to true under the assignment). This unweighted version assumes each clause has equal importance, though it generalizes naturally to the weighted Max-SAT (Max-WSAT), where clauses carry nonnegative weights and the objective is to maximize the total weight of satisfied clauses.[1] Max-SAT extends the classic Boolean satisfiability problem (SAT), which is the decision variant asking whether there exists an assignment satisfying all clauses; SAT was the first problem proven NP-complete by Stephen Cook in 1971, establishing its central role in the theory of NP-completeness. Like SAT, Max-SAT is NP-hard, with the decision version—determining if at least k clauses can be satisfied—being NP-complete even for unweighted instances.[2] Its hardness holds for restricted cases, such as Max-2-SAT (clauses with at most two literals per clause), which remains NP-complete despite the polynomial solvability of 2-SAT.[1] Max-SAT is also APX-complete, meaning it admits polynomial-time approximation algorithms with a constant factor but lacks a polynomial-time approximation scheme (PTAS) unless P = NP.[2] Key variants of Max-SAT address practical needs in modeling: partial Max-SAT distinguishes hard clauses (which must all be satisfied) from soft clauses (to be maximized), while cardinality-constrained Max-SAT limits clause sizes or incorporates counting constraints.[2] These extensions enable encoding of real-world optimization tasks where full satisfiability is infeasible but partial solutions with quantifiable quality are valuable. Solving Max-SAT exactly is intractable for large instances due to its exponential worst-case complexity, leading to a rich body of algorithmic research. Exact solvers often leverage SAT solvers as NP-oracles within branch-and-bound frameworks, iteratively tightening upper and lower bounds on the optimal solution; notable examples include MSU3 (unsatisfiability-based upper bounding) and Open-WBO, which dominated the MaxSAT Evaluations from 2014 to 2016.[2] For approximation, early greedy heuristics by Johnson (1974) achieved a 1/2-approximation ratio, later improved to 3/4 by Yannakakis (1994) via linear programming relaxations and randomized rounding techniques refined by Goemans and Williamson (1994).[1] More recent local search and reactive methods continue to push practical performance, with inapproximability results showing that no algorithm can guarantee better than 7/8 for general Max-SAT unless P = NP. Beyond theory, Max-SAT finds applications in diverse domains requiring balanced decision-making under constraints, such as software package upgrades (maximizing compatible installations), error localization in C code (identifying minimal fault sets), and haplotype inference in bioinformatics (reconstructing genetic phases from pedigrees).[2] Its ability to model trade-offs via soft constraints has also driven advances in hardware design (e.g., VLSI circuit optimization) and knowledge representation in logic-based systems. Ongoing MaxSAT competitions benchmark solvers on industrial and crafted benchmarks, fostering progress in scalable optimization.[2]Fundamentals
Formal Definition
The maximum satisfiability problem (MAX-SAT) is defined over Boolean formulas in conjunctive normal form (CNF). A CNF formula \phi is a conjunction \bigwedge_{i=1}^m C_i of m clauses, where each clause C_i is a disjunction of literals over a set of Boolean variables X = \{x_1, \dots, x_n\}. A literal is either a variable x_j or its negation \neg x_j. An assignment \sigma: X \to \{0,1\} satisfies a clause C_i if at least one literal in C_i evaluates to true under \sigma; otherwise, the clause is falsified.[3][4] In the unweighted MAX-SAT problem, the input is a CNF formula \phi, and the objective is to find an assignment \sigma that maximizes the number of satisfied clauses. The decision version asks whether there exists an assignment satisfying at least k clauses, for a given integer k. Let \mathrm{opt}(\phi) denote the maximum number of clauses that can be satisfied by any assignment.[4] The weighted MAX-SAT problem extends the unweighted version by associating a positive weight w_i \in \mathbb{R}^+ with each clause C_i. The objective is then to find an assignment \sigma that maximizes the total weight \sum_{i: C_i \text{ satisfied by } \sigma} w_i of satisfied clauses.[4] In this setting, \mathrm{opt}(\phi) denotes the maximum total weight achievable. A variant known as partial MAX-SAT (or weighted partial MAX-SAT) distinguishes hard clauses (which must all be satisfied) from soft clauses (which have positive weights and may be falsified); the goal is to satisfy all hard clauses while maximizing the total weight of satisfied soft clauses, treating falsified soft clauses as having weight 0.[3] MAX-SAT generalizes the Boolean satisfiability problem (SAT), which is the special case requiring k = m (all clauses satisfied).Historical Context
The Maximum Satisfiability (MAX-SAT) problem emerged in the early 1970s amid foundational studies on computational complexity and approximation algorithms for NP-complete problems. David S. Johnson introduced the problem in 1974, framing it within the broader exploration of NP-completeness and developing the first approximation algorithms for it, which guaranteed satisfying at least half of the clauses in certain cases. This work built on the recognition of the Boolean satisfiability problem (SAT) as NP-complete, extending it to an optimization variant where the goal is to maximize the number of satisfied clauses rather than achieve full satisfiability. In 1981, Mihalis Yannakakis improved the approximation ratio to 3/4 using linear programming relaxations.[5] In the late 1970s and 1980s, researchers like Michael R. Garey and David S. Johnson further connected MAX-SAT to approximation theory through their comprehensive catalog of NP-complete problems, proving NP-hardness for restricted variants such as MAX-2-SAT (where clauses have at most two literals). Their 1979 book formalized these results and highlighted approximation as a practical response to intractability, influencing subsequent algorithmic developments. Interest grew steadily, but practical solvers remained limited until the 1990s, when advances in SAT solving techniques—such as the Davis-Putnam-Logemann-Loveland (DPLL) procedure enhancements—spilled over to MAX-SAT, enabling more efficient heuristic and exact methods for real-world instances. A key milestone came in 1994 when Michel X. Goemans and David P. Williamson presented new 3/4-approximation algorithms for general MAX-SAT based on linear programming relaxations and randomized rounding techniques.[6] In 1995, they introduced a semidefinite programming (SDP)-based approximation achieving approximately 0.878 for MAX-2-SAT, setting a benchmark for hardness-aware approximations.[7] The field gained momentum in the late 1990s through dedicated workshops and evaluations, culminating in the first formal MAX-SAT Evaluation in 2006 as an affiliated event of the SAT conference, which benchmarked solvers and spurred competition-driven innovations.[8] Earlier precursors, such as discussions at the SAT 2000 workshop, highlighted growing interest in optimization extensions of SAT.[9] Post-2010, MAX-SAT research surged due to applications in AI domains like planning, machine learning model optimization, and knowledge representation, as well as hardware and software verification tasks requiring trade-off balancing in over-constrained systems.[3] In the 2020s, local search methods saw significant refinements, with hybrid approaches combining stochastic local search and core-guided techniques improving solution quality on industrial benchmarks by up to 5% over prior state-of-the-art solvers in evaluations.[10] These advances reflect MAX-SAT's evolution from theoretical construct to a vital tool in scalable optimization.Illustrative Examples
Unweighted Example
Consider the unweighted MAX-SAT instance consisting of three Boolean variables x_1, x_2, x_3 and the following four clauses, each with implicit weight 1: \phi = (x_1 \lor x_2) \land (x_1 \lor \neg x_2) \land (\neg x_1 \lor x_3) \land (\neg x_1 \lor \neg x_3). The objective is to assign truth values to the variables to maximize the number of satisfied clauses. This formula is unsatisfiable, as no assignment can satisfy all four clauses simultaneously. The first two clauses force x_1 to be true: if x_1 were false, both clauses would require x_2 to be true and false, a contradiction. Likewise, the last two clauses force x_1 to be false: if x_1 were true, both would require x_3 to be true and false, another contradiction. The maximum number of satisfiable clauses is 3. For instance, the assignment x_1 = \top, x_2 = \bot, x_3 = \top satisfies the first three clauses but falsifies the fourth:- Clause 1: \top \lor \bot = \top
- Clause 2: \top \lor \neg \bot = \top \lor \top = \top
- Clause 3: \neg \top \lor \top = \bot \lor \top = \top
- Clause 4: \neg \top \lor \neg \top = \bot \lor \bot = \bot.
| x_1 | x_2 | x_3 | Satisfied Clauses | Count |
|---|---|---|---|---|
| \bot | \bot | \bot | 2, 3, 4 | 3 |
| \bot | \bot | \top | 2, 3, 4 | 3 |
| \bot | \top | \bot | 1, 3, 4 | 3 |
| \bot | \top | \top | 1, 3, 4 | 3 |
| \top | \bot | \bot | 1, 2, 4 | 3 |
| \top | \bot | \top | 1, 2, 3 | 3 |
| \top | \top | \bot | 1, 2, 4 | 3 |
| \top | \top | \top | 1, 2, 3 | 3 |