フーリエ・モツキンの消去法

フーリエ・モツキンの消去法（フーリエ・モツキンのしょうきょほう、）とは、数理論理学および計算機科学において、一次不等式からなる一階述語論理式の限量子（∀や∃）を除去するアルゴリズム。限量子消去法（）の1つ。1826年にジョゼフ・フーリエが発見し、1918年にが再発見し、1936年にが再々発見したSatisﬁability Checking Fourier–Motzkin Variable Elimination。

 アルゴリズム 
以下の手順を繰り返し行い、限量子を除去していくArithmetic Decision Procedures: a simple introduction。変数の定義域は実数もしくは有理数。
 以下の置き換えを行う。
 等式や不等式に ￢ がかかる物は反転させる。
 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 の変換を行う。
 下記公式を使い、限量子を除去する。

 上記は一般的な形式だが、より分かりやすく、2つの不等式の場合に書き下すと以下の通り。

 具体例 
 に対して、Fourier–Motzkin消去法を使用し、簡略化する。








 ここで公式を使用する。






 整数への拡張 
変数の定義域を整数にする場合の拡張を William Pugh が1992年に発表しているThe Omega Test: a fast and practical integer programming algorithm for dependence analysis。オメガテストと名付けた判定条件を追加している。

また、1972年に D. C. Cooper がフーリエ・モツキンの消去法の直接の拡張ではないが、整数変数に対する限量子消去法であるCooper法を発表しているTheorem Proving in Arithmetic without Multiplication。

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

 脚注 

Category:数理論理学
Category:述語論理
Category:ジョゼフ・フーリエ
Category:数学に関する記事
Category:数学のエポニム