前提知識

Quolifier Eliminationの理解のために、以下のサイトを読んでいく
- An Introduction to Quantifier Elimination by Cylindrical Algebraic Decomposition
- CiNiiで検索してもCAD = Cylindrical Algebraic Decompositionには日本語の定訳は無いようだった
出てきた用語
- 実閉体
- 原子論理式

量化記号消去問題

実閉体の理論において式の変数というものはいくつかの実閉体の要素である
原子論理式は、それらの変数の多項式の符号条件である
式 $F$ が与えられると、quantifier elimination問題は限量子記号がない式$\overline{F}$を要求する
それは$F \Harr \overline{F}$のようなもので、式 $F$ を入力式、$\overline{F}$ を解式と呼ぶ

要は限量子記号をもつ式を、それと同値な限量子記号がない式に変換するということか
限量子記号とは・・・

全称量化記号 (universal quantifier) と呼ぶ記号 ∀

存在量化記号 (existential quantifier) と呼ぶ記号 ∃

だった

単純で馴染みのある量化記号消去問題の入力式の例は次のとおりです。
$F: (\exist_x) [ ax^2 + bx + c ]$

↑ $ax^2 + bx + c$ を満たす$x$が存在する

この量化記号消去問題の1つの解法は、次のとおりです。
$\overline{F}: b^2 -4ac \geq 0 \space \land [ b \neq 0 \lor a \neq 0 \lor c = 0 ]$

入力式 $F$は、ある意味で次の質問をしていることになります。二次多項式はどういう条件で実数の根を持つのですか？出力式 $\overline{F}$はこの質問に答えます。

量化記号消去法の来歴

1930年代に、A. Tarskiは、その構築のためのアルゴリズムを与えることによって、任意の入力式に解の式が存在することを証明しました。残念ながら、この方法の計算コストは、些細な問題を除いて実用的ではありませんでした。
1973年にコリンズは、柱形代数分解（CAD）に基づくまったく新しい方法を発見しました。これは、以前のどのアプローチよりもはるかに効率的でした。この方法では、最悪計算量として $F$ に含まれる変数の数の二重指数関数時間の時間計算量になる。

$O(2^{2^{x}})$ 時間？

しかし、$F$の多項式の数、$F$の多項式の程度、$F$の係数のbit長、$F$の原始論理式の数によっては多項式時間で処理できる。この方式はこれまでに様々な方法で改良され、実装され、重要な問題を解く能力があることを示しています。

コリンズの柱形代数分解（CAD）ベースのアルゴリズムの導入から、その他にもQEの解法は提案されました。
RenegarとHeintzの手法は変数の数ではなく数量子の変更数に対して二重指数関数時間の計算量でした。RenegarはQEのアルゴリズムに対してGrigor'ev'sの決定手続きが拡張可能であると主張しました。
Renegarよりは劣りますが、Weispfenningはグレブナー基底の把握とPedersen, Roy, そして Szpirglasの業績を元にしたQEに対する新たなアプローチを導入しました。漸近解析は行われませんでした。

他の研究は、実閉体の完全な理論の制限の考慮に焦点を当てています。

例えばWeispfenningは束縛変数は線形的にしか式に現れないことを考えました。

$$( \exists_x) [ a_2 x^2 + a_1 x + a_0 = 0 \land F' ]$$

$F'$ は量化記号自由式です。Weispfenningは、量化記号がついた変数が最大で3次的に現れる特定の式を攻略する(=attacking?)方法を開発しました。この方法は実装されており、CADベースの方法では実用的ではない多くの問題にうまく対処しています。その複雑度は$F$中の自由変数の数に依存しません、このことは多くの問題で有用です。彼はまた、この方法を完全な理論に拡張する方法、つまり多項式の次数(=degree)の制限がないことを示しています。

量化記号消去問題は、変数の数において本質的に二重指数関数時間の計算量です。したがって、完全な理論のアルゴリズムは、これらの範囲内で機能する必要があります。課された最悪時間計算量にもかかわらず、多くの重要な問題が妥当な時間内に解決できることが期待されています。私の目標は、CADアルゴリズムを改善して、その実用的な適用範囲を拡大することです。

ここまで、以下のページの翻訳