Beautiful Interpolants - tozima's blog

by Aws Albarghouthi and Kenneth L. McMillan

良い interpolant を計算するための手法の提案。

概要

Interpolant は SMT ソルバの証明から抽出することができるが、従来の DILL(T) を基盤とする SMT ソルバの返す証明（およびそこから抽出される interpolant）は複雑になりがちという問題があった。この論文では、簡単な論理式による interpolant を与える手法を提案している。

基本となるのは $A \Rightarrow I$ かつ $I \Rightarrow \neg B$ を満足する「簡単な」述語 $I$ が存在するかどうかというクエリであり、これを繰り返すことで interpolant を見つける。簡単な述語の例としては、half-space $a_1 x_1 + a_2 x_2 + \dots + a_n x_n \le b$ という形の論理式が挙げられている。ここで $x_1, \dots, x_n$ は変数で、 $a_1, \dots, a_n, b$ は述語を特徴づけるパラメータ（＝述語にとっては定数）である。「この形の論理式で interpolant が存在するか」という問題は Farkas の補題というものを用いることで普通の線形計画問題（の解の存在判定）に帰着することができ、効率的に計算することができる。

$A, B$ がもう少し複雑な形の場合、例えば $A = \bigvee_{i \in I} A_i$ かつ $B = \bigvee_{j \in J} B_j$ のような形の場合についても議論されている。原理的には各 $(i,j) \in I \times J$ について上記手順で half-space による interpolant $a_1^{i,j} x_1 + \dots + a_n^{i,j} x_n \le b^{i,j}$ を求めればその Boolean combination が interpolant になるが、それでは interpolant が複雑過ぎるので、できるだけ多くの $(i,j)$ の組で一つの half-space を共通して使うように計算する手法が提案されている。

感想

名前だけは知っていたが、読んだことはなかった論文。読んだ感想としては、あまりの驚きの無さにショックであった。歴史的な背景はきちんと追えていないのだが、もしかしたらこの論文が template-based で Farkas's Lemma を使う推論手法そのものの初出なのかもしれない。そうだとすれば、この論文に驚きがないのは手法が既に業界に広く知られているからであって、驚きがないことが偉大な論文ということになるだろう。