実多項式系
はじめに
実多項式系とは，整方程式および不等式で構築された式
を，下のように論理結合子および量限定子を使って結合したものである．
変数 
が 
または 
内に現れることを束縛出現，
がその他の部分に現れることを自由出現という．実多項式系に変数 
の自由出現がある場合，
はその系の自由変数という．実多項式系に量限定子が含まれない場合は，quantifier freeという．
以下は，自由変数 
，
，
を持つ実多項式系の例である．
実多項式系はすべて，冠頭標準形
に変換することができる．ここで，それぞれの 
は 
または 
であり，
は系のquantifier free部分と呼ばれる量限定子のない式である．
量限定子のない実多項式系はすべて，選言標準形
に変換することができる．ここで，それぞれの 
は整方程式，あるいは不等式である．
Reduce，Resolve，FindInstanceは常に，quantifier-free部分が選言標準形で表して，実多項式系を冠頭標準形にする．それから方程式と不等式の両辺を減算して
という形式にする．このチュートリアルでは，常に系が上の形式に変換されているものと想定する．
Reduceは，任意の実多項式系を解くことができる．自由変数 
を持つ系では，解（
について 
を拡張した後）は，以下の形式
の項の選言である．ここで 
は以下のいずれかである．
また，
および 
は，
を満足するすべての 
について正しく定義され（つまり，Rootオブジェクトの分母と主要項が非零），
および 
は実数値を持ち，連続であり，不等式 
を満足するような代数関数（Rootオブジェクトあるいは根号を使って表される）である．
式(4)で記述された
の部分集合は，セルと呼ばれる．実多項式系の解の異なる項で記述されるセルは，独立である．
以下で系(
1)を解く．セルはネストされた形式で表されている．
| Out[1]= |  |
以下で
について
を拡張する関数を定義する．
独立なセルの結合として，明示的に書かれた系(
1)の解である．
| Out[5]= |  |
Resolveは任意の実多項式系から量限定子を除去することができる．入力で変数が指定されておらず，すべての入力の多項式が束縛変数において最大で二次式であるならば，Resolveは結果の系を解かずに量限定子を除去することができることもある．そうでなければ，ResolveはReduceと同じアルゴリズムを使い，同じ答を出す．
| Out[6]= |  |
FindInstanceは任意の実多項式系を扱うことができ，実数解の例，あるいは空リスト（解のない系の場合）を与える．複数の例が要求された場合，例は系のすべての解からランダムに生成されるので，
オプションの値に依存する可能性がある．1つの例が要求され，系に全称記号(
)が含まれていない場合は，1つの例だけを生成するより高速なアルゴリズムが使われ，返される例は常に同じものになる．
| Out[7]= |  |
実多項式系を解くときに一般的に用いられる主なツールは，CAD (Cylindrical Algebraic Decomposition)である（例えば[1]を参照のこと）．実多項式系に対するCADは，Mathematica ではCylindricalDecompositionで直接利用することができる．この他にも特殊な問題を解くために使われるアルゴリズムもある．
CAD法
半代数集合とセル分割
の部分集合が，量限定子を含まない実多項式系の解集合である場合，それは半代数集合である．タルスキー(Tarski)の定理[2]によれば，任意の（量化された）実多項式系の解集合は半代数集合である．
すべての半代数集合は，以下のように再帰的に定義された独立のセルの有限結合[3]として表すことができる．
のセルは，点あるいは開区間である．
CAD法の投影段階
CAD法を使って半代数集合のセル分解を見付ける場合，射影とリフティングの2つの段階がある．射影では，系(2)のquantifier-free部分 
に存在する多項式の因数の集合 
から始め，
が成り立つような射影演算子 
を使って，変数をひとつひとつ除去する．一般に，
の多項式すべてがセル 
で一定の符号なら，
の多項式すべてが 
上で描写可能である．つまり，各多項式が 
の多項式として 
上に一定数の実根を持ち，根は 
上で連続関数であり，根は一定の多様性を持ち，2つの多項式の2つの根は 
において常に等価であるか，決して等価にならないかのどちらかであるということである．変数は
という順で並ぶ．これで，
の多項式の根は半代数集合のセル分解の構築に必要な代数関数となる．
もとのCollins射影の大きさは，向上された結果より小さくなった．現在，すべての場合に適用可能な最善の射影演算子はHong [5]によるものである．しかし，ほとんどの場合，McCallum [6, 7]が提唱し，Brown [8]が改善した，これより小さい射影演算子を使うことができる．特殊な場合に適用できるさらに小さい演算子もある．等式制約がある場合は，Collins [9]が提案し，McCallum [10, 11]が改善・証明した射影演算子を使うことができる．厳密な不等式だけで方程式がない場合，および，自由変数がない，または半代数集合の完全次元部分にしか関心がない場合は，[12, 13]で記述してあるさらに小さい射影演算子を使う使うことができる．また，0次元イデアルを生成する等式制約を含む系では，グレブナー基底(Gröbner bases)を使って射影多項式を見付ける．
Mathematica は与えられた例題に対して，上述の適切な射影のなかで最小のものを使う．できる限り，等式制約を使用するが，等式制約を使用しないときは，Brownが改善したMcCallumの射影を試みる．系がうまくいかない場合は，Hongの射影を計算する．
CAD法のリフティング段階
リフティング段階では，半代数集合のセル分解を見付ける．一般に，実際の詳細は使用される射影演算子に依存するが，
の異なる根すべてと根の間の開区間で構成される
の中のセルから開始する．各セルに標本点を見付け，半代数集合を記述する系（系には 
だけを含む条件が付いている場合がある）を満足しない標本点を持つセルを削除する．次にそのセルを
のセルまで一度に一次元ずつリフティングする．セルを
までリフティングしたとしよう．セル 
を
までリフティングするために，
に 
の標本点 
の座標が代入された 
の実根を見付ける．多項式 
は 
上で描写可能なので，各根 
は 
における連続の代数関数の値であり，その関数は 
が 
の 
番目の根となるような多項式 
の 
番目の根として表すことができる．ここでセル 
を
までリフティングする作業には，これらの代数関数のグラフ，および後続のグラフ間の 
×
のスライスが含まれる．それぞれの新セルの標本点は，根のひとつと等価である 
，あるいは2つの連続する根の間の数に，
番目の座標を加えることにより得られる．第1段階で行ったように，リフティングされたセルのうち，半代数集合を記述する系を満足しない標本点を持つものは削除する．
ならば，
は量限定子変数であり，リフティングされたセルをすべて構築する必要はないかもしれない．必要なのは，
上の 
の真値（必ず定数）を求めることだけである．
ならば，リフティングされたセルのいずれかにおいて 
の真値がTrueであるとすぐに，値がTrueであることが分かる．
ならば，リフティングされたセルのいずれかにおいて 
の真値がFalseであるとすぐに値がFalseであることが分かる．
このようにして計算された標本点の係数は，一般に代数的数である．コストの高い代数的数の計算を避けるために，Mathematica では結果の妥当性が認められる限り，任意精度の浮動小数点数(Mathematica "bignum")による係数近似を使う．単独あるいはペアの多項式の2つの根が異なることを証明したり，標本点で多項式の非零符号を見付けたりする場合には，近似演算を使っただけで十分なことがある．近似演算で証明できないのは，単独あるいはペアの多項式の2つの根が等しいこと，あるいは標本点において多項式がゼロであること等である．しかし，セルの起源についての情報を使えば，このような問題が解けることが多い．例えば，2つの多項式の終結式がセル上で消失し，これらの多項式が等しい可能性のある1組の複素根を精度範囲内に持つならば，これらの根は等しいと結論付けることができる．同様に，標本点の最後の座標が，与えられた多項式の因数の根であるなら，この多項式は標本点においてゼロであるということが分かる．セルに関して集めた情報を使っても不確実性をすべて解決できない場合は，座標の厳密な代数的数値を計算する．詳細は[14, 24]を参照のこと．
決定問題，FindInstance，仮定
決定問題とは，すべての変数が存在量化された系である．つまり，
という形式の系のことである．ここで 
はすべて 
の変数となっている．決定問題を解くことは，それがTrueとFalseのどちらと等価であるかを判定すること，言い換えれば，量限定子を含まない整方程式および不等式の系 
が解を持つかどうかを判定することである．
Mathematica で実多項式の決定問題を解くために使用するアルゴリズムはすべて，系に解がある場合に 
を満足する点を生成することができる．従って，このセクションで説明するアルゴリズムは，単独の例が要求され，系に量限定子が含まれていない，あるいは存在記号しか含まれていない場合は常に，決定問題に対してReduceおよびResolveだけではなく，FindInstanceでも使われる．また，このアルゴリズムはSimplify，Refine，Integrate等，仮定を使う Mathematica 関数で，推論検定のために使われる．
以下の決定問題を解くことで，集合
に，原点を中心とする半径4/5の円板が含まれることが証明される．
| Out[10]= |  |
以下は，
に単位円板が含まれないことを示し，
に属さない単位円板上の点があるという反証を挙げている．
| Out[11]= |  |
Mathematica で任意の実多項式の決定問題を解くために使える主なメソッドはCAD (Cylindrical Algebraic Decomposition)法である．しかし，この他にも，使用可能な場合にはCADよりもよいパフォーマンスを提供する特殊な場合のアルゴリズムがいくつかある．
多項式がすべて有理数係数あるいは浮動小数点数係数に比例する場合，Mathematica ではシンプレックス線形計画法に基づくメソッドが使われる．他の線形系では，Loos-Weispfenningの線形量限定子除去法[15]の変形が使われる．系に方程式がなく，厳密な不等式だけが含まれている場合は，CAD法の高速な「一般」形が使われる[12, 13]．0次元イデアルを生成する等式制約を含む系では，解の探求にグレブナー基底が使われる．浮動小数点数係数の非線形系には，CADの非厳密係数バージョン[16]が使われる．
また，他の決定問題法の前処理として使える特殊な場合のメソッドもある．系に，ひとつの変数の定数係数に比例する等式制約が含まれる場合，線形変数の除去にこの制約が使われる．系に定数係数と比例して現れる変数しかない場合は，その変数はLoos-Weispfenningの線形量限定子除去法[15]で除去される．二次の系にしか現れない変数がある場合は，その変数を除去するためには仮の代入法[22, 23]によるWeispfenningの量限定子除去の二次法が使われる．この方法で非常にスピードアップする例もあるが，ほとんどの場合はかなりスピードが落ちる．デフォルトでは，このアルゴリズムは前処理としては使われない．
グループのシステムオプションQVSPreprocessorをTrueにすると，Mathematica はこれを使うようになる．
Mathematica には，この他にも特殊な場合の実多項式の決定問題法が2つある．まず，Aubry，Rouillier，Safey El Dinによるアルゴリズム[17]は方程式のみを含む系に適用される．このアルゴリズムの方がCAD法よりも格段に速く実行できる例もあるが，ランダムに選ばれた方程式系では，パフォーマンスがかなり劣ることが多い．従って，これはデフォルトでは使われない．
グループのシステムオプションARSDecisionをTrueに設定すると，Mathematica でそのアルゴリズムが使われるようになる．また，G. X. ZengとX. N. Zengによるアルゴリズム[18]は，単独の厳密な不等式で構成される系に適用される．ここでも，このアルゴリズムの方がCAD法よりも速くなる例もあるが，一般には遅くなる．従って，これもデフォルトにはなっていない．
グループのオプションZengDecisionをTrueに設定すると，このアルゴリズムが使われる．
任意の実多項式系
実多項式系を解く
タルスキーの定理[2]によると，任意の（量化された）実多項式系の解集合は，半代数集合である．Reduceはこの集合を解形式(4)で記述する．
以下は，
がどのようなときに，集合
が原点を中心とする半径
の円板を含むかを示している．
| Out[12]= |  |
| Out[13]= |  |
次は
軸に沿った
平面上にホイットニーの傘(Whitney umbrella)
を射影する．
| Out[14]= |  |
ここでは定義を直接使って，直前の射影集合の内部を求める．
| Out[15]= |  |
量限定子除去(QE)
変数が指定されていないResolveの目的は，量限定子を除去して，量限定子を含まない等価の式を生成することにある．その式は，使用されるアルゴリズムによって，解形式の場合もあれば，そうでない場合もある．
ここでは，入力にある
，
，
の多項式が複雑であるため，量限定子を含まない式を完全な解形式で生成することは難しい．しかし，
は入力の多項式で線形にのみ現れるので，係数の複雑性にほとんど依存しないLoos-Weispfenningの線形量限定子除去法を使うと，量限定子を即座に除去することができる．
| Out[16]= |  |
アルゴリズム
Mathematica で実多項式系およびそのQEを解くために使われる主なメソッドは，CAD法である．しかし，特殊な場合にはこれよりも簡単な方法が使える．
系に最内部の量限定子の変数についての等式制約が含まれていれば，以下の恒等式
を使って系を簡約化するために，その等式制約が使われる．ここで 
あるいは 
が非零の定数である場合，変数 
が除去される．
系の多項式すべてが最内部の量限定子の変数に比例する場合は，変数はLoos-Weispfenningの線形量限定子除去法[15]を使って除去される．
系の多項式すべてが，最も内側の量限定子からの変数について最大でも二次である場合は，仮の代入アルゴリズム[22, 23]によるWeispfenningの量限定子除去の二次法を使って変数が除去される．システムオプションQuadraticQEのデフォルト設定では，変数を指定せず少なくとも2つのパラメータを持つResolveに対して，また，1つの変数の除去がシステムのLeafCountを最大でも2倍にする限りにおいて少なくとも3つの変数を持つReduceおよびResolveに対して，このアルゴリズムが使われる．
上記3つの特殊な場合のメソッドが適用されない場合には，CAD法が使われる．しかし，まだ除去すべき量限定子が残っているか，解が要求されるかのいずれかである．
0次元イデアルを生成する等式制約を含む系には，Mathematica では解集合を見付けるためにグレブナー基底が使われる．
オプション
実多項式系を解く Mathematica 関数には，操作方法を制御するオプションが数多く備わっている．このセクションでは，そのようなオプションを要約する．
実多項式系への操作に影響を与えるReduce，Resolve，FindInstanceのオプション
CubicsとQuartics
Reduceは，デフォルトでは実数の三次および四次方程式の解法にカルダノの公式を使わない．
| Out[17]= |  |
| Out[18]= |  |
それでもなお，パラメータを含む三次および四次方程式の解は，
Root オブジェクトを使って表される．
| Out[19]= |  |
その理由は，カルダノの公式は実数解とそれ以外の解とを分離しないためである．例えば，以下で，
のときは3番目の有理解が実数であるが，
のときは最初の有理解が実数である．
| Out[20]= |  |
| Out[21]= |  |
WorkingPrecision
WorkingPrecisionの設定はCAD法のリフティング段階に影響を及ぼす．有限の作業精度 prec では，リフティングされる第1変数の標本点が，prec 桁精度で任意精度の浮動小数点数として表される．連続した変数の標本点を計算すると，すでに計算された標本点の座標に依存するしているために，厳密ではない可能性のある係数を持つ多項式の根が見付かる．従って，標本点の座標の精度は prec 以下となる．標本点における多項式の符号を判別するためには，代入後に得られる浮動小数点数のSignを評価するだけでよい．有限のWorkingPrecisionを使うと，答はより速く得られる．しかし，答が誤っていたり，精度の損失により計算が失敗したりする可能性がある．
| Out[22]= |  |
| Out[23]= |  |
ReduceOptionsグループのシステムオプション
ここで挙げるのは，実多項式系でのReduce，Resolve，FindInstanceの動作に影響を及ぼす
グループのシステムオプションである．これらのオプションは以下のように設定する．
実多項式系でのReduce，Resolve，FindInstanceの動作に影響を及ぼす
グループのオプション
AlgebraicNumberOutput
零次元イデアル 
を生成する方程式制約を持つ系の場合，Mathematica はグレブナー基底メソッドを使って投影多項式を見付けるCADアルゴリズムの変形を使う．
のグレブナー基底の辞書式順序が，最後の変数以外のすべての変数に定数係数の線形多項式を含んでいるならば，解のすべての座標は一つの代数的数の多項式，つまり最後の座標である．
の設定は，Reduceが解の座標を最後の座標によって生成された場のAlgebraicNumberオブジェクトとして表すかどうかを決定する．
| Out[24]= |  |
AlgebraicNumberOutput->Falseにすると，解の座標は
Rootオブジェクトの多項式として与えられる．
| Out[26]= |  |
FactorInequalities
入力の前処理段階で，以下のような変換
を使うと，計算が速くなることがある．しかし，これは一般に問題を解きやすくする訳ではない．さらには，問題を顕著に難しくしてしまうこともある．この変換はデフォルトでは使われない．
| Out[30]= |  |
変換(
7)を使うと，最初の例の速度が上がる．しかし，2つ目の例は顕著に遅くなっている．2つ目の例では，不等式の数が指数関数的に増加してしまっているのである．
| Out[34]= |  |
ReorderVariables
Reduceはデフォルトでは，指定された変数の順序を変えることができない．変数リストに現れる変数は，その後に現れる変数の解を表すために使用することができるが，その逆はできない．
| Out[36]= |  |
システムオプション
ReorderVariables->Trueと設定すると，
Reduceは系を解きやすくする変数順序を選ぶことができる．
| Out[38]= |  |
デフォルトでは
Solveは指定された変数の順序を変えることができる．この例では，
について解いてから
の解で
を表す方が簡単である．
| Out[40]= |  |
システムオプションを
ReorderVariables->Falseにすると，
Solveは指定された変数の順序を使う．
| Out[42]= |  |
UseNestedRoots
デフォルトでは
Reduceは三角方程式系によって定義された代数的数を表す
Rootオブジェクトで解を表すことができる．
| Out[44]= |  |
システムオプションを
UseNestedRoots->Falseにすると，
Reduceは一変数方程式のよって定義された代数的数を使う．
| Out[46]= |  |
すべての解の座標の最小多項式を見付けるのは遅い可能性がある．
| Out[48]= |  |
| Out[50]= |  |
UseNestedRoots->Trueと設定すると，
Reduceは最後の変数で線形となる三角方程式系によって定義された代数的数を使う．
| Out[52]= |  |
| Out[54]= |  |
InequalitySolvingOptionsグループのシステムオプション
ここで挙げるのは，実多項式系でのReduce，Resolve，FindInstance，CylindricalDecompositionの動作に影響を及ぼす
グループのシステムオプションである．これらのオプションは以下のように設定する．
| | |
| "ARSDecision" | False | [17]で与えられた決定アルゴリズムを使うかどうか |
| "BrownProjection" | True | [8]で与えられた向上射影演算子をCAD法で使うかどうか |
| "CAD" | True | CAD法を使うかどうか |
| "CADBacksubstitution" | Automatic | CAD法が解座標の数値を代入しなおすべきかどうか |
| "CADCombineCells" | True | CAD法の出力を，解の公式が同一となっている範囲の隣接セルを結合することによって，簡約するかどうか |
| "CADDefaultPrecision" | 30.103 | CAD法のリフティング段階で計算される非有理根の初期の精度．近似根での計算が妥当とされない場合，アルゴリズムは精度を" "の値だけ引き上げる．これで問題が解決しない場合は，厳密な代数的数の計算に戻る |
| "CADExtraPrecision" | 30.103 | CAD法のリフティング段階で使われる追加の精度 |
| "CADMethod" | Automatic | CylindricalDecompositionで使われるCAD計算メソッドを指定する |
| "CADSortVariables" | True | 単独の量限定子もしくは決定問題の量限定子変数に対して，CAD法で変数順序のヒューリスティックを使うかどうか |
| "CADZeroTest" | {0,∞} | 代数的数の座標の点で多項式を評価することによって得られた式について，CAD法で使うゼロ検定法を決定する |
| "EquationalConstraintsCAD" | Automatic | CAD法の投影段階で等式制約を使うかどうか．デフォルトのAutomatic設定では，[11]で正しいと証明された演算子が使われる．Trueの場合は，[4]で提案された複数の等式制約を使った証明されていない投影演算子が使われる |
| "FGLMBasisConversion" | False | 0次元のブレブナー基底の単変数多項式を求めるために，CADで[20]に基づくグレブナー基底変換法を使うかどうか．使わない場合は が使われる |
| "FGLMElimination" | Automatic | 等式制約が0次元イデアルを形成する系に対する決定およびQEアルゴリズムで，除去に使われる変数のひとつの線形等式制約（定数主要係数）を探すために，[20]に基づくアルゴリズムを使うかどうか |
| "GenericCAD" | True | 決定および最適化問題で，[13]に記述されているCAD法の変形を使うかどうか |
| "GroebnerCAD" | True | 等式制約が0次元イデアルを形成する系に対するCAD法で，射影としてグレブナー基底を使うかどうか |
| "LinearDecisionMethodCrossovers" |
| {0,30,20,Automatic} | 実数係数を持つ線形方程式および不等式系の解を見付けるために使用するメソッドを決定する |
| "LinearEquations" | True | 決定問題の変数を除去するために，線形等式制約（定数の主要係数）を使うかどうか |
| "LinearQE" | True | QE問題に対してLoos-Weispfenningの線形量限定子除去法[15]を使うかどうか |
| "LWDecision" | True | 線形不等式系を持つ決定問題に対して，Loos-Weispfenningの線形量限定子除去法[15]を使うかどうか |
| "LWPreprocessor" | Automatic | 決定問題の前処理として，Loos-Weispfenningの線形量限定子除去法[15]を使うかどうか |
| "ProjectAlgebraic" | Automatic | CAD法で代数的数の係数に代入される変数についての射影を計算するか，その最小多項式を使うか |
| "ProveMultiplicities" | True | CAD法のリフティング段階で投影方程式のの複数根と零主係数を証明する方法を決める |
| "QuadraticQE" | Automatic | QEのバーチャル代入法により，Weispfenningの量限定子除去の二次法を使うかどうか |
| "QVSPreprocessor" | False | バーチャル代入法によるWeispfenningの量限定子除去の二次法を決定問題の前処理として使うかどうか |
| "ReducePowers" | Automatic | CAD法の入力で  を  で置換するかどうか．ここで  は系の  のすべての指数のGCDである |
| "RootReduced" | False | 0次元イデアルを形成する等式制約を持つ系の解座標を単独のRootオブジェクトに還元するかどうか |
| "Simplex" | True | 線形不等式系の決定アルゴリズムで，シンプレックス法を使うかどうか |
| "SimplifyInequalities" | Automatic | whether to use the inequality simplification heuristic presented in [25] |
| "ThreadOr" | True | 量限定子を含まない系を解く必要がない場合に，決定問題，最適化，存在記号のQEにおけるそれぞれの選言を別々に解くかどうか． |
| "ZengDecision" | False | [18]で与えられる決定アルゴリズムを使うかどうか |
実多項式系でのReduce，Resolve，FindInstanceの動作に影響を及ぼす
グループのオプション
ARSDecision
オプション
は
Mathematica でAubry，Rouillier，Safey El Dinによるアルゴリズム[
17]を使うかどうかを指定する．このアルゴリズムは，方程式だけを含む決定問題に適用される．このアルゴリズムの方がCAD法よりもよいパフォーマンスを見せる場合もあるが，ランダムに選ばれた方程式系では，著しく劣るようである．従って，これはデフォルトでは使われない．以下の決定問題（文献ではbutcher8と呼ばれる）は，CAD法では1000秒以内に終了しないが，[
17]で与えられるアルゴリズムではかなり速く実行される．
| Out[55]= |  |
BrownProjection
Mathematica のCAD法の実装では，デフォルトでブラウンの向上射影演算子[
8]を使う．この向上により，通常計算は著しくスピードアップする．ブラウンの射影演算子を使うことで，わずかにスピードが遅くなる場合もある．オプション
でブラウンの向上射影演算子を使うかどうかを指定する．最初の例[
21]では，ブラウンの向上射影演算子を使うことでスピードアップしているが，2番目の例では遅くなっている．
| Out[61]= |  |
| Out[65]= |  |
CAD
オプション
は，
Mathematica でCAD法を使ってもよいかどうかを指定する．
が
Falseに設定されていると，CAD法を必要とする計算は，高度に複雑なCAD計算を試みず，直ちに失敗する．CAD法が有効でも，この計算は1000秒以内では終了しない．
| Out[68]= |  |
CADBacksubstitution
デフォルトでは，
Mathematica はCADアルゴリズムに解座標の有理数値を代入し返す．他の数値は代入されない．
| Out[70]= |  |
| Out[71]= |  |
CADBacksubstitution->Trueでは，解座標の数値はすべて代入し返される．
| Out[73]= |  |
| Out[74]= |  |
CADBacksubstitution->Falseでは
Mathematica does はCDAアルゴリズムに座標値を代入しない．
| Out[76]= |  |
| Out[77]= |  |
CADCombineCells
デフォルトでは
Mathematica は，解の公式が同一となっている隣接したセルを結合することによりCADアルゴリズムの結果を簡約化する．ここでは，解集合は結合されていないが，
の解の公式はすべての実数
について同じである．
| Out[79]= |  |
| Out[80]= |  |
| Out[82]= |  |
投影多項式は結合されたセル上で描写できない場合がある．例えば，ここでは
と
は
において共通根を持っているが，区間
の他の点においては共通根を持っていない．
| Out[83]= |  |
CADCombineCells->Falseの場合，
Mathematica はCADセルを結合しない．
| Out[85]= |  |
CADDefaultPrecisionとCADExtraPrecision
Mathematica は
CAD法のリフティング段階で，有効とされた数値計算をデフォルトで使い，数値計算が妥当とされないときだけ，厳密な代数的数の計算に戻る[
14, 24]．オプション
は標本点の座標の計算に使う初期精度を指定する．この精度で実行された計算が妥当とされない場合は，このアルゴリズムは
の値により精度を引き上げる．それでも問題が解決しない場合は，厳密な代数的数の計算に戻る．
と
の値を選ぶことは，数値計算の速度と，精度の損失のためにアルゴリズムが正確な計算に戻る点の数との間のトレードオフである．デフォルト値の100ビットでは，精度損失のためにアルゴリズムが厳密な計算に戻らなければならない場合はほとんどない．
を
Infinityに設定すると，
Mathematica はCAD法のリフティング段階で，厳密な代数的数の計算を使う．以下は，
の設定を最低にすることで最も速く実行する例である（16.2556 (54 ビット)より低い値に設定すると，
は16.2556に設定される）．
CADDefaultPrecision->Infinityとすると，この例は1000秒以内に終了しなかった．
| Out[87]= |  |
| Out[89]= |  |
CADMethod
の設定はCylindricalDecompositionにより使われるCAD計算メソッドを指定する．これはCADアルゴリズムを使う他の関数には影響しない．デフォルト設定のCADMethod->Automaticは設定Directと
を組み合せたものである．
| Out[92]= |  |
| Out[94]= |  |
| Out[96]= |  |
| Out[98]= |  |
CADSortVariables
CAD法のパフォーマンスは，使用される変数の順序に左右されることが多い．変数順序は，解こうとしている問題により解決される面もある．量限定子の変数は，自由変数より先に射影され，最内部の量限定子の変数は最初に射影されなければならないのである．
Reduceと
Resolveで指定される変数は，
が
Trueに設定されていない限り，並べ替えることはできない．しかし，それでも変数順序にいくらかの自由が残される．同一の量限定子の変数および
FindInstanceに与えられた変数は，順序を変えることができるのである．
Mathematica はデフォルトで変数順序のヒューリスティックを使って変数の順序を決定する．ほとんどの場合，そのヒューリスティックでCADのパフォーマンスは向上する．しかし，ヒューリステックが最善の順序を選ばない場合もある．
を
Falseに設定すると，ヒューリスティックを無効にし，使用される変数の順序は量限定子の変数リスト，もしくは
FindInstanceの変数リストの引数で与えられる．以下は，量化された変数の順序を変えなかったら，1000秒以内で終了しない例[
21]である．
| Out[100]= |  |
| Out[102]= |  |
CADZeroTest
厳密な代数的数の座標を持つ標本点が使われると，このオプションの設定がCAD法のリフティング段階に影響を及ぼす．デフォルトでは Mathematica は任意制度の浮動小数点数の座標を持つ標本点を使い，[14, 24]のメソッドを使ってその結果の正当性を立証する．厳密な代数的数の座標を持つ標本点は，近似計算の結果の正当性が立証されない場合か，CADDefaultPrecisionがInfinityに設定されている場合にのみ使われる．
代数的数の座標での標本点で評価された多項式の符号を判定するためには，まず代数的数の数値近似で多項式を評価する．この結果が非零（つまり，ゼロが結果の近似数の誤差範囲内にない）であれば，符号は分かる．そうでない場合は，代数的数での多項式がゼロであるかどうかを検定する必要がある．
オプションの値により，このとき使うゼロ検定法を指定する．値は，
というペアになる．デフォルト値の 
では，Mathematica は式がゼロであればゼロとなるような確度 
を計算する．
ならば，式の値が確度 
まで計算されて，その符号がチェックされる．さもなくば，式はRootReduceを使って単一のRootオブジェクトとして表され，Rootオブジェクトの符号が見付けられる．デフォルト値の 
では，eacc>$MaxPrecisionの場合RootReduceに戻る．
であれば，RootReduceが常に使われる．
ならば，確度 
までゼロである式は零とみなされる．これが最も速いメソッドであるが，他の2つとは異なり，誤った結果を与える可能性がある．それは，非零であってもゼロに近い式がゼロとして扱われている可能性があるためである．
| Out[105]= |  |
以下の例は，30桁確度の数値ゼロ検定を使ったCAD法でより速く実行されている．この例の結果は正確であるが，この
の設定では誤った結果を導くこともある．
| Out[107]= |  |
システムオプションのデフォルト設定では，この例は各段に速く実行できる．
| Out[110]= |  |
EquationalConstraintsCAD
オプションは，CAD法の投影段階で等式制約を使うかどうかを指定する．デフォルト設定のAutomaticでは，Mathematica は[11]で正しいと証明された投影演算子を使う．EquationalConstraintsCAD->Trueでは，[4]で提案された小さいが，証明されていない投影演算子が使われる．
ここではCADアルゴリズムを
EquationalConstraintsCAD->Trueで使い，系を満足するインスタンスを見付ける．解を見付けるために使われるメソッドは証明されていない構想に基づいたものであるが，解は正しいと証明される．つまり入力系を満足する．
| Out[112]= |  |
デフォルト設定の
EquationalConstraintsCAD->Automaticでは，この系の解を見付けるのに幾分長い時間がかかる．
| Out[114]= |  |
EquationalConstraintsCAD->Falseでは，この系の解を見付けるのに，ずっと長い時間がかかる．
| Out[116]= |  |
次では
FindInstanceが系に解がないことを示している．これはCAD法を
EquationalConstraintsCAD->Trueで使っているので，解の正確さは証明されていない推測に基づく．
| Out[118]= |  |
デフォルト設定の
EquationalConstraintsCAD->Automaticでは，系に解がないことを証明するのにもっと長い時間がかかるが，解は正しいことが分かっている．
| Out[120]= |  |
FGLMBasisConversion
Mathematica は0次元イデアル 
を生成する等式制約を持つ系では，ブレブナー基底を使って射影式を見付けるCAD法の変形法を使う．辞書式順序の 
のグレブナー基底が，最後の変数以外のすべての変数に定数係数を持つ線形多項式を含まず，UseNestedRootsがFalseにされているならば，各変数 
について 
に属する 
の一元多項式を見付ける．Mathematica はこれを2つの方法で行う．デフォルトでは，
演算に基づいたメソッドを使う．
をTrueに設定すると，Mathematica は[20]に基づくメソッドを使う．
[
20]に基づくメソッドは，概してやや遅めである．
| Out[125]= |  |
FGLMElimination
オプションは，0次元イデアル 
を生成する等式制約を持つ系に適用できる特殊な場合のヒューリスティックを，Mathematica で使用するかどうかを指定する．このヒューリスティックは，[20]に基づくメソッドを使って，
の中に量化変数のひとつについて線形な（定数係数を持つ）多項式を見付け，除去のためにその多項式を使う．このメソッドは，決定アルゴリズムでもQE法でも使うことができる．デフォルトのAutomatic設定では，「解く」変数が指定されていないResolve，および少なくとも自由変数を2つ持つ系でのみ使うことができる．
これはデフォルトで[
20]に基づく除去法を使い，量限定子を含まない系を未解決の形式で返す．
| Out[128]= |  |
を
Falseに設定すると，この例の計算にかかる時間が長くなり，答は解形式で返される．可読性をよくするために，答の
Nを示す．
| Out[130]= |  |
自由変数が1つしかない場合，
Resolveはデフォルトで[
20]に基づく除去法を使わない．可読性をよくするために，答の
Nを示す．
| Out[132]= |  |
を
Trueに設定すると，この例の計算にかかる時間が長くなり，答は未解決の形式で返される．
| Out[134]= |  |
GenericCAD
Mathematica は[13]で記述されたCAD法の簡約化バージョンを使って，決定問題を解き，方程式を含まない実多項式系の解を求める．このメソッドは解を求め，系の不等式すべてが厳密（
または 
）である場合に解がないことを証明するものである．このメソッドは弱い（
または 
）不等式を含む系にも使うことができる．しかし，その系の厳密な不等式バージョンに解がないことが証明すると，もとの系に解があるかどうかを判別するためにCAD法が必要になる．システムオプション
は，Mathematica でこのメソッドを使うかどうかを指定する．
ここでは
法が系の厳密な不等式バージョンの解を見付ける．
| Out[136]= |  |
なしでは，系の解を見付けるのにもっと時間がかかる．
| Out[138]= |  |
この系には解がなく，弱い不等式を含んでいる．
法がこの系の厳密な不等式バージョンの解を見付けなかったら，
Mathematica は完全なCAD法を実行して，解がないことを証明する必要がある．
| Out[140]= |  |
同じ例を
GenericCAD->Falseで実行すると，上の
の計算で使った時間を節約することができる．
| Out[142]= |  |
以下の系は厳密な不等式しか含んでいないので，
は系に解がないことを証明することができる．
| Out[144]= |  |
を使わないと，系に解がないことを証明するのにずっと長時間かかる．
| Out[146]= |  |
GroebnerCAD
0次元イデアルの 
を生成する等式制約のある系には，Mathematica はグレブナー基底を使って射影式を求めるCADの変形法を使う．
をFalseと設定すると，Mathematica は標準のCAD射影を使う．
GroebnerCAD->Falseと設定すると，この例の実行時間はずっと遅くなる．
| Out[148]= |  |
| Out[150]= |  |
| Out[151]= |  |
LinearDecisionMethodCrossovers，LWDecision，Simplex
この3つのオプションは，決定問題を解くため，または線形方程式および不等式の系の解の例を見付けるために使われる．利用可能なメソッドにはLoos-Weispfenning法[15]，シンプレックス法，改訂シンプレックス法がある．この3つのメソッドはすべて，有理係数および浮動小数点数係数を持つ系を扱うことができる．厳密な非有理係数を持つ系では，Loos-Weispfenning法だけが実装される．
はLoos-Weispfenning法が使用可能かどうかを指定する．
はシンプレックス法と改訂シンプレックス法が使えるかどうかを指定する．
は，すべてのメソッドが使用可能，適用可能である場合に，どのメソッドを使うかを決定する．オプションの値は
が必要である．Mathematica では，
変数までの線形系には，Loos-Weispfenning法[15]が使われる．
から 
変数の系にはシンプレックス法が，
変数より多い系には改訂シンプレックス法が使われる．シンプレックス法が使われる場合，不等式の数が変数の数の 
倍に満たないとき，
がTrueかAutomaticのとき，系が厳密なときは，スラック変数が使われる．デフォルト値は 
，
，
，s==Automaticである．
3元の線形系の解を見付けるときは，デフォルトではシンプレックス法が使われる．
| Out[153]= |  |
| Out[155]= |  |
ここではLoos-Weispfenning法が使われている．
| Out[157]= |  |
以下でLoos-Weispfenning法が使われているのは，シンプレックス法と改訂シンプレックス法は厳密な非有理係数を持つ系には実装されないためである．
| Out[159]= |  |
| Out[161]= |  |
LinearEquations
オプションは，定数の主係数を持つ線形等式制約を変数除去のために使用するかどうかを指定する．この設定は一般にアルゴリズムのパフォーマンスを向上させる．このオプションは，「純粋な」CADベースの決定アルゴリズムの実験を可能にするために提供されている．
ここで
Mathematica は，CADを使って結果となる2変数の系の解を求める前に，第一方程式を使って
を除去する．
| Out[163]= |  |
ここでは，
Mathematica はCADを使ってもとの3変数の系の解を求めている．
| Out[165]= |  |
LinearQE
オプションは，系のすべての方程式および不等式のなかで最も線形に現れる最内部の量限定変数を，少なくとも1つ含む系を扱うために使われる．オプション設定は，決定問題の解決には影響を与えない．デフォルト設定のTrueでは，Mathematica はLoos-Weispfenning法[15]を使って，系で線形にのみ現れる量限定変数をすべて除去する．その後，量限定子が残っている場合，あるいは結果を自由変数について解く必要がある場合は，CAD法が使われる．LinearQE->Automaticと設定すると，Loos-Weispfenning法は，系で定数係数を持ち，線形にのみ現れる変数に対してのみ使われる．LinearQE->Falseとすると，Loos-Weispfenning法は使用されない．
デフォルト設定の
LinearQE->Trueでは，
と
の両方を除去するためにはLoos-Weispfenning法が使われ，二変数の量限定子を含まない残りの系を解くためにはCAD法が使われる．
| Out[167]= |  |
LinearQE->Automaticと設定すると，
を除去するためだけにLoos-Weispfenning法が使われ，三変数の残りの系を解くためにはCADが使われる．この例では，デフォルトのメソッドの方がずっと速い．
| Out[169]= |  |
LinearQE->Falseと設定すると，Loos-Weispfenning法は使われない．
ReduceではCAD法を使って，四変数のもとの系が解かれるが，この例ではずっと長い時間がかかっている．
| Out[171]= |  |
| Out[172]= |  |
以下は，デフォルトメソッドの方が速くない場合の例である．デフォルト設定の
LinearQE->Trueでは，
と
の両方を除去するためにLoos-Weispfenning法が使われ，量化変数と自由変数をそれぞれ1つずつ持つ残りの系を解くためにはCAD法が使われる．今回は，デフォルトメソッドが最高速ではない．
| Out[174]= |  |
LinearQE->Automaticとすると，
を除去するためだけにLoos-Weispfenning法が使われ，量化変数2つと自由変数1つを持つ残りの系を解くためにはCAD法が使われる．
| Out[176]= |  |
LinearQE->Falseと設定すると，系を解くのにCAD法が使われる．この例では，この訃報が一番速い．
| Out[178]= |  |
デフォルト設定の
LinearQE->Trueでは，すべての量化変数が系で線形にのみ表れ，系の量限定子を含まないバージョンを解形式で与える必要のない量限定子除去問題では，確実に有利である．これは，すべての変数の数で二重に指数関数的に増大するCAD法の複雑性とは異なり，Loos-Weispfenning法の複雑性が自由変数の数にはほとんど依存していないためである．
LinearQE->False，
QuadraticQE->Falseと設定すると，この例は1000秒では終了しない．
| Out[180]= |  |
LWPreprocessor
オプション設定は，決定問題の解決と例の探索に影響を与える．このオプションは，結果の系にCAD法を適用する前に，Loos-Weispfenning法[8]を使って，すべての等式および不等式で最も線形に現れる変数を除去するかどうかを指定する．デフォルト設定のAutomaticでは，Mathematica はLoos-Weispfenning法を使って，定数係数を持ち，線形にのみ現れる変数を除去する．LWPreprocessor->Trueとすると，Loos-Weispfenning法は線形にのみ現れる変数すべてに使用される．LWPreprocessor->Falseでは，Loos-Weispfenning法はCADベースの決定法の前処理として使用されない．
デフォルト設定の
LWPreprocessor->Automaticでは，Loos-Weispfenning法は
を除去するためだけに使用され，三変数の残りの系の解を求めるためにはCAD法が使われる．
| Out[181]= |  |
LWPreprocessor->Trueと設定すると，
と
の両方を除去するためにLoos-Weispfenning法が使われ，二変数を持つ残りの系の解を求めるためにはCAD法が使われる．以下の例では，このメソッドはデフォルトのものより遅い．
| Out[183]= |  |
LWPreprocessor->Falseとすると，CAD法は四変数を持つ持つの系の解を見付けるために使われる．この例では，このメソッドはデフォルトと同じくらいの速さである．
| Out[185]= |  |
以下の例は，最後の不等式が等式になっていること以外，前の例と同じである．デフォルトの
LWPreprocessor->Automaticでは，Loos-Weispfenning法は
を除去するためだけに使われ，3変数の残りの系の解を見付けるためにはCAD法が使われる．
| Out[187]= |  |
LWPreprocessor->Trueとすると，Loos-Weispfenning法は
と
の両方を除去するために使われ，二変数の残りの系の解を見付けるためにはCAD法が使われる．改訂したこの例では，このメソッドの方がデフォルトよりも速い．
| Out[189]= |  |
LWPreprocessor->Falseと設定すると，CADアルゴリズムは4変数のもとの系の解を見付けるために使われる．改訂したこの例では，このメソッドの方がデフォルトよりも7倍遅くなっている．
| Out[191]= |  |
ProjectAlgebraic
オプションの設定は，CAD法の代数的数の係数の取扱いに影響を及ぼす．
入力系の係数で見付かった代数的数は，新しい変数で置き換えられる．この新しい変数は常に変数順の最初に置かれるので，CAD法の投影段階では最後に除去される．現在の射影式に 
個の変数が含まれており，少なくとも最初の 
個が代数的数の係数に取って代る場合，射影を継続するかどうかを選ぶことができる．射影段階を継続しない場合は，それぞれの変数が対応する代数的数の係数に等しいという関係が成り立つ，最初の
個の変数の0次元セルを拡張するリフティング段階を開始することができる．最後の 
の射影を計算することを選択した場合は，リフトされている変数に当たる代数的数の係数が射影式の根の間に存在することが，リフティング段階で分かる．従って，この変数については0次元セルを有理数の標本点で拡張することになる．このように，最後の
の射影の計算を避けることと，標本点での代数的数による座標を避けることとの間には，トレードオフがある．
ProjectAlgebraic->Trueと設定すると，残りの変数が1つになるまで，代数的数による係数を置換する変数について射影段階が続く．ProjectAlgebraic->Falseと設定すると，代数的数による係数を置換しない変数が1つ残ると同時に，射影段階が終了する．デフォルト設定のProjectAlgebraic->Automaticでは，代数的数の係数を置換しない変数が多くて1つ残っており，少なくとも3つの射影式または射影変数の次数が2より大きい射影式がある場合に，射影段階が終了する．
系に方程式，不等式および高次の代数的数の係数がほとんどない場合は，
ProjectAlgebraics->Trueを使った方がよいだろう（
N はよりよい可読性のために出力に適用される）．
| Out[196]= |  |
| Out[198]= |  |
低次の代数的数の係数，方程式，不等式が系に多く含まれる場合は，
ProjectAlgebraics->Falseとした方が速い．
| Out[200]= |  |
| Out[202]= |  |
ProveMultiplicities
の設定は，CAD法のリフティング段階で任意精度の浮動小数点数（Mathematica の"bignum"）計算（詳細は[14, 24]を参照）を使って得た投影多項式の多根および主係数0を証明する方法を決定する．デフォルト設定のProveMultiplicities->Trueでは，Mathematica はセルの原点についての情報を使う．これで十分ではない場合は，セル座標の厳密値を計算し，部分終結式の主係数と厳密な零検定を使う．これで失敗したときのみ，厳密計算に戻る．ProveMultiplicities->Automaticでは，Mathematica はセルの原点の情報を使い，それで十分でない場合は厳密計算に戻る．ProveMultiplicities->Falseでは，無限桁の整数の計算がすべての根の分離に失敗するたび，あるいは投影多項式の主係数が非零であることを証明するのに失敗するたびに，Mathematica は厳密計算に戻る．
一般に，任意精度の浮動小数点数で得られた結果を証明するために利用できるメソッドすべてを使うと，よりよいパフォーマンスが得られる．
| Out[205]= |  |
| Out[207]= |  |
| Out[209]= |  |
QuadraticQE
オプションは，仮の代入アルゴリズム[22, 23]によるWeispfenningの量限定子除去の二次形式を使って，系のすべての方程式および不等式で最大でも二次的に現れる量化変数を除去するかどうかを指定する．すべての変数の数において二重指数的であるCAD法の複雑さとは異なり，Weispfenningのアルゴリズムの複雑さは，自由変数の数にはほとんど依存しない．従って，すべての量限定子がこのアルゴリズムを使って除去できる場合，多数の自由変数が存在する場合，量限定子を含まないタイプの系が解形式で与えられる必要のない場合には，これを使った方が確実によい．しかしながら，Weispfenningのアルゴリズムを使って変数を除去すると，式の大きさを顕著に大きくしてしまうので，Mathematica が結果にCADを適用しなければならない場合や系にほとんど自由変数が含まれていない場合は，もとの系にCADを使った方が速い． デフォルト設定のAutomatic,では，Mathematica は変数の指定されていない，あるいは少なくとも2つの変数のあるResolve，および1つの変数の除去が系のLeafCountを最大でも二倍にする限りにおいて少なくとも3つの変数を持つReduceとResolveに対してこのアルゴリズムを使う．この分類はかなりうまくいくようであるが，これが最適のアルゴリズムとはならない場合もある．オプション値を変更することで，非常に長時間かかるであろう問題を解くことができる場合がある．QuadraticQE->Trueという設定では，除去しなければならない二次変数がある場合は常にWeispfenningのアルゴリズムが使われ，QuardaticQE->Falseでは使われない．
変数が指定されていない，あるいは少なくとも2つのパラメータを持つ
Resolveでは，
を除去するのにWeispfenningのアルゴリズムが使われる．結果はパラメータ
，
，
について解かれない．
| Out[211]= |  |
この
Reduceの例についてはデフォルトでCAD法が使われる．結果はパラメータ
，
，
について解かれる．
| Out[212]= |  |
QuadraticQE->Trueと設定すると，
Reduceで
を除去するのにはWeispfenningのアルゴリズムが，パラメータ
，
，
に対する量限定子のない式を解くのにはCAD法が使われる．この例では，はじめからデフォルトメソッドのCADを使うよりも速い．
| Out[214]= |  |
3つの自由変数を持つこの系では，Weispfenningのアルゴリズムの方がCAD法よりもずっと速いい．
| Out[216]= |  |
| Out[218]= |  |
自由変数が1つしかないこの系では，
ResolveでCAD法が使われる．
| Out[219]= |  |
ここではWeispfenningのアルゴリズムの方が時間がかかり，結果も複雑である．
| Out[221]= |  |
QVSPreprocessor
オプション設定は，決定問題を解く場合とインスタンスを見付ける場合に影響する．このオプションは，結果となる系にCADアルゴリズムを適用する前にすべての方程式および不等式で最大で二次で現れる変数を除去するために，仮の代入アルゴリズム[22, 23]によるWeispfenningの量限定子削除の二次形式を使うかどうかを指定する．デフォルト設定はFalseであり，このアルゴリズムは使用されない．前処理としてWeispfenningのアルゴリズムを使うことでパフォーマンスが顕著に向上する例もあるし，前処理を使うことによりパフォーマンスが著しく低下する例もある．前処理は多数の変数がある例やインスタンスが存在する例で効果を発揮する傾向がある．QVSPreprocessor->Trueと設定すると，二次変数があるたびにWeispfenningのアルゴリズムが使われ，QVSPreprocessor->Automaticと設定すると，少なくとも4つの変数を持つ系に対してこのアルゴリズムが使われる．
ここでは
Mathematica はWeispfenningのアルゴリズムを前処理として使い，解を求めている．前処理がないと，ずっと時間がかかる．
| Out[224]= |  |
| Out[226]= |  |
| Out[228]= |  |
| Out[230]= |  |
ReducePowers
CAD法の入力に含まれる変数 
は，その系に表れる 
のすべてのベキ乗が整数 
の整数倍である場合，Mathematica は入力系の 
を新しい変数で代替し，新しい系でCAD法を実行してから，もとの変数で表現されるように解を求める．ReducePowers->Falseと設定すると，このショートカットがオフになる．ReducePowers->Falseという設定では，CAD法の出力におけるセルの範囲として現れる代数関数は，常に有理関数，二次無理式，Rootオブジェクトのいずれかになる．デフォルトのReducePowers->Trueでは，これに加えて，以前の任意の式 
に対しては 
，整数 
および有理関数または二次無理式 
に対してはRoot[a#n-e&, 1]となることがある．
デフォルト設定の
ReducePowers->Trueでは，CAD法は
と
に代る変数で二次方程式を解き，結果を
および
で表す．結果には，内部に二次無理式を持つ
Rootオブジェクトが含まれている．
| Out[231]= |  |
ReducePowers->Trueと設定すると，CAD法は50次方程式をそのまま解くので，上より時間が長くかかる．結果には，内部に多項式を持つ
Rootオブジェクトが含まれている．
| Out[233]= |  |
RootReduced
0次元イデアル 
を生成する等式制約を含む系では，Mathematica はグレブナー基底法を使って射影多項式を求めるCAD法の変形を使う．
の辞書式順序のグレブナー基底に，最後の変数以外のすべての変数（一般に真である）に定数係数を持つ線形多項式が含まれている場合，解の座標すべてが最後の座標の多項式で簡単に表される．それ以外の場合は，座標は三角方程式系によって定義された代数的数を表すRootオブジェクトとして与えられる．
をTrueに設定すると，Mathematica は各座標を，最小の多項式と根の数によって定義された1つの数値的なRootオブジェクトとして表す．この簡約表現の計算は，系を解くよりも格段に時間がかかることが多い．
デフォルトでは，
で表現された
の値を得る．
| Out[234]= |  |
| Out[235]= |  |
RootReduced->Trueと設定すると，
Mathematica は
の値を1つの
Rootオブジェクトとして表す．しかし計算にはもっと時間がかかる．
| Out[237]= |  |
デフォルトでは，
Reduceは三角方程式系により定義された代数的数を表す
Rootオブジェクトで解を表す．
| Out[239]= |  |
RootReduced->Trueと設定すると，
Mathematica は
の値を，最小多項式と根の数によって定義された
Rootオブジェクトとして表す．しかし，計算にはより時間がかかる．
| Out[241]= |  |
SimplifyInequalities
デフォルト設定のSimplifyInequalities->Automaticでは，Mathematica は[25]で提示されている不等式の簡約化ヒューリスティックを使ってCADアルゴリズムへの入力を簡約化し，CADの投影因子の不等式を推定する．その後，その不等式を使って投影段階で非零の係数と部分終結式を認識し，リフティング段階でセルを削除する．ヒューリスティックは仮想代入アルゴリズム[15, 23]の中間結果を簡約化するのにも使われる．SimplifyInequalitiesをTrueに設定すると，不等式簡約化ヒューリスティックが追加の変換 
を実行する．SimplifyInequalities->Falseでは，不等式簡約化ヒューリスティックは使われない．
次の例では不等式簡約化によりCADの計算が速くなっている．
| Out[243]= |  |
| Out[245]= |  |
最初の例では方程式の因数分解でCAD計算が速くなっており，2つ目の例ではCAD計算が遅くなっている．
| Out[250]= |  |
| Out[252]= |  |
ThreadOr
オプション
は，決定アルゴリズム（自由変数あるいはパラメータを含まない系ではReduceとResolve），FindInstance，QE（変数指定のないResolve)において，以下の恒等式
をどのように使うかを指定する．デフォルト設定のThreadOr->Trueでは，恒等式(8)は解法を試みる前に使われる．ThreadOr->Falseとすると，恒等式(8)はその使用を必要とするアルゴリズム（シンプレックス法等）によって使われることがある．しかし，その使用を必要としないアルゴリズム（CAD法等）では使われない．
以下で
Reduceは
Orの簡単な第1項目を指定する例を見付けるため，これより複雑な第二項を扱わない．
| Out[253]= |  |
| Out[255]= |  |
以下の系には解がないので，
ThreadOr->Trueと設定すると
Reduceは各項にCADベースの決定法を実行する必要がある．
| Out[257]= |  |
Orの6項すべてに全く同じ多項式が含まれているので，式全体にCADベースの決定法を実行することは，1つの項にCADベースの決定法を実行するのと非常に類似した計算となる．この場合，
ThreadOr->Falseで計算した方が速い．
| Out[259]= |  |
ZengDecision
オプションは，
Mathematica でG. X. ZengとX. N. Zeng[
18]によるアルゴリズムを使うかどうかを指定する．このアルゴリズムは，1つの厳密な不等式からなる系についての決定問題に適用される．このアルゴリズムが，[
13]で記述されているCAD法の厳密ない不等式の変形よりもうまく動作する例がある．しかし，ランダムに選ばれた不等式ではパフォーマンスが劣るため，デフォルトでは使用されない．以下に挙げるのは，
ZengDecision->Trueと設定した方がわずかに速く実行される[
18]からの例である．
| Out[261]= |  |
| Out[263]= |  |
参考文献
[1] Caviness B. F. and J. R. Johnson, eds. Quantifier Elimination and Cylindrical Algebraic Decomposition: Texts and Monographs in Symbolic Computation. Springer-Verlag (1998)
[2] Tarski A. A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)
[3] Łojasiewicz S. Ensembles Semi-Analytiques. Inst. Hautes Études Sci. (1964)
[4] Collins G. E. "Quantifier Elimination for the Elementary Theory of Real Closed Fields by Cylindrical Algebraic Decomposition" Lecture Notes in Computer Science 33 (1975): 134-183
[5] Hong H. "An Improvement of the Projection Operator in Cylindrical Algebraic Decomposition" In Issac '90: Proceedings of the International Symposium on Symbolic and Algebraic Computation (M. Nagata, ed.), 261-264, 1990
[6] McCallum S. "An Improved Projection for Cylindrical Algebraic Decomposition of Three Dimensional Space" J. Symb. Comput. 5, no. 1/2 (1988): 141-161
[7] McCallum S. "An Improved Projection for Cylindrical Algebraic Decomposition" In Quantifier Elimination and Cylindrical Algebraic Decomposition: Texts and Monographs in Symbolic Computation (B. F. Caviness and J. R. Johnson, eds.). Springer-Verlag, 242-268, 1998
[8] Brown C. W. "Improved Projection for Cylindrical Algebraic Decomposition" J. Symb. Comput. 32, no. 5 (2001): 447-465
[9] Collins G. E. "Quantifier Elimination by Cylindrical Algebraic Decomposition—Twenty Years of Progress" In Quantifier Elimination and Cylindrical Algebraic Decomposition: Texts and Monographs in Symbolic Computation (B. F. Caviness and J. R. Johnson, eds.). Springer-Verlag, 8-23, 1998
[10] McCallum S. "On Projection in CAD-Based Quantifier Elimination with Equational Constraint" In Issac '99: Proceedings of the International Symposium on Symbolic and Algebraic Computation (Sam Dooley, ed.), 145-149, 1999
[11] McCallum S. "On Propagation of Equational Constraints in CAD-Based Quantifier Elimination" In Issac 2001: Proceedings of the International Symposium on Symbolic and Algebraic Computation, 223-231, 2001
[12] Strzebonski A. "An Algorithm for Systems of Strong Polynomial Inequalities" The Mathematica Journal 4, no. 4 (1994): 74-77
[13] Strzebonski A. "Solving Systems of Strict Polynomial Inequalities" J. Symb. Comput. 29, no. 3 (2000): 471-480
[14] Strzebonski A. "Cylindrical Algebraic Decomposition Using Validated Numerics" Paper presented at the ACA 2002 Session on Symbolic-Numerical Methods in Computational Science, Volos, Greece (2002) (Notebook with the conference talk available at members.wolfram.com/adams)
[15] Loos R. and V. Weispfenning. "Applying Linear Quantifier Elimination" Comput. J. 36, no. 5 (1993): 450-461
[16] Strzebonski A. "A Real Polynomial Decision Algorithm Using Arbitrary-Precision Floating Point Arithmetic" Reliable Comput. 5, no. 3 (1999): 337-346; Developments in Reliable Computing (Tibor Csendes, ed.). Kluwer Academic Publishers (1999): 337-346
[17] Aubry P., F. Rouillier, and M. Safey El Din. "Real Solving for Positive Dimensional Systems" J. Symb. Comput. 34, no. 6 (2002): 543-560
[18] Zeng G. X. and X. N. Zeng. "An Effective Decision Method for Semidefinite Polynomials" J. Symb. Comput. 37, no. 1 (2004): 83-99
[19] Akritas A. G. and A. Strzebonski. "A Comparative Study of Two Real Root Isolation Methods" Nonlinear Analysis: Modelling and Control 10, no. 4 (2005): 297-304
[20] Faugere J. C., P. Gianni, D. Lazard, and T. Mora. "Efficient Computation of Zero-Dimensional Gröbner Bases by Change of Ordering" J. Symb. Comput. 16, no. 4 (1993): 329-344
[21] Dorato P., W. Yang, and C. Abdallah. "Robust Multi-Objective Feedback Design by Quantifier Elimination" J. Symb. Comput. 24, no. 2 (1997): 153-159
[22] Weispfenning V. "Quantifier Elimination for Real Algebra—The Cubic Case" In Issac 1994: Proceedings of the International Symposium on Symbolic and Algebraic Computation, 258-263, 1994
[23] Weispfenning V. "Quantifier Elimination for Real Algebra—The Quadratic Case and Beyond" Appl. Algebra Eng. Commun. Comput. 8, no. 2 (1997): 85-101
[24] Strzebonski A. "Cylindrical Algebraic Decomposition Using Validated Numerics" J. Symb. Comput. 41, no. 9 (2006): 1021-1038
[25] Brown C. W. and A. Strzebonski. "Black-Box/White-Box Simplification and Applications to Quantifier Elimination" In Issac 2010: Proceedings of the International Symposium on Symbolic and Algebraic Computation (Stephen M. Watt, ed.), 69-76, 2010
[26] Strzebonski A. "Computation with Semialgebraic Sets Represented by Cylindrical Algebraic Formulas" In Issac 2010: Proceedings of the International Symposium on Symbolic and Algebraic Computation (Stephen M. Watt, ed.), 61-68, 2010
[27] Strzebonski A. "Solving Polynomial Systems over Semialgebraic Sets Represented by Cylindrical Algebraic Formulas" In Issac 2012: Proceedings of the International Symposium on Symbolic and Algebraic Computation (Joris van der Hoeven and Mark van Hoeij, eds.), 335-342, 2012
は
のセル，
は連続の代数関数，
と 
は連続の代数関数，
，
のいずれかであり，
では 
が成り立つ．
