AlgoVerse

Resolution

From two clauses, one containing ℓ and the other ¬ℓ, build a new clause holding the rest of both. Reaching the empty clause shows the clauses are unsatisfiable; proof by contradiction works this way.

From the clauses p ∨ A and ¬p ∨ B follows A ∨ B: if p is true, B must be, and if it is false, A must be. The new clause is the resolvent.

Read the full explanation ↓
Input:
clauses="p|q, ~p|r, ~…"PDF export

Proving q from p ∨ q, ¬p ∨ r and ¬r: add the negated conclusion (¬q) and reach the empty clause.

  1. def resolution(clauses):
  2. # clauses: "p|q, ~p|r, ~q": a conjunction of disjunctions. Each clause becomes a sorted list of literals.
  3. known = []
  4. rows = [] # for the picture: number, clause, where it came from
  5. for part in clauses.split(","):
  6. lits = sorted(set(x.strip() for x in part.split("|") if x.strip()))
  7. if lits and lits not in known:
  8. known.append(lits)
  9. rows.append([len(rows) + 1, " ∨ ".join(lits), "given"])
  10. count = len(known)
  11. i = 0
  12. while i < len(known):
  13. for j in range(i):
  14. for lit in known[i]:
  15. other = lit[1:] if lit.startswith("~") else "~" + lit
  16. if other not in known[j]:
  17. continue
  18. r = []
  19. for x in known[i] + known[j]:
  20. if x != lit and x != other and x not in r:
  21. r.append(x)
  22. r.sort()
  23. tautology = False
  24. for x in r:
  25. if "~" + x in r:
  26. tautology = True
  27. if tautology or r in known:
  28. continue
  29. known.append(r)
  30. rows.append([len(rows) + 1, " ∨ ".join(r) if r else "□", str(j + 1) + ", " + str(i + 1)])
  31. if not r:
  32. return False
  33. i = i + 1
  34. return True

Invariant: Every new clause follows from the earlier ones: any assignment making all the clauses true makes it true too.

Start

count—

The table is still empty.

Local variables

clauses'p|q, ~p|r, ~r, ~q'

Orange = changed in this step

Call stack

  1. resolution()line 1
Step 1 of 323
Black = resolvent · Orange = key stepgiven: 0/1 · resolvent: 0/6 · useless: 0/2 · empty_clause: 0/1
    Explanation

    The resolution rule

    From the clauses p ∨ A and ¬p ∨ B follows A ∨ B: if p is true, B must be, and if it is false, A must be. The new clause is the resolvent.

    Proof by resolution

    To prove that q follows from some premises:

    1. write the premises and the negation of q as clauses (CNF);
    2. resolve as long as anything new appears;
    3. if the empty clause □ appears (from r and ¬r, say), the set is unsatisfiable, so q follows (proof by contradiction).

    Resolution is complete: if a set is unsatisfiable, it eventually produces the empty clause. If nothing new appears and the empty clause has not, the set is satisfiable.

    The input

    Clauses are separated by commas and the literals of a clause by |; ~ means not. The variables are p, q, r and s.