Introduction

Imagine a long list of demands, each of the form "A is true, or B is false, or C is true." A single yes/no setting for every variable might make all of them happy at once — or it might not. The classic SAT problem only asks a yes/no question: does some setting satisfy every clause?

But the world is rarely so generous. Constraints conflict. Wishes contradict. When you genuinely cannot satisfy everything, the useful question changes: how many clauses can I satisfy at once? That is MAX-SAT — the maximization version of SAT.

This shift from "is it possible?" to "how close can I get?" looks tiny. It is not. It turns a decision problem into an optimization problem, drags it into the realm of the NP-hard, and — beautifully — reveals a hard mathematical wall at exactly 7/8.

Try It: Climb Toward the Maximum

Below is a small formula in conjunctive normal form: a list of clauses, each a bundle of literals joined by OR. A clause is satisfied if at least one of its literals is true. Your goal is not to satisfy all of them — that may be impossible — but to satisfy as many as you can.

<p class="hint">Each row is a <b>clause</b> — its literals are joined by OR, so the
clause is green when <b>at least one</b> literal is true. You can't satisfy every
clause here, so satisfy <b>as many as you can</b>. Toggle the variables and watch
the score climb.</p>
<div id="vars" class="vars"></div>
<div id="clauses" class="clauses"></div>
<div class="score" id="score">Satisfied: 0 / 0</div>
<div class="btns">
  <button id="find" type="button">Find optimum</button>
  <button id="random" type="button" class="ghost">Random coin flip</button>
  <button id="reset" type="button" class="ghost">All false</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .8rem; line-height: 1.45; }
