Splitting on Demand in SAT Modulo Theories http://homepage.cs.uiowa.edu/~tinelli/papers/BarNOT-LPAR-06.pdf
Reluplex論文を読んでて[1]、on-demand splitting の形式化はどうするものなのだろうなと気になって、 もともと自分のtoysmtでもその辺りのAPI設計をどうするのが良いのかなと悩んでいたというのもあり、 読んでみた。
on-demand splitting とは、例えば配列の理論のソルバで read(write(A,i,v),j) = read(A,j) みたいな制約があったときに、これが成り立つのが i≠j だからなのか read(A,i)=v だからなのかで場合分けして処理したいけど、理論ソルバ内で場合分けするのは大変なので、オンデマンドで read(write(A,i,v),j) ≠ read(A,j) ∨ i≠j ∨ read(A,i)=v のような論理式を追加して、SATソルバ側で場合分けさせよう、というような話。
ただし、一般に新たな原始論理式、元の論理式に現れていなかった定数記号を含む論理式を追加したいので、正当性の定義や停止性がちょっと複雑になる。 前者に関してはequivalenceからequi-satisfiabilityにしたり、後者に関しては新たに追加される可能性のあるリテラルの有限集合を定義して、その範囲でしか追加しないことにして停止性を保証するなど。
また、ちょっと意外で面白かったののは、複数の理論を扱う際に、結合した理論ソルバで考えるだけでなく、 theory combination 自体にも踏み込んで、delayed theory combination (DTC) 的な手法(?)を同じ枠組みで扱っている点。
そういえば、この論文はLPAR2006 [2]の論文で、SMTの基礎の主要な論文って2000年代前半からこれくらいの時期までにほぼ出ていて、考えてみたらそれから10年経っているんだよなぁ。
[1] https://plus.google.com/+MasahiroSakai/posts/913ZviJ4iVR
[2] https://www.lix.polytechnique.fr/~hermann/LPAR2006/