Introduction

Imagine a set of yes/no switches and a list of rules about them: "at least one of A, B, C is on", "A and B are not both on", and so on. Is there any way to flip the switches so that every rule holds at once?

That is the Boolean satisfiability problem, or SAT. The switches are variables (true or false), the rules are clauses, and a formula is satisfiable if some assignment makes all clauses true at the same time.

It sounds like a puzzle, and it is — but it's also the problem that, in 1971, became the very first to be proven NP-complete. Almost every hard problem you've met on this site can be rephrased as a SAT formula. Understanding SAT means understanding the shape of difficulty itself.

Try to Satisfy It

Here is a small formula in the standard form SAT uses: an AND of clauses, where each clause is an OR of variables (a bar or ¬ means "not"). The whole formula is true only when every clause is true.

Flip the variables and watch the clauses light up. Notice how easy it is to check a guess — one glance tells you which clauses are red. The hard part is finding an assignment that turns them all green, and with n variables there are 2n2^{n} assignments to consider. Stuck? Press Brute-force search to try them one by one.

<p class="hint">A logic formula is a big <b>AND</b> of clauses; each clause is an <b>OR</b> of
variables (some negated, shown with ¬). The formula is satisfied only when <b>every clause</b>
is true. Flip the variables below and watch the clauses turn green. Can you make them all green?</p>
<div id="formula" class="formula"></div>
<div class="vars" id="vars"></div>
<p id="status" class="status"></p>
<div class="bar-btns">
  <button id="solve" type="button">Brute-force search</button>
  <button id="reset" type="button" class="ghost">All false</button>
