Fourier–Motzkin消去法
提供: miniwiki
Fourier–Motzkin消去法(英: Fourier-Motzkin elimination)とは、数理論理学および計算機科学において、一次不等式からなる一階述語論理式の限量子(∀や∃)を除去するアルゴリズム。限定記号消去法(英: Quantifier elimination)の1つ。1826年にジョゼフ・フーリエが発見し、1918年に L. L. Dines が再発見し、1936年に Theodore Motzkin が再々発見した[1]。
アルゴリズム
以下の手順を繰り返し行い、限量子を除去していく[2]。変数の定義域は実数もしくは有理数。
- 以下の置き換えを行う。
- 等式や不等式に ¬ がかかる物は反転させる。
- a ≧ b は b ≦ a へ
- a > b は b < a へ
- a = b は (a ≦ b) ∧ (b ≦ a) へ
- ∀x. P(x) は ¬ ∃x. ¬ P(x) へ
- 下記簡略化は随時行う。
- 常に成り立つ もしくは 常に不成立な不等式は真や偽に置き換える。
- 真や偽が ∧ や ∨ や ¬ に付く場合は適切に論理式を簡略化する。
- ∃x. P(x) の形式において、P(x) が x を使用してなければ、∃x. を取り除く。
- ∃x. P(x) の形式で、P(x) に限量子が出てこない物を探し、P(x) を選言標準形に変換する。
- ∃x. (P(x) ∨ Q(x)) ⇔ (∃x. P(x)) ∨ (∃x. Q(x)) の変換を行う。
- Q が x を使用していない場合、∃x. (P(x) ∧ Q) ⇔ (∃x. P(x)) ∧ Q の変換を行う。
- 下記公式を使い、限量子を除去する。
- [math]\exists x. \left(\bigwedge_h c_h \le a_h x \right) \land \left(\bigwedge_i c_i \lt a_i x \right) \land \left(\bigwedge_j b_j x \le d_j \right) \land \left(\bigwedge_k b_k x \lt d_k \right)[/math]
- [math]\Leftrightarrow \left(\bigwedge_{h,j} b_j c_h \le a_h d_j \right) \land \left(\bigwedge_{h,k} b_k c_h \lt a_h d_k \right) \land \left(\bigwedge_{i,j} b_j c_i \lt a_i d_j \right) \land \left(\bigwedge_{i,k} b_k c_i \lt a_i d_k \right)[/math]
- 上記は一般的な形式だが、より分かりやすく、2つの不等式の場合に書き下すと以下の通り。
- [math](\exists x. c \le ax \land bx \le d) \Leftrightarrow bc \le ad[/math]
- [math](\exists x. c \lt ax \land bx \le d) \Leftrightarrow bc \lt ad[/math]
- [math](\exists x. c \le ax \land bx \lt d) \Leftrightarrow bc \lt ad[/math]
- [math](\exists x. c \lt ax \land bx \lt d) \Leftrightarrow bc \lt ad[/math]
- 上記は一般的な形式だが、より分かりやすく、2つの不等式の場合に書き下すと以下の通り。
具体例
[math]\forall i. (1 \le i \le n \to i \neq n)[/math] に対して、Fourier–Motzkin消去法を使用し、簡略化する。
[math]\forall i. (1 \le i \le n \to i \neq n)[/math] [math]\Leftrightarrow\forall i. ((\lnot (1 \le i \le n)) \lor (i \neq n))[/math] [math]\Leftrightarrow\lnot \exists i. \lnot((\lnot (1 \le i \le n)) \lor (i \neq n))[/math] [math]\Leftrightarrow\lnot \exists i. (1 \le i \le n) \land (i = n)[/math] [math]\Leftrightarrow\lnot \exists i. (1 \le i) \land (i \le n) \land (i = n)[/math] [math]\Leftrightarrow\lnot \exists i. (1 \le i) \land (i \le n) \land (i \le n) \land (n \le i)[/math] [math]\Leftrightarrow\lnot \exists i. (1 \le i) \land (i \le n) \land (n \le i)[/math] [math]\Leftrightarrow\lnot \exists i. (1 \le i) \land (n \le i) \land (i \le n)[/math] ここで公式を使用する。 [math]\Leftrightarrow\lnot \exists i. (1 \le n) \land (n \le n)[/math] [math]\Leftrightarrow\lnot \exists i. (1 \le n)[/math] [math]\Leftrightarrow\lnot (1 \le n)[/math] [math]\Leftrightarrow 1 \gt n[/math] [math]\Leftrightarrow n \lt 1[/math]
整数への拡張
変数の定義域を整数にする場合の拡張を William Pugh が1992年に発表している[3]。オメガテストと名付けた判定条件を追加している。
また、1972年に D. C. Cooper がFourier–Motzkin消去法の直接の拡張ではないが、整数変数に対する限定記号消去法であるCooper法を発表している[4]。
多項式の場合
一次式ではなく、より一般的な多項式の場合 George E. Collins が1975年に発表した Cylindrical Algebraic Decomposition (CAD) を使用することにより、限定記号消去が出来る。