🧩 Constraint Solving POTD:Problem of the Day: Maximum Satisfiability (MaxSAT)

[github-actions[bot]]

Problem Statement

Given a Boolean formula in conjunctive normal form (CNF) — a collection of clauses, each a disjunction of literals — find an assignment to the variables that maximizes the number of satisfied clauses.

Unlike classical SAT (which asks: "Can all clauses be satisfied?"), MaxSAT relaxes the requirement and accepts partial satisfaction. This makes it a true optimization problem: we want to find the best feasible solution, not just any feasible solution.

Concrete Example

Consider this 3-variable MaxSAT instance with 5 clauses:

(x1 ∨ ¬x2 ∨ x3)       Clause 1
(¬x1 ∨ x2)            Clause 2
(x2 ∨ x3)             Clause 3
(¬x1 ∨ ¬x2 ∨ ¬x3)    Clause 4
(x1)                  Clause 5

An assignment like {x1 = true, x2 = true, x3 = false} satisfies clauses 1, 2, 3, and 5 (4 out of 5). Can we do better? Try to find an assignment that satisfies all 5 clauses, or prove that 4 is the best we can do.

Input/Output Specification

• Input: A CNF formula with n Boolean variables and m clauses. Each clause is a list of literals (variables or their negations).
• Output: An assignment (variable → {true, false}) that maximizes the number of satisfied clauses. Report the number of satisfied clauses.

---

Why It Matters

Real-world applications:

1. Fault diagnosis & debugging: Hardware test vectors often produce overconstrained systems. MaxSAT helps find an assignment that satisfies as many test constraints as possible.

2. AI planning & reasoning: When multiple competing preferences or soft constraints exist (e.g., "prefer this sensor, but if unavailable, use that one"), MaxSAT balances trade-offs gracefully.

3. Bioinformatics: Sequence alignment and phylogenetic tree inference often involve soft constraints; MaxSAT finds solutions respecting as many biological constraints as feasible.

4. Software engineering: Automated bug fixing and program synthesis benefit from MaxSAT when complete satisfaction is impossible.

5. Weighted formula variants (Weighted MaxSAT, Partial MaxSAT) extend this to real-world domains like energy grid scheduling, traffic management, and financial portfolio optimization.

---

Modeling Approaches

Approach 1: Classical MaxSAT (Unweighted, Complete Enumeration)

Paradigm: Brute-force search + SAT checking

Decision variables: Binary variables x_i ∈ {0, 1} for each Boolean variable.

Objective: Maximize the count of satisfied clauses:

maximize Σ y_j
subject to:
  y_j ∈ [0, 1]  (indicator for clause j being satisfied)
  For each clause (l1 ∨ l2 ∨ ... ∨ l_k):
    y_j ≤ (Σ assignments to literals in clause) / k

Trade-offs:

• Simple to understand
• Complete enumeration is exponential in the number of variables
• No leverage from SAT solver optimizations
• Better for small instances (< 20 variables)

---

Approach 2: SAT-Based Upper Bounding (Linear Relaxation + Cutting Planes)

Paradigm: SAT solver + incremental refinement (binary search on "how many clauses can we satisfy?")

Formulation:

• Start with a candidate lower bound (e.g., 0 clauses satisfied).
• Query: "Can we satisfy ≥ k clauses?"
• Encode this as a new SAT instance: add a constraint that forces at least k clauses to be true.
• Use binary search to narrow the gap between lower and upper bounds.

Trade-offs:

• Leverages mature SAT solver technology (conflict analysis, unit propagation)
• Practical for instances with hundreds of variables and thousands of clauses
• Each query involves a SAT solve, so total runtime scales with the binary search depth
• Works well when the optimal number of clauses is not too close to the total

---

Approach 3: Integer Linear Programming (ILP)

Paradigm: Mixed-integer linear program

Decision variables:

• x_i ∈ {0, 1} for each Boolean variable
• y_j ∈ {0, 1} for each clause (1 if satisfied, 0 otherwise)

Objective:

maximize Σ_j y_j

Constraints: For each clause (l1 ∨ l2 ∨ ... ∨ l_k), ensure:

