Category: Satisfiability · Date: 2026-04-04

Problem Statement

The Maximum Satisfiability (MAX-SAT) problem asks: given a set of Boolean clauses, find a truth assignment to the variables that satisfies as many clauses as possible.

This is the optimization counterpart of the classic decision problem SAT (which asks only whether all clauses can be satisfied at once). When not all clauses can be simultaneously satisfied, MAX-SAT quantifies how close we can get.

Concrete Instance

Consider 4 Boolean variables x₁, x₂, x₃, x₄ and 7 clauses:

Input: a CNF formula with n variables and m clauses (optionally weighted).
Output: a truth assignment x₁, …, xₙ ∈ {true, false} maximizing the number (or total weight) of satisfied clauses.

For the instance above, the assignment x₁=T, x₂=T, x₃=T, x₄=F satisfies 6 out of 7 clauses (clause 4 is falsified). Can you do better?

Weighted Partial MAX-SAT extends the problem with: (a) weights on soft clauses (maximize weighted sum of satisfied soft clauses), and (b) hard clauses that must always be satisfied. This is the industry-relevant variant used in most solvers.

Why It Matters

• AI planning & diagnosis: MAX-SAT naturally models over-constrained planning problems — when a plan can't meet all goals, satisfy as many as possible. It's also the backbone of ATPG (Automatic Test Pattern Generation) in circuit testing.
• Machine learning: Many ML tasks (Markov Logic Networks, structured prediction, MAP inference in graphical models) reduce to weighted MAX-SAT. Solving MAX-SAT efficiently is therefore a key bottleneck in probabilistic inference.
• Combinatorial auctions & network design: Winner determination in auctions and fault-tolerant network design both map cleanly to weighted partial MAX-SAT instances with hard capacity constraints.

Modeling Approaches

Approach 1 — MIP (Mixed-Integer Programming)

Introduce a binary variable yⱼ ∈ {0,1} for each clause j indicating whether it is satisfied, plus the original Boolean variables xᵢ ∈ {0,1}.

Decision variables:

• xᵢ ∈ {0, 1} for each variable i
• yⱼ ∈ {0, 1} for each clause j (1 = clause satisfied)

Formulation:

maximize  Σⱼ wⱼ · yⱼ

subject to:
  for each clause j = (L₁ ∨ L₂ ∨ … ∨ Lₖ):
    Σ_{Lᵢ = xₚ}  xₚ  +  Σ_{Lᵢ = ¬xₚ}  (1 - xₚ)  ≥  yⱼ
  xᵢ, yⱼ ∈ {0, 1}
```

**Trade-offs:** MIP solvers (Gurobi, CPLEX) provide strong LP relaxations and proven optimality guarantees. However, they don't exploit the logical structure of clauses as directly as dedicated SAT-based solvers. Scales well to thousands of variables when clause density is moderate.

---

#### Approach 2 — Branch-and-Bound with SAT (MaxSAT solvers)

Modern dedicated MAX-SAT solvers combine **CDCL** (Conflict-Driven Clause Learning) with **lower-bound propagation** via the *core-guided* paradigm.

**Key idea:** Repeatedly extract *unsatisfied cores* (minimal unsatisfiable subsets) from the soft clauses and relax them by introducing *cardinality constraints*, tightening the lower bound without exhaustive enumeration.

```
procedure CoreGuidedMaxSAT(hard H, soft S with weights w):
  cost ← 0
  while SAT(H ∪ S):
    if current model satisfies all of S: return (cost, model)
    C ← extract_unsat_core(H ∪ S)   // a minimal unsat subset of S
    relax C: add cardinality constraint (at least |C|-1 of C must hold)
    cost ← cost + min_weight(C)
  return UNSAT (should not happen if H is satisfiable)
