Introduction

Imagine planning a dinner where each guest has a small demand: "either Ana or Beto must come", "either Beto stays home or Carla comes", and so on. Every rule mentions just two people. Your job is to decide who is invited so that every rule is satisfied at once.

This is 2-SAT: a pile of clauses, each a simple "at least one of these two must be true." It feels fiddly, but there is a slick trick that always settles it fast — yes-or-no, with a witness, in a single sweep.

Now loosen one rule to mention three people: "Ana, Beto or Carla — at least one of them comes." That one extra option, repeated across the clauses, is 3-SAT, and it is one of the hardest problems in all of computer science. The jump from two to three literals is the most famous cliff in complexity theory.

Try It

Below are two satisfiability puzzles. Each clause is a box that must end up true, and a clause is true when at least one of its literals is true (a bar over a name means "not invited"). Toggle the variables and watch the clauses light up.

<p class="hint">Two satisfiability puzzles. Each clause must be <b>true</b>; a clause is true when at least one literal is true. A bar like <span class="bar">x</span> means "NOT x". Click the variable chips to flip true/false, or let each solver run.</p>

<div class="panel">
  <h4>2-SAT &middot; 2 literals per clause &middot; <span class="tag p">in P (linear)</span></h4>
  <div id="vars2" class="vars"></div>
  <div id="cl2" class="clauses"></div>
  <div class="btns">
    <button id="solve2" type="button">Solve 2-SAT</button>
    <button id="reset2" type="button" class="ghost">Reset</button>
  </div>
  <div id="st2" class="status"></div>
</div>

<div class="panel">
  <h4>3-SAT &middot; 3 literals per clause &middot; <span class="tag np">NP-complete</span></h4>
  <div id="vars3" class="vars"></div>
  <div id="cl3" class="clauses"></div>
  <div class="btns">
    <button id="solve3" type="button">Solve 3-SAT</button>
    <button id="reset3" type="button" class="ghost">Reset</button>
  </div>
  <div id="st3" class="status"></div>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #1c2530; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .8rem; line-height: 1.45; }