.vars { display: flex; gap: .5rem; flex-wrap: wrap; margin: 0 0 .9rem; }
.var { font: 700 15px ui-monospace, monospace; padding: .4rem .8rem; border-radius: 999px;
       border: 1px solid #1d3557; cursor: pointer; user-select: none; transition: all .12s; }
.var.t { background: #1d3557; color: #fff; }
.var.f { background: #fff; color: #1d3557; }
.clauses { display: flex; flex-direction: column; gap: 5px; margin: .3rem 0 .8rem; }
.clause { display: flex; align-items: center; gap: .5rem; font: 600 15px ui-monospace, monospace;
          padding: .4rem .7rem; border-radius: 8px; border: 1px solid #cdd9e3; background: #f3f6f9; }
.clause.sat { background: #e3f6e9; border-color: #9ed8b4; }
.clause.unsat { background: #fdeaec; border-color: #f0aeb5; }
.lit { padding: .1rem .35rem; border-radius: 5px; }
.lit.on { background: #0a7d33; color: #fff; }
.lit.off { background: #e7e9ec; color: #777; }
.mark { margin-left: auto; font-weight: 800; }
.clause.sat .mark { color: #0a7d33; }
.clause.unsat .mark { color: #c92f3c; }
.score { font-size: 1.1rem; font-weight: 800; margin: .4rem 0 .8rem; }
.score b { color: #1d3557; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// MAX-SAT: given a CNF formula, find the assignment that satisfies the MOST
// clauses. Scoring an assignment is a quick scan; finding the maximum in general
// is NP-hard. This formula is deliberately UNSATISFIABLE, so the best you can do
// is fewer than all clauses — that is the whole point of "MAX".
//
// Literals: positive n = "var n is true", negative -n = "var n is false".
const VARS = ['x1','x2','x3'];
const CLAUSES = [
  [ 1,  2,  3],   // x1 OR x2 OR x3
  [-1, -2, -3],   // NOT x1 OR NOT x2 OR NOT x3
  [ 1, -2,  3],   // x1 OR NOT x2 OR x3
  [-1,  2, -3],   // NOT x1 OR x2 OR NOT x3
  [ 1,  2, -3],   // x1 OR x2 OR NOT x3
  [-1, -2,  3],   // NOT x1 OR NOT x2 OR x3
  [ 1, -2, -3],   // x1 OR NOT x2 OR NOT x3
  [-1,  2,  3]    // NOT x1 OR x2 OR x3
];
// assign[i] = boolean value of variable i (0-indexed: x1=index0)
let assign = VARS.map(() => false);

const litTrue = (lit, a) => lit > 0 ? a[lit - 1] : !a[-lit - 1];
const clauseSat = (cl, a) => cl.some(l => litTrue(l, a));
const score = a => CLAUSES.filter(cl => clauseSat(cl, a)).length;
const litText = l => (l < 0 ? '¬' : '') + VARS[Math.abs(l) - 1];

function renderVars() {
  const v = document.getElementById('vars'); v.innerHTML = '';
  VARS.forEach((name, i) => {
    const d = document.createElement('div');
    d.className = 'var ' + (assign[i] ? 't' : 'f');
    d.textContent = name + ' = ' + (assign[i] ? 'true' : 'false');
    d.addEventListener('click', () => { assign[i] = !assign[i]; render(); });
    v.appendChild(d);
  });
}
function renderClauses() {
  const wrap = document.getElementById('clauses'); wrap.innerHTML = '';
  CLAUSES.forEach(cl => {
    const sat = clauseSat(cl, assign);
    const row = document.createElement('div');
    row.className = 'clause ' + (sat ? 'sat' : 'unsat');
    const inner = document.createElement('div');
    inner.style.display = 'flex'; inner.style.gap = '.3rem'; inner.style.alignItems = 'center';
    cl.forEach((l, idx) => {
      const s = document.createElement('span');
      s.className = 'lit ' + (litTrue(l, assign) ? 'on' : 'off');
      s.textContent = litText(l);
      inner.appendChild(s);
      if (idx < cl.length - 1) { const o = document.createElement('span'); o.textContent = '∨'; o.style.color = '#999'; inner.appendChild(o); }
    });
    row.appendChild(inner);
    const m = document.createElement('span');
    m.className = 'mark'; m.textContent = sat ? '✓' : '✗';
    row.appendChild(m);
    wrap.appendChild(row);
  });
}
function renderScore() {
  const s = score(assign);
  document.getElementById('score').innerHTML =
    fmt('Satisfied: <b>%s% / %length%</b>', { s: s, length: CLAUSES.length });
}
function render() { renderVars(); renderClauses(); renderScore(); }

function findOptimum() {
  let best = null, bestScore = -1, tried = 0;
  for (let mask = 0; mask < (1 << VARS.length); mask++) {
    tried++;
    const a = VARS.map((_, i) => !!(mask & (1 << i)));
    const sc = score(a);
    if (sc > bestScore) { bestScore = sc; best = a; }
  }
  assign = best; render();
  console.log(fmt('Best satisfies %bestScore%/%length% clauses, found after trying all %tried% assignments. (This formula is unsatisfiable, so the max is %bestScore%, not %length%.)', { bestScore: bestScore, length: CLAUSES.length, tried: tried }));
}
function randomFlip() {
  assign = VARS.map(() => Math.random() < 0.5);
  render();
}
document.getElementById('find').addEventListener('click', findOptimum);
document.getElementById('random').addEventListener('click', randomFlip);
document.getElementById('reset').addEventListener('click', () => { assign = VARS.map(() => false); render(); });
render();
Result
Console

Toggle each variable between true and false and watch the satisfied-clause counter move. Notice the asymmetry: scoring any assignment is instant — you just walk the clauses and count. Finding the assignment with the highest score is the hard part. Press Find optimum to let the computer try all 2n2^{n} assignments by brute force; with a handful of variables that's fine, but the count doubles with every variable you add.

The Real Complexity

How hard is MAX-SAT, really?

  • Scoring an assignment is trivial: walk the clauses, count the satisfied ones.
  • Brute force tries all 2n2^{n} assignments — fine for toy formulas, hopeless past a few dozen variables.
  • It's NP-hard. MAX-SAT contains SAT as a special case: if you could always find the maximum, you could tell whether all clauses are satisfiable. So an exact, efficient solver would settle P vs NP. None is known.

Here is where MAX-SAT becomes genuinely beautiful. Since exact answers are out of reach, we approximate — aim for a guaranteed fraction of the optimum:

  • The 7/8 surprise. For formulas where every clause has exactly three distinct literals (MAX-E3SAT), just flip every variable by a fair coin. Each clause fails only if all three literals come up false — probability 1/8 — so on average you satisfy 7/8 of the clauses. No cleverness required.
  • And you can't do better. In 2001, Johan Hastad proved (using the PCP theorem) that approximating MAX-E3SAT to any ratio beyond 7/8 is itself NP-hard. The dumb coin flip is, astonishingly, optimal — no polynomial algorithm can guarantee more unless P = NP.

So MAX-SAT sits at a rare, sharp boundary: an NP-hard problem whose best-possible approximation is known exactly, and it's the one a child could discover by tossing coins.

Where It Matters

"I can't satisfy every rule — satisfy as many as possible (or the most valuable ones)" describes a huge swath of real decisions, and modern MaxSAT solvers are remarkably good at it:

  • Scheduling and timetabling: not every preference can be honored, so maximize the satisfied ones — closely related to graph coloring constraints.
  • Hardware and software debugging: when a circuit or program is over-constrained and inconsistent, MaxSAT pinpoints the smallest set of clauses to relax.
  • Planning and configuration: with soft, weighted preferences, weighted MaxSAT finds the highest-value feasible plan.
  • Bioinformatics and machine learning: aligning data, learning interpretable rules, and reconciling noisy constraints all reduce to maximizing satisfied conditions.

Whenever the perfect answer is unreachable, MAX-SAT is the formal way to ask for the best attainable one — the optimization heart beating inside SAT.

Conclusion

Change one word in SAT — from "satisfy all the clauses" to "satisfy the most you can" — and a decision problem becomes an optimization problem, instantly NP-hard. Scoring stays effortless; finding the true maximum is as hard as anything we know, tied directly to P vs NP.

And yet the limits are crisp. A blind coin flip already guarantees 7/8 of three-literal clauses, and Hastad proved in 2001 that nothing efficient can promise more. MAX-SAT is a small lesson with a big moral: when you can't have everything, the math of how close you can get is often as deep — and as sharply bounded — as the question of whether you could have it all.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/max-sat/Content licensed under CC BY-NC 4.0.