```

**Trade-offs:** Core-guided solvers (e.g., **Open-WBO**, **RC2** in PySAT, **PACOSE**) outperform MIP on highly structured, large SAT-like instances. They natively exploit logical propagation and learn conflict clauses. However, tuning restart and core-extraction strategies matters greatly for performance.

---

#### Approach 3 — Local Search (SLS)

Stochastic local search treats MAX-SAT as a black-box optimization problem.

```
procedure WalkSAT(formula F, max_flips, noise p):
  α ← random assignment
  for flip in 1..max_flips:
    if all clauses satisfied: return α
    C ← pick a random unsatisfied clause
    with probability p:  flip a random variable in C
    else:                flip the variable in C that breaks fewest clauses
  return best α seen

Trade-offs: SLS methods like WalkSAT and GSAT are extremely fast in practice and find near-optimal solutions quickly for random instances. They cannot prove optimality and may get stuck in local optima. Best used as a portfolio component or when approximate solutions suffice.

from pysat.formula import WCNF
from pysat.examples.rc2 import RC2

# Variables: x1=1, x2=2, x3=3, x4=4 (negation = negative index)
wcnf = WCNF()

# Soft clauses (weight=1 each) — maximize satisfied
wcnf.append([1, 2, -3],   weight=1)   # clause 1
wcnf.append([-1, 3],      weight=1)   # clause 2
wcnf.append([2, 4],       weight=1)   # clause 3
wcnf.append([-2, -4],     weight=1)   # clause 4
wcnf.append([1, -2, 4],   weight=1)   # clause 5
wcnf.append([-1, -3, -4], weight=1)   # clause 6
wcnf.append([3, 4],       weight=1)   # clause 7

with RC2(wcnf) as solver:
    model = solver.compute()
    print("Assignment:", model)
    print("Cost (unsatisfied):", solver.cost)
    print("Satisfied:", 7 - solver.cost)

Key Techniques

1. Core-Guided Optimization & Cardinality Encoding

The pivotal insight in modern MAX-SAT is that instead of branching on variables directly, we can identify unsatisfiable cores among soft clauses and encode the relaxation as a cardinality constraint (at-most-k or at-least-k). Efficient cardinality encodings (totalizer, sequential counter) are crucial — they determine how much propagation the underlying SAT solver can perform.

2. Preprocessing & Resolution-Based Lower Bounds

Unit propagation and failed literal detection eliminate variables before search. Resolution-based lower bounds (from LP relaxations or the dual of cardinality extensions) let solvers prune large portions of the search tree without ever exploring them. The gap between the LP relaxation bound and the optimal integer solution is often very tight for random 3-SAT instances.

3. Symmetry Breaking & Clause Learning

Even in MAX-SAT, symmetry breaking (e.g., when variables appear symmetrically in multiple clauses) can dramatically prune the search space. Clause learning (from CDCL) is inherited by MAX-SAT solvers to avoid re-exploring equivalent conflict states, making the search non-chronological and far more efficient than simple backtracking.

Challenge Corner

Think about this:

In the Weighted Partial MAX-SAT formulation, hard clauses must be satisfied and soft clauses are maximized. Suppose you model a nurse scheduling instance (from last Tuesday's POTD!) as Weighted Partial MAX-SAT — how would you encode the shift-coverage hard constraints vs. the nurse preference soft constraints?

Bonus: The approximation ratio for MAX-3-SAT is 7/8 (achieved by a simple randomized algorithm). Can you design a randomized algorithm that guarantees satisfying at least 7/8 of clauses in expectation? What assumption does this make about clause structure?

References

1. Argelich, J. et al. — MAX-SAT Evaluation (annual competition). Results and benchmarks at maxsat.pages.inesctec.pt
2. Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J. — Iterative and core-guided MaxSAT solving: A survey and assessment, Constraints 18(4), 2013. The definitive survey of core-guided algorithms.
3. Selman, B., Kautz, H., Cohen, B. — Noise strategies for improving local search, AAAI 1994. The original WalkSAT paper.
4. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) — Handbook of Satisfiability (2nd ed.), IOS Press, 2021. Chapters 19–21 cover MAX-SAT in depth.

Generated by Constraint Solving — Problem of the Day · ● 222.2K · ◷

• expires on Apr 11, 2026, 12:54 PM UTC