AlgoVerse

درخت عبارت و مسئله‌ی صدق‌پذیری

یک فرمول گزاره‌ای را به درخت عبارت تبدیل می‌کند و آن را برای هر مقداردهی متغیرها با پیمایش پس‌ترتیب ارزیابی می‌کند؛ فرمول صدق‌پذیر است اگر سطری درست شود. 2^n مقداردهی.

هر فرمول گزاره‌ای یک درخت عبارت دارد: برگ‌ها متغیرها هستند و گره‌های داخلی عملگرها (¬ یک فرزند، ∧ و ∨ دو فرزند). مقدار فرمول با پیمایش پس‌ترتیب به دست می‌آید: اول فرزندان، بعد عملگر.

ادامه‌ی توضیح ↓
ورودی:
formula="(a&~b)|(~a&c…"خروجی PDF

(a ∧ ¬b) ∨ (¬a ∧ c) ∨ ¬c؛ سه متغیر و ۸ سطر، ۷ سطر درست است (فقط وقتی هر سه درست‌اند نادرست می‌شود).

  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

ناوردا: مقدار هر گره فقط پس از مقدار فرزندانش حساب می‌شود (پس‌ترتیب).

شروع اجرا

∅

models—

جدول هنوز خالی است.

درخت فراخوانی‌های بازگشتی

نارنجی پر = فراخوانی در حال اجرا · حاشیه‌ی نارنجی = هنوز روی پشته · خاکستری = تمام شده

متغیرهای محلی

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

نارنجی = در همین گام عوض شد

Call stack

  1. satisfiable()خط 8
گام ۱ از ۱٬۱۱۵
خط سیاه = row · خط نارنجی = گام کلیدیparsed: 0/1 · variable: 0/40 · negate: 0/24 · conj: 0/16 · disj: 0/16 · row: 0/8
    توضیح

    درخت عبارت

    هر فرمول گزاره‌ای یک درخت عبارت دارد: برگ‌ها متغیرها هستند و گره‌های داخلی عملگرها (¬ یک فرزند، ∧ و ∨ دو فرزند). مقدار فرمول با پیمایش پس‌ترتیب به دست می‌آید: اول فرزندان، بعد عملگر.

    صدق‌پذیری

    فرمول صدق‌پذیر است اگر مقداردهی‌ای از متغیرها آن را درست کند. روش مستقیم (کتاب هوروویتز) همه‌ی 2^n مقداردهی را امتحان می‌کند و هر بار درخت را ارزیابی می‌کند: همان جدول درستی.

    این مسئله (SAT) نخستین مسئله‌ای است که NP-کامل بودنش ثابت شد (Cook–Levin)؛ هیچ الگوریتم چندجمله‌ای برایش شناخته نشده است.

    ورودی

    حروف a تا d متغیرند؛ ~ نقیض، & «و»، | «یا» و پرانتز. ~ از همه قوی‌تر و | از همه ضعیف‌تر است.