FMplex: 線形実数計算の制約充足問題に対する効率的な解法

本論文では、Fourier-Motzkin変数消去法に基づいた新しい手法FMplexを提案する。FMplexは、ケース分割を用いることで、Fourier-Motzkin変数消去法の指数関数的な計算量を改善し、単一指数関数的な計算量に抑えることができる。また、FMplexはシンプレックス法との強い対応関係を持つことを示し、SMT解法への適用を行う。