A Fast Linear-Arithmetic Solver for DPLL(T)
概要
問題をヒューリスティックスを用いて簡単化し、問題の大きさを小さくできる
theory propagation の効率的な手段を提供する
厳格な不等式（<, > のこと）の問題を解くための簡単な方法を提供する
incremental な Simplex 法をベースとしている
与えられた問題が論理的な組合せで表現されている場合（and, or が入っているとか）、そのようなものは対応する理論ソルバと SAT ソルバを合わせて使うことで解くことができる（つまり、従来のように理論ソルバに食わせるのは SAT ソルバでその制約が成り立つものであるかどうか判定した後でよい）。
conflict の原因となったものとは、その conflict を起こすために同時に成り立つことが必要となる原子論理式の集合であればよい。
assert された原子論理式の集合を $ \alphaで表す。
与えられた制約に表れる原子論理式の集合を$ \mathcal{A}で表す。
Theory solver は次のような API を実装しているものとする。
type Unsat = Subset<α>
Assert(γ : Atom) -> Either<"ok", Unsat>
sound である必要はあるが、complete である必要はない。つまり、前提が真ならそこから導かれる結論がいつでも真である必要はあるが、恒心であるものをいつでも真であるとする必要はない。
Check() -> Either<"ok", Unsat>
"ok" が返されたときに新しい checkpoint が作られる
sound かつ complete である必要がある
これによって作成された checkpoint と、backtrack 後の状態は同値である必要があるが、すべて一緒である必要はない。
Backtrack() -> void
一番最近の checkpoint に backtrack する
Propagate() -> Array(Pair(Subset<α>, Atom))
theory propagation を行い、まだ assert されていないが現在の α のサブセット Γ から導出でき、かつ制約に含まれているような原子論理式を Atom として返す
sound である必要はあるが、exhausive である必要はない。つまり、前提が真ならそこから導かれる結論がいつでも真である必要はあるが、そのようなものすべてを必ず列挙しないといけないということはない。
Incremental な Simplex 法を用いたアルゴリズムは、与えられた制約を適切に equisatisfiable な形に書き換えることによって避けることができる。その方法は非常に単純であり、既に変数ではないような線形算術の項 $ t_i\ R\ bの左側に現れるものを新しい変数で置換する。
Simplex ソルバーが持つ状態
各変数の値$ \beta(x_i)
初期値 0
各 nonbasic 変数の上限$ u_j
初期値$ +\infty
各 nonbasic 変数の下限$ l_j
初期値$ -\infty
タブロー
各 basic 変数$ x_iについて、その変数を nonbasic 変数$ x_jで$ x_i = \sum_{x_j \in \mathcal{N}}a_{ij}x_jとして表すやつ
初期値$ Ax=0に対応する形で保持