y_j ≤ Σ_i contribution(l_i)

where contribution captures whether each literal is satisfied.

Trade-offs:

• Natural formulation for branch-and-bound solvers (CPLEX, Gurobi)
• Supports weighted variants trivially
• Can add domain-specific valid inequalities for strengthening
• Solver overhead is higher than pure SAT, but often finds optimal solutions faster in practice for large, structured instances

---

Example: ILP Model (Pseudo-code)

maximize: sum of y[j] for all clauses j

variables:
  x[i] ∈ {0, 1}  for each variable i
  y[j] ∈ {0, 1}  for each clause j

constraints:
  For clause j = (l1 ∨ l2 ∨ ... ∨ l_k):
    y[j] ≤ (value_of_l1) + (value_of_l2) + ... + (value_of_l_k)
    where value_of_li = x[i] if li is positive, 1 - x[i] if li is negated

End.

Example instance encoding:
Clause (x1 ∨ ¬x2):

y[clause] ≤ x[1] + (1 - x[2])

This constraint forces y[clause] to be 0 if neither literal is satisfied.

---

Key Techniques

1. Clause Weighting & Core Extraction

Many solvers use iterative unsatisfiable core extraction:

• Attempt to satisfy all clauses (standard SAT).
• If unsatisfiable, extract a core (minimal unsatisfiable subset).
• Remove one clause from the core, relax it to a soft constraint, and retry.
• Repeat until a solution is found.

This trades satisfaction of some clauses for satisfiability of others, guided by conflict analysis.

2. Branch-and-Bound with Lower/Upper Bounds

Solvers maintain:

• Lower bound: Best feasible solution found so far (current assignment)
• Upper bound: Relaxation of the problem (e.g., an LP bound or counting argument)

At each search node, prune if the upper bound ≤ lower bound. This dramatically reduces the search space.

3. Symmetry Breaking & Local Search

For structured instances, identify variable symmetries and add breaking constraints (e.g., "if variable x and y are interchangeable, force x ≤ y in lexicographic order"). Hybrid approaches combine SAT with local-search moves (flipping variable assignments) to escape local minima.

---

Challenge Corner

Extend and explore:

1. Weighted MaxSAT: Suppose each clause has a weight w_j (importance). How would you modify your model and solver strategy to maximize Σ w_j · y_j instead of just the count?

2. Partial MaxSAT: In some formulations, certain "hard" clauses must be satisfied, while others are "soft" and contribute to the objective. How does this change your propagation and branching strategy?

3. Approximation & Heuristics: MaxSAT is NP-hard. What simple randomized or greedy heuristics could give you a reasonable solution in polynomial time? (Hint: random assignment satisfies each clause with probability close to 1 - (1/2)^k for a clause with k literals.)

4. Symmetry Exploitation: If your CNF has redundant variables or clauses, how would you detect and exploit these symmetries to reduce the search space?

---

References

1. "An Introduction to SAT Solving" — Handbook chapter by Biere, Heule, van Maaren, and Walsh (2009). Covers SAT and MaxSAT broadly.

2. "MaxSAT Evaluation" — International competition website and proceedings (www.maxsat.org). Showcases state-of-the-art algorithms and benchmarks.

3. "Handbook of Constraint Programming" — Ch. 32 on SAT and pseudo-Boolean satisfaction (Rossi, van Beek, Walsh, 2006). Excellent unified perspective.

4. "Maximum Satisfiability: A Tutorial" — Paper by Argelich et al. (various years). Practical overview of algorithms, from basic SAT-based methods to advanced core-guided techniques.

---

Dive deeper: Try encoding a small MaxSAT instance and solving it with a SAT solver supporting MaxSAT (e.g., Open-WBO, RC2, or MaxHS). Compare the time and solution quality across different instance sizes!

Generated by 🧩 Constraint Solving — Problem of the Day · copilot · haiku45 · ~8 AIC · ⌖ ~7 AIC · ⊞ 6.7K · ◷

• expires on Nov 5, 2026, 3:31 AM UTC-08:00

[github-actions[bot]]

This discussion has been marked as outdated by Constraint Solving — Problem of the Day.

A newer discussion is available at Discussion #73175.