.bar { border-top: 2px solid currentColor; }
.panel { border: 1px solid #d4dde6; border-radius: 12px; padding: .8rem .9rem; margin-bottom: 1rem; background: #f7fafc; }
.panel h4 { margin: 0 0 .6rem; font-size: .98rem; }
.tag { font-size: .72rem; padding: .12rem .5rem; border-radius: 999px; vertical-align: middle; }
.tag.p { background: #d6f0dc; color: #0a7d33; }
.tag.np { background: #fadbdf; color: #c92f3c; }
.vars { display: flex; flex-wrap: wrap; gap: .4rem; margin-bottom: .7rem; }
.chip { font: 700 14px ui-monospace, monospace; padding: .35rem .7rem; border-radius: 8px;
        border: 1px solid #adb8c2; background: #fff; cursor: pointer; user-select: none; min-width: 64px; text-align: center; }
.chip.t { background: #1d3557; color: #fff; border-color: #1d3557; }
.chip.f { background: #fff; color: #1d3557; }
.clauses { display: flex; flex-wrap: wrap; gap: .4rem; }
.clause { font: 600 13px ui-monospace, monospace; padding: .3rem .55rem; border-radius: 8px;
          border: 1px solid #cdd9e3; background: #fff; }
.clause.sat { background: #e7f6ec; border-color: #9bd6ad; color: #0a6b2c; }
.clause.unsat { background: #fdeef0; border-color: #f0aeb5; color: #b3303c; }
.lit { display: inline-block; }
.neg { text-decoration: overline; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .7rem; }
button { font: 600 13px system-ui, sans-serif; padding: .42rem .85rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.status { font-size: .9rem; font-weight: 600; margin-top: .5rem; min-height: 1.3em; line-height: 1.4; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ---- Two SAT instances over variables encoded as integers 0..n-1. ----
// A literal is {v: index, neg: bool}. A clause is an array of literals.
// Clause is satisfied if ANY literal evaluates true under assignment a[].

// 2-SAT instance (satisfiable). Vars: a=0, b=1, c=2.
const V2 = ['a','b','c'];
const C2 = [
  [{v:0,neg:false},{v:1,neg:false}],   // a OR b
  [{v:1,neg:true }, {v:2,neg:false}],   // ¬b OR c
  [{v:0,neg:true }, {v:2,neg:false}],   // ¬a OR c
  [{v:2,neg:false},{v:0,neg:false}],    // c OR a
];
// 3-SAT instance (satisfiable). Vars: x=0, y=1, z=2, w=3.
const V3 = ['x','y','z','w'];
const C3 = [
  [{v:0,neg:false},{v:1,neg:false},{v:2,neg:false}], // x OR y OR z
  [{v:0,neg:true }, {v:1,neg:true }, {v:3,neg:false}],// ¬x OR ¬y OR w
  [{v:1,neg:false},{v:2,neg:true }, {v:3,neg:true }], // y OR ¬z OR ¬w
  [{v:0,neg:true }, {v:2,neg:false},{v:3,neg:false}], // ¬x OR z OR w
  [{v:0,neg:false},{v:1,neg:true }, {v:3,neg:true }], // x OR ¬y OR ¬w
];

const a2 = new Array(V2.length).fill(false);
const a3 = new Array(V3.length).fill(false);

function litTrue(l, a){ return a[l.v] !== l.neg; }
function clauseSat(cl, a){ return cl.some(l => litTrue(l, a)); }
function allSat(C, a){ return C.every(cl => clauseSat(cl, a)); }

function litLabel(names, l){
  return '<span class="lit'+(l.neg?' neg':'')+'">'+names[l.v]+'</span>';
}

function render(names, C, a, varsEl, clEl){
  const vw = document.getElementById(varsEl); vw.innerHTML='';
  names.forEach((nm,i)=>{
    const c=document.createElement('div');
    c.className='chip '+(a[i]?'t':'f');
    c.textContent=nm+'='+(a[i]?'T':'F');
    c.addEventListener('click',()=>{ a[i]=!a[i]; render(names,C,a,varsEl,clEl); });
    vw.appendChild(c);
  });
  const cw = document.getElementById(clEl); cw.innerHTML='';
  C.forEach(cl=>{
    const d=document.createElement('div');
    const ok=clauseSat(cl,a);
    d.className='clause '+(ok?'sat':'unsat');
    d.innerHTML='('+cl.map(l=>litLabel(names,l)).join(' ∨ ')+')';
    cw.appendChild(d);
  });
}
function setStatus(id,t,cls){ const s=document.getElementById(id); s.innerHTML=t; s.className='status '+cls; }

// ---- 2-SAT solver: implication graph + SCC (Tarjan), linear time. ----
// Node 2*v = literal "v true", node 2*v+1 = literal "v false".
function node(v,val){ return val ? 2*v : 2*v+1; }   // val=true -> v is true
function solve2sat(C, n){
  const N=2*n, adj=Array.from({length:N},()=>[]);
  // clause (p OR q): ¬p -> q and ¬q -> p
  for(const cl of C){
    const [p,q]=cl;
    // p means literal: var p.v is (true if !p.neg). "p false" node implies "q true".
    const pTrue=node(p.v,!p.neg), pFalse=node(p.v,p.neg);
    const qTrue=node(q.v,!q.neg), qFalse=node(q.v,q.neg);
    adj[pFalse].push(qTrue);
    adj[qFalse].push(pTrue);
  }
  // Tarjan SCC
  let idx=0; const low=new Array(N).fill(-1), num=new Array(N).fill(-1);
  const onst=new Array(N).fill(false), stk=[], comp=new Array(N).fill(-1); let cc=0;
  function dfs(u){
    num[u]=low[u]=idx++; stk.push(u); onst[u]=true;
    for(const w of adj[u]){
      if(num[w]<0){ dfs(w); low[u]=Math.min(low[u],low[w]); }
      else if(onst[w]){ low[u]=Math.min(low[u],num[w]); }
    }
    if(low[u]===num[u]){
      while(true){ const x=stk.pop(); onst[x]=false; comp[x]=cc; if(x===u)break; }
      cc++;
    }
  }
  for(let u=0;u<N;u++) if(num[u]<0) dfs(u);
  // unsat if v-true and v-false share a component
  const a=new Array(n).fill(false);
  for(let v=0;v<n;v++){
    if(comp[2*v]===comp[2*v+1]) return null;
    // Tarjan numbers components in reverse topological order:
    // assign the literal whose component index is SMALLER (later in topo) = true.
    a[v]= comp[2*v] < comp[2*v+1];
  }
  return a;
}

// ---- 3-SAT solver: brute force over 2^n assignments (the hard part). ----
function solve3sat(C, n){
  let steps=0;
  for(let mask=0; mask<(1<<n); mask++){
    steps++;
    const a=new Array(n);
    for(let i=0;i<n;i++) a[i]=!!(mask&(1<<i));
    if(allSat(C,a)) return {a, steps, total:(1<<n)};
  }
  return {a:null, steps, total:(1<<n)};
}

document.getElementById('solve2').addEventListener('click',()=>{
  const sol=solve2sat(C2,V2.length);
  if(sol){ for(let i=0;i<sol.length;i++) a2[i]=sol[i]; render(V2,C2,a2,'vars2','cl2');
    setStatus('st2','✓ Solved in one linear pass (implication graph + SCC). No search needed.','ok'); }
  else setStatus('st2','✗ Unsatisfiable (a variable and its negation share a component).','bad');
});
document.getElementById('reset2').addEventListener('click',()=>{ a2.fill(false); render(V2,C2,a2,'vars2','cl2'); setStatus('st2','','');});

document.getElementById('solve3').addEventListener('click',()=>{
  const r=solve3sat(C3,V3.length);
  if(r.a){ for(let i=0;i<r.a.length;i++) a3[i]=r.a[i]; render(V3,C3,a3,'vars3','cl3');
    setStatus('st3',fmt('✓ Found after trying %steps% of %total% assignments — brute-force search, 2ⁿ in the worst case.', { steps: r.steps, total: r.total }),'ok');
    console.log('3-SAT solution:', r.a, '|', 'tried', r.steps, 'of', r.total); }
  else setStatus('st3',fmt('✗ No assignment satisfies all clauses (checked all %total%).', { total: r.total }),'bad');
});
document.getElementById('reset3').addEventListener('click',()=>{ a3.fill(false); render(V3,C3,a3,'vars3','cl3'); setStatus('st3','','');});

render(V2,C2,a2,'vars2','cl2');
render(V3,C3,a3,'vars3','cl3');
Result
Console

Press Solve 2-SAT and the answer appears in one linear pass — no searching, just following forced consequences. Press Solve 3-SAT and the only general method is to try assignments: with n variables there are 2n2^{n} of them. Checking any proposed answer is instant for both; only finding one explodes — and only for the three-literal version.

The Real Complexity

The two problems look almost identical, yet they sit on opposite sides of the most important line in the field.

  • 2-SAT is in P — in fact linear time. A clause "x or y" is the same as two implications: "if not x then y" and "if not y then x." Build the implication graph of all such arrows, find its strongly connected components, and the formula is unsatisfiable exactly when some variable and its negation land in the same component. Aspvall, Plass and Tarjan (1979) turned this into an O(n+m)O(n + m) algorithm — one graph pass.
  • 3-SAT is NP-complete. "x or y or z" cannot be reduced to implications between single variables; a clause leaves a genuine choice. The Cook–Levin theorem (Stephen Cook, 1971; independently Leonid Levin, 1973) proved that general SAT — and 3-SAT in particular — is NP-complete, the very first problem shown to be so. Every problem in NP reduces to it.
  • The cliff is the choice. Two literals force consequences (logic propagates); three literals branch. That single extra option is the difference between a one-sweep algorithm and 2n2^{n} search.

So 2-SAT and 3-SAT are the cleanest illustration of the question behind P vs NP: if you ever found a fast method for 3-SAT, P would equal NP and almost every hard problem would collapse to easy.

Where It Matters

The two-versus-three split is not academic — it tells engineers exactly when a problem will stay cheap and when it may blow up.

  • 2-SAT in practice: any "this OR that" constraint solver — conflict-free scheduling, 2-coloring checks, data-cleaning rules, type inference, and parts of program analysis — runs in linear time because the constraints are binary.
  • 3-SAT as the universal hard core: it is the standard starting point for proving other problems NP-complete, via reductions to graph coloring, vertex cover and beyond.
  • Industrial SAT solvers: modern solvers attack 3-SAT and harder formulas with clever heuristics, cracking instances with millions of variables in hardware verification, planning and cryptanalysis — even though the worst case stays exponential.
  • Knowing the boundary: when you model a real problem, the moment a constraint needs three or more options at once is the moment you may have crossed from easy to hard.

The lesson is the same one behind SAT: the shape of your constraints, not their number, decides whether you get a fast answer.

Conclusion

2-SAT and 3-SAT are nearly the same sentence with one word changed — and that word moves you from a problem solved in a single graph sweep to one that may resist every algorithm we will ever write. Two literals propagate; three literals choose, and choice is where intractability lives.

That razor-thin boundary is why these two problems are taught side by side: they show, more clearly than anything else, that the difference between easy and impossible can hinge on a single extra option. Behind that gap stands P vs NP — and 3-SAT is its sharpest face.

Share this article

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

Comments

Loading comments...

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