</div>
<p id="note" class="note"></p>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .6rem; line-height: 1.45; }
.formula { display: flex; flex-wrap: wrap; align-items: center; gap: .35rem; margin: .5rem 0; font: 600 15px ui-monospace, monospace; }
.clause { padding: .3rem .55rem; border-radius: 8px; border: 2px solid #ccc; background: #f4f4f4; transition: all .12s; white-space: nowrap; }
.clause.sat { background: #e7f6ee; border-color: #2a9d8f; color: #0a7d33; }
.clause.unsat { background: #fdecec; border-color: #e63946; color: #c0392b; }
.and { color: #999; font-weight: 700; padding: 0 .1rem; }
.vars { display: flex; flex-wrap: wrap; gap: .5rem; margin: .6rem 0; }
.var { padding: .45rem .8rem; border-radius: 8px; border: 2px solid #bbb; background: #fff; cursor: pointer; font: 700 15px ui-monospace, monospace; min-width: 70px; transition: all .12s; }
.var.t { background: #457b9d; color: #fff; border-color: #457b9d; }
.var.f { background: #eee; color: #555; }
.status { font-size: 1rem; font-weight: 700; min-height: 1.3em; margin: .3rem 0; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c0392b; }
.bar-btns { display: flex; gap: .5rem; flex-wrap: wrap; margin: .3rem 0; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #457b9d; background: #457b9d; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #457b9d; }
.note { font-size: .85rem; color: #666; margin: .3rem 0 0; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Boolean satisfiability (SAT) in conjunctive normal form: an AND of clauses,
    // each an OR of literals. CHECKING an assignment is one pass over the clauses;
    // FINDING a satisfying one means searching up to 2^n assignments.
const VARS = ['a', 'b', 'c', 'd'];
// literal = { v: variable index, neg: is-negated }
const CLAUSES = [
  [{ v: 0, neg: false }, { v: 1, neg: false }, { v: 2, neg: false }], // a ∨ b ∨ c
  [{ v: 0, neg: true }, { v: 1, neg: true }],                          // ¬a ∨ ¬b
  [{ v: 1, neg: false }, { v: 2, neg: true }, { v: 3, neg: false }],   // b ∨ ¬c ∨ d
  [{ v: 1, neg: true }, { v: 2, neg: false }],                         // ¬b ∨ c
  [{ v: 3, neg: true }, { v: 0, neg: false }],                         // ¬d ∨ a
];
let assign = VARS.map(() => false);

const litTrue = (lit, asg) => lit.neg ? !asg[lit.v] : asg[lit.v];
const clauseSat = (cl, asg) => cl.some(l => litTrue(l, asg));
const litText = lit => (lit.neg ? '¬' : '') + VARS[lit.v];

function buildFormula() {
  const box = document.getElementById('formula');
  box.innerHTML = '';
  CLAUSES.forEach((cl, i) => {
    if (i) { const a = document.createElement('span'); a.className = 'and'; a.textContent = '∧'; box.appendChild(a); }
    const el = document.createElement('span');
    el.className = 'clause'; el.dataset.i = i;
    el.textContent = '(' + cl.map(litText).join(' ∨ ') + ')';
    box.appendChild(el);
  });
}

function buildVars() {
  const box = document.getElementById('vars');
  box.innerHTML = '';
  VARS.forEach((name, i) => {
    const b = document.createElement('button');
    b.className = 'var'; b.dataset.i = i;
    b.addEventListener('click', () => { assign[i] = !assign[i]; render(); });
    box.appendChild(b);
  });
}

function countSolutions() {
  let n = 0;
  for (let m = 0; m < (1 << VARS.length); m++) {
    const asg = VARS.map((_, i) => Boolean(m & (1 << i)));
    if (CLAUSES.every(cl => clauseSat(cl, asg))) n++;
  }
  return n;
}
const TOTAL_SOLUTIONS = countSolutions();

function render() {
  let satCount = 0;
  CLAUSES.forEach((cl, i) => {
    const ok = clauseSat(cl, assign);
    if (ok) satCount++;
    const el = document.querySelector(`.clause[data-i="${i}"]`);
    el.classList.toggle('sat', ok);
    el.classList.toggle('unsat', !ok);
  });
  VARS.forEach((name, i) => {
    const b = document.querySelector(`.var[data-i="${i}"]`);
    b.textContent = `${name} = ${assign[i] ? 'T' : 'F'}`;
    b.classList.toggle('t', assign[i]);
    b.classList.toggle('f', !assign[i]);
  });
  const st = document.getElementById('status');
  if (satCount === CLAUSES.length) {
    st.textContent = fmt('All %length% clauses true — the formula is SATISFIED! 🎉', { length: CLAUSES.length });
    st.className = 'status ok';
  } else {
    st.textContent = fmt('%satCount% of %length% clauses satisfied — keep flipping.', { satCount: satCount, length: CLAUSES.length });
    st.className = 'status bad';
  }
  document.getElementById('note').textContent =
    fmt('This formula has %TOTAL_SOLUTIONS% satisfying assignment(s) out of %v% possible.', { TOTAL_SOLUTIONS: TOTAL_SOLUTIONS, v: 1 << VARS.length });
}

function bruteForce() {
  const total = 1 << VARS.length;
  let steps = 0, found = -1;
  for (let m = 0; m < total; m++) {
    steps++;
    const asg = VARS.map((_, i) => Boolean(m & (1 << i)));
    if (CLAUSES.every(cl => clauseSat(cl, asg))) { found = m; break; }
  }
  const st = document.getElementById('status');
  if (found >= 0) {
    assign = VARS.map((_, i) => Boolean(found & (1 << i)));
    render();
    st.textContent = fmt('Found a satisfying assignment after checking %steps% of %total% — the formula is SATISFIABLE.', { steps: steps, total: total });
    st.className = 'status ok';
  } else {
    st.textContent = fmt('Checked all %total% assignments — UNSATISFIABLE.', { total: total });
    st.className = 'status bad';
  }
  console.log(fmt('SAT brute force: checked %steps%/%total%, %v%', { steps: steps, total: total, v: found >= 0 ? 'SAT' : 'UNSAT' }));
}

document.getElementById('solve').addEventListener('click', bruteForce);
document.getElementById('reset').addEventListener('click', () => { assign = VARS.map(() => false); render(); });

buildFormula();
buildVars();
render();
Result
Console

With four variables there are only sixteen possibilities, so brute force finishes instantly. But double the variables to a few hundred — common in real formulas — and 2n2^{n} becomes more assignments than there are atoms in the universe. That is the wall SAT puts in front of us.

The First NP-complete Problem

SAT holds a unique place in computer science. In 1971, the Cook–Levin theorem proved it NP-complete — the first problem ever shown to be so.

That word carries a precise, powerful meaning:

  • Checking is easy. Given an assignment, you verify it in one quick pass over the clauses. So SAT is in NP.
  • It's universal. Every problem in NP can be rewritten as a SAT formula. Solve SAT efficiently and you solve all of them — which is exactly the P vs NP question.
  • Even 3-SAT is hard. Restricting every clause to just three literals (3-SAT) stays NP-complete, while the two-literal version (2-SAT) is easy. The boundary of difficulty is razor-thin.

Because so many problems reduce to SAT, it became the natural starting point for proving other problems hard: show that SAT reduces to your problem, and your problem is NP-hard too. SAT is the seed from which the whole forest of NP-complete problems grew.

How Solvers Win

Here is the twist that makes SAT inspiring rather than depressing: despite being NP-complete, real SAT formulas are solved every day — formulas with millions of variables.

Modern SAT solvers don't blindly try 2n2^{n} assignments. They are clever:

  • Unit propagation: if a clause has only one unassigned literal left, its value is forced — so commit to it and cascade the consequences.
  • Backtracking (DPLL): guess a variable, follow the forced consequences, and if you hit a contradiction, undo and try the other value.
  • Clause learning (CDCL): when a guess fails, learn a new clause that records why, so the same dead end is never explored again.

None of this changes the worst case — SAT is still NP-complete. But on the structured formulas that arise in practice, these tricks prune the search so aggressively that solvers feel almost magical. It's a beautiful lesson: "hard in theory" and "useless in practice" are not the same thing.

Where It Matters

SAT solvers are one of computer science's quiet success stories, hidden inside tools you rely on:

  • Hardware verification: chip makers encode "could this circuit ever misbehave?" as a SAT formula — if it's unsatisfiable, the chip is provably correct on that property.
  • Software verification: bug-finding and model-checking tools turn programs into formulas to prove safety or hunt for crashes.
  • Planning and scheduling: robotics, logistics, and AI planners express goals and constraints as SAT (or its richer cousin, SMT).
  • Product configuration: "which option combinations are valid?" — from car trims to software packages — is a satisfiability question.
  • Security: SAT both attacks (analyzing crypto, finding exploits) and defends (proving protocols correct).

Whenever a question reduces to "is there a consistent way to set all these variables?", a SAT solver is often the sharpest tool in the box.

Conclusion

SAT is the problem that gave NP-completeness its first home. A formula of simple true/false switches captures, in one tidy package, the gap between checking (trivial) and finding (potentially astronomical). Every NP-complete problem on this site is, at heart, a SAT formula in disguise.

Yet SAT also delivers the most hopeful message in this whole story. A problem can be NP-complete in the worst case and still be tamed, day after day, on the instances that actually matter. The limits of algorithms are real — but human ingenuity keeps finding clever ways to live, and even thrive, right up against them.

Share this article

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

Comments

Loading comments...

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