Virtual Substitution

　CAD の話が続きましたので，今回は QE のもう一つの基本，Virtual Substitution of Parametric Test Points をお話しましょう．
　随分と長い名前というか，説明そのものですが，直訳なら「変数を含む試験点の仮想的代入」といった所でしょうか？　まぁ呼び方はともかく，その特徴は次の通りです．

長所
・自由変数の個数が多い場合に CAD よりも高速
短所
・次数が高い式を含むシステムは処理できない．解の公式を用いるので，現実的には 2 次式まで
・出力が長大

ということで，次数を限定した，いわゆる special QE ですが，問題の形式を限定しないので general に近いものです．
　原理は極めて簡明です．まず，システムを連立不等式の解の存在条件に帰着させて，解集合が空でないなら，それは有限個の区間の和集合であり，それが境界点を持つなら，その全てが連立不等式を構成する多項式の零点であることにより，その値，および，それに十分近い値の何れかが，解集合に属するので，全てを代入した式の選言が成り立ち，逆にその選言が成り立つなら，解集合は空でない，というものです（実際には主係数や判別式による場合分けや，解集合がR全体となる場合に対する無限大の代入なども行われます）．
　代入する値は，Weispfenning 博士の当初（1988）の 論文では，多項式の零点 r，および，r-1，r+1，そして，異なる零点の中点の全てとなっていましたが，現在は上記のように節減されています．
　Mathematica でも，QuadraticQE や QVSPreprocessor といったオプションを True にすれば，Reduce や FindInstance で，2 次の Virtual Substitution を利用できますが，デフォルトでは False です．
　一方，Virtual Substitution と言えば RedLog，RedLog と言えば Virtual Substitution と言われるだけあって，RedLog のメインの QE 関数である rlqe は，Virtual Substitution で頑張れるだけ頑張り，駄目なら CAD という手順を踏みます．また，rlqea（QE with Answer）は解となる Parametric Test Point も添えて答えてくれる QE 関数です．

　なお，90年代に噂されていた，3 次の Virtual Substitution
は未だ実装されていません．