Fourier–Motzkin消去法

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

Fourier–Motzkin消去法: Fourier-Motzkin elimination)とは、数理論理学および計算機科学において、一次不等式からなる一階述語論理式の限量子(∀や∃)を除去するアルゴリズム限定記号消去法: Quantifier elimination)の1つ。1826年ジョゼフ・フーリエが発見し、1918年に L. L. Dines が再発見し、1936年に Theodore Motzkin が再々発見した[1]

アルゴリズム[編集]

以下の手順を繰り返し行い、限量子を除去していく[2]。変数の定義域は実数もしくは有理数

  1. 以下の置き換えを行う。
    1. 等式や不等式に ¬ がかかる物は反転させる。
    2. a ≧ b は b ≦ a へ
    3. a > b は b < a へ
    4. a = b は (a ≦ b) ∧ (b ≦ a) へ
    5. ∀x. P(x) は ¬ ∃x. ¬ P(x) へ
  2. 下記簡略化は随時行う。
    1. 常に成り立つ もしくは 常に不成立な不等式は真や偽に置き換える。
    2. 真や偽が ∧ や ∨ や ¬ に付く場合は適切に論理式を簡略化する。
    3. ∃x. P(x) の形式において、P(x) が x を使用してなければ、∃x. を取り除く。
  3. ∃x. P(x) の形式で、P(x) に限量子が出てこない物を探し、P(x) を選言標準形に変換する。
  4. ∃x. (P(x) ∨ Q(x)) ⇔ (∃x. P(x)) ∨ (∃x. Q(x)) の変換を行う。
  5. Q が x を使用していない場合、∃x. (P(x) ∧ Q) ⇔ (∃x. P(x)) ∧ Q の変換を行う。
  6. 下記公式を使い、限量子を除去する。
    \exists x. \left(\bigwedge_h c_h \le a_h x \right) \land \left(\bigwedge_i c_i < a_i x \right) \land \left(\bigwedge_j b_j x \le d_j \right) \land \left(\bigwedge_k b_k x < d_k \right)
    \Leftrightarrow \left(\bigwedge_{h,j} b_j c_h \le a_h d_j \right) \land \left(\bigwedge_{h,k} b_k c_h < a_h d_k \right) \land \left(\bigwedge_{i,j} b_j c_i < a_i d_j \right) \land \left(\bigwedge_{i,k} b_k c_i < a_i d_k \right)
上記は一般的な形式だが、より分かりやすく、2つの不等式の場合に書き下すと以下の通り。
(\exists x. c \le ax \land bx \le d) \Leftrightarrow bc \le ad
(\exists x. c < ax \land bx \le d) \Leftrightarrow bc < ad
(\exists x. c \le ax \land bx < d) \Leftrightarrow bc < ad
(\exists x. c < ax \land bx < d) \Leftrightarrow bc < ad

具体例[編集]

\forall i. (1 \le i \le n \to i \neq n) に対して、Fourier–Motzkin消去法を使用し、簡略化する。

\forall i. (1 \le i \le n \to i \neq n)
\Leftrightarrow\forall i. ((\lnot (1 \le i \le n)) \lor (i \neq n))
\Leftrightarrow\lnot \exists i. \lnot((\lnot (1 \le i \le n)) \lor (i \neq n))
\Leftrightarrow\lnot \exists i. (1 \le i \le n) \land (i = n)
\Leftrightarrow\lnot \exists i. (1 \le i) \land (i \le n) \land (i = n)
\Leftrightarrow\lnot \exists i. (1 \le i) \land (i \le n) \land (i \le n) \land (n \le i)
\Leftrightarrow\lnot \exists i. (1 \le i) \land (i \le n) \land (n \le i)
\Leftrightarrow\lnot \exists i. (1 \le i) \land (n \le i) \land (i \le n)
ここで公式を使用する。
\Leftrightarrow\lnot \exists i. (1 \le n) \land (n \le n)
\Leftrightarrow\lnot \exists i. (1 \le n)
\Leftrightarrow\lnot (1 \le n)
\Leftrightarrow 1 > n
\Leftrightarrow n < 1

整数への拡張[編集]

変数の定義域を整数にする場合の拡張を William Pugh が1992年に発表している[3]。オメガテストと名付けた判定条件を追加している。

また、1972年に D. C. Cooper がFourier–Motzkin消去法の直接の拡張ではないが、整数変数に対する限定記号消去法であるCooper法を発表している[4]

多項式の場合[編集]

一次式ではなく、より一般的な多項式の場合 George E. Collins が1975年に発表した Cylindrical Algebraic Decomposition (CAD) を使用することにより、限定記号消去が出来る。

参照[編集]