AlgoVerse

Expression trees and satisfiability

Turn a propositional formula into an expression tree and evaluate it for every assignment with a postorder walk; the formula is satisfiable if some row comes out true. 2^n assignments.

Every propositional formula has an expression tree: the leaves are variables and the inner nodes operators (¬ with one child, ∧ and ∨ with two). The formula's value comes from a postorder walk: the children first, then the operator.

Read the full explanation ↓
Input:
formula="(a&~b)|(~a&c…"PDF export

(a ∧ ¬b) ∨ (¬a ∧ c) ∨ ¬c; three variables and 8 rows, 7 of them true (only all three true makes it false).

  1. class Node:
  2. def __init__(self, key):
  3. self.key = key
  4. self.left = None
  5. self.right = None
  8. def satisfiable(formula):
  9. root = parse(formula)
  10. if root is None:
  11. return None
  12. names = []
  13. collect(root, names)
  14. names.sort()
  15. n = len(names)
  16. rows = [names + ["value"]]
  17. models = 0
  18. for m in range(2 ** n):
  19. env = {}
  20. for i in range(n):
  21. env[names[i]] = (m >> (n - 1 - i)) % 2 == 1
  22. value = evaluate(root, env)
  23. row = []
  24. for name in names:
  25. row.append("T" if env[name] else "F")
  26. row.append("T" if value else "F")
  27. rows.append(row)
  28. if value:
  29. models = models + 1
  30. return models
  33. def evaluate(node, env):
  34. # Postorder: both children first, then the operator at this node.
  35. if node.key in env:
  36. v = env[node.key]
  37. return v
  38. right = evaluate(node.right, env)
  39. if node.key == "¬":
  40. v = not right
  41. return v
  42. left = evaluate(node.left, env)
  43. if node.key == "∧":
  44. v = left & right
  45. else:
  46. v = left | right
  47. return v
  50. def collect(node, names):
  51. if node is None:
  52. return
  53. if node.key.isalpha() and node.key not in names:
  54. names.append(node.key)
  55. collect(node.left, names)
  56. collect(node.right, names)
  59. def parse(text):
  60. # | is or, & is and, ~ is not; ~ binds tightest and | loosest.
  61. toks = []
  62. for c in text:
  63. if c != " ":
  64. toks.append(c)
  65. pos = [0]
  66. root = parse_or(toks, pos)
  67. if pos[0] != len(toks):
  68. return None
  69. return root
  72. def parse_or(toks, pos):
  73. left = parse_and(toks, pos)
  74. while left is not None and pos[0] < len(toks) and toks[pos[0]] == "|":
  75. pos[0] += 1
  76. left = join("∨", left, parse_and(toks, pos))
  77. return left
  80. def parse_and(toks, pos):
  81. left = parse_not(toks, pos)
  82. while left is not None and pos[0] < len(toks) and toks[pos[0]] == "&":
  83. pos[0] += 1
  84. left = join("∧", left, parse_not(toks, pos))
  85. return left
  88. def parse_not(toks, pos):
  89. if pos[0] >= len(toks):
  90. return None
  91. c = toks[pos[0]]
  92. pos[0] += 1
  93. if c == "~":
  94. return join("¬", None, parse_not(toks, pos))
  95. if c == "(":
  96. inner = parse_or(toks, pos)
  97. if inner is None or pos[0] >= len(toks) or toks[pos[0]] != ")":
  98. return None
  99. pos[0] += 1
  100. return inner
  101. if c.isalpha():
  102. return Node(c)
  103. return None
  106. def join(op, left, right):
  107. if right is None:
  108. return None
  109. node = Node(op)
  110. node.left = left
  111. node.right = right
  112. return node

Invariant: Each node's value is computed only after its children's (postorder).

Start

∅

models—

The table is still empty.

Recursion tree

Filled orange = running call · Orange outline = still on the stack · Grey = finished

Local variables

formula'(a&~b)|(~a&c)|~c'

Orange = changed in this step

Call stack

  1. satisfiable()line 8
Step 1 of 1,115
Black = row · Orange = key stepparsed: 0/1 · variable: 0/40 · negate: 0/24 · conj: 0/16 · disj: 0/16 · row: 0/8
    Explanation

    Expression trees

    Every propositional formula has an expression tree: the leaves are variables and the inner nodes operators (¬ with one child, ∧ and ∨ with two). The formula's value comes from a postorder walk: the children first, then the operator.

    Satisfiability

    A formula is satisfiable if some assignment of its variables makes it true. The direct method (as in Horowitz–Sahni) tries all 2^n assignments and evaluates the tree each time: that is the truth table.

    This problem (SAT) was the first one proved NP-complete (Cook–Levin); no polynomial algorithm for it is known.

    The input

    The letters a to d are variables; ~ is not, & and, | or, plus brackets. ~ binds tightest and | loosest.