MAX-SAT

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.

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">{{hint}}</p>
<div id="vars" class="vars"></div>
<div id="clauses" class="clauses"></div>
<div class="score" id="score">{{satisfied_init}}</div>
<div class="btns">
  <button id="find" type="button">{{btn_find}}</button>
  <button id="random" type="button" class="ghost">{{btn_random}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</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; }

// Code not found

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 $2^{n}$ assignments by brute force; with a handful of variables that's fine, but the count doubles with every variable you add.

How hard is MAX-SAT, really?

• Scoring an assignment is trivial: walk the clauses, count the satisfied ones.
• Brute force tries all $2^{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.

"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.

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.