Two-phase Method と Dual Simplex:
単体法(Simplex method)の二段階法(Two-phase Method)の一段階目では、 人工変数(artificial variables)を導入することで自明な実行可能基底解(basic feasible solution)が存在する形に変形した上で、 人工変数の値の最小化を目的関数として最適化を行うことで、人工変数を取り除き、 元問題の実行可能基底階を得る。
参考: http://www.math.cuhk.edu.hk/~wei/lpch3.pdf
一方、SMTソルバでよく使われている方法は、目的関数が定数であるような問題に対して、双対単体法(dual simplex method)を用いることで、実行可能基底解を求めている。
A Fast Linear-Arithmetic Solver for DPLL(T)
http://yices.csl.sri.com/cav06.pdf
http://yices.csl.sri.com/slides-cav06.pdf
Integrating Simplex with DPLL(T)
http://yices.csl.sri.com/sri-csl-06-01.pdf
ここで、一時的に元問題の目的関数を空にしたうえでこの方法を用いれば、二段階法の一段階目と同等の効果を得られるはずだけど、これらはどういう関係にあるのだろうか？
実質的に同じ事をしているのではないかと思うのだけれど、そうなら人工変数を導入したりといった面倒な二段階単体法の代わりに、後者の方法を用いたい。