sat.hopeg

# X ↑ Y / Zを X Y / !(X) Zの略記法とする(カット)。

# 入力は変数x1, x2, ..., xnを使った連言標準形の論理式とする。ただし最後に特別な記号$を付ける。
# 例: x1 ∨ x2 ∧ x1 ∨ ¬x3 $
# 簡単のために、¬x3は1つのシンボルとする。


# .は任意の1シンボルにマッチするパターン。...は省略
START <- SAT(., ., ..., .)

# x1, x2, ..., xnは変数であり、仮定を表す。
# x1 = .であれば、まだx1について何も仮定していない状態であり、
# x1 = &("x1") . であれば、x1は真と仮定した状態であり、
# x1 = &("¬x1") . であれば、x1は偽と仮定した状態である。
SAT(x1, x2, ..., xn)
  <- $ # 節が残っていなければ受理。
   / &("x1") ↑ # 最初のシンボルが"x1"の場合
     (
      x1 # それはこれまでの仮定と矛盾せず、
        [^∧]* "∧" # 次の∧までを飛して、
        SAT(&("x1") x1, x2, ..., xn) # "x1"を仮定に加えたものにマッチする。
      / # あるいは
      "x1" "∨" # 他の選択肢があり
      SAT(x1, x2, ..., xn) # "x1"を仮定に加えずに、他の選択肢を試した場合に受理される。
     )
   / &("¬x1") ↑ # 最初のシンボルが"¬x1"の場合、仮定に"¬x1"を加える以外は同じ。
     (x1 [^∧]* "∧" SAT(&("¬x1") x1, x2, ..., xn)
      / "¬x1" "∨" SAT(x1, x2, ..., xn))
   / &("x2") ↑
     (x2 [^∧]* "∧" SAT(x1, &("x2") x2, ..., xn)
      / "x2" "∨" SAT(x1, x2, ..., xn))
   / &("¬x2") ↑
     (x2 [^∧]* "∧" SAT(x1, &("¬x2") x2, ..., xn)
      / "¬x2" "∨" SAT(x1, x2, ..., xn))
   ...

# 最初のシンボルが∧の場合は、マッチしないことに注意。これは空の節があることに相当し、充足不可能である。