2013年08月15日

SMTソルバでプログラムを作る

ICFP programming contest 2013に参加していました(よくわかる解説)。チームの成績は戦略ミスなどもあって散々だったのですが、ちょっと変わったアプローチで問題に取り組んだと思うので、自分のチームのアプローチを紹介しておきます。リポジトリはこちら

なにを達成したいか

Knuth本やHacker's delight に紹介されているプログラミング技術の一つとして、bit trickが挙げられます。たとえば、整数xのビット表現のうち、一番右にある1をクリアするコードは "x & (x - 1)" として記述できます。このようなコードを、仕様から直接導出することはできるでしょうか? あるいは、有限個の入出力(Oracleと呼ぶことにします)が与えられた場合、その入出力を満たすようなプログラムを生成することは出来るでしょうか? これらの疑問に答えるのが、Jha, Gulwani, Tiwari らの研究です。[1,2]

どうすれば解けたことになるか

適当な仮想マシンを想定し、そのバイトコードの並びを考えてみます。たとえば、「整数xのビット表現のうち、一番右にある1をクリアするコード」は、"x & (x - 1)"ですが、これを記述するには and, sub1 の2命令があれば、


1: %v1 = sub1 %input
2: %v2 = and %input, %v1
3: ret %v2


のように書けます。簡単のために、命令セットは静的単一代入方式で書かれることにしましょう。また、手元の仮想マシンの命令セットをlibraryと呼ぶことにします。
さて、問題を解くのに必要な命令セットの組が、わかっているとしましょう。Libraryから、問題を解くのに必要な命令セットを含む、いくつかの命令を取り出します。たとえば、今手元に、add1, sub1, and, xor の命令セットがあるとします。


add1
sub1
and
xor


ここからどうすれば、目的のプログラムを生成できるでしょうか?
・もし、これらのコードが、バイトコードで何行目に位置するかがわかり、
・もし、これらのコードが、どこで何行目のバイトコードの出力を利用するか(あるいは関数への入力をそのまま利用するか)がわかれば、
プログラムは完成します。つまり、


%v2 = add1 %v1
%v1 = sub1 %input
%v4 = and %input, %v1
%v3 = xor %v1, %v2


……の、赤字の部分を埋めてやれることができれば、プログラムを生成した、ということができます。出力の順に並び替えると、このようになります。


%v1 = sub1 %input
%v2 = add1 %v1
%v3 = xor %v1, %v2
%v4 = and %input, %v1
ret %v4


ここで、add1やxorがデッドコードになっていることに注意してください。

どうやって解くか

「add1が出力アルゴリズムのi行目にある」ことを表す、Oadd,iというboolean変数を用意します。例えば、上の例ではOadd,1..3 = false, Oadd,4=true が成り立ちます。同様にライブラリ内の他の行についても、boolean変数を用意します。

「add1の入力が出力アルゴリズムのi行目にある」ことを示す、Iadd,iを用意します。例えば、上の例ではIadd,1 = false, Iadd,2 = true, ...が成り立ちます。同様に(ry。入力が複数ある場合は、その場所ごとに変数を用意します。

・出てくるバイトコードについて、自分の入力を自分に食わせたり、自分より後に出てくる命令の出力を入力に使ったり、ということはできません。これを制約として表した論理式を作りましょう。例えば、Oadd,1=trueならば、Iadd,2=falseが成り立ちます。なぜならば、2行目の出力を1行目で使うことはできないからです。Oadd,1→¬Iadd,2.
・また、一つの行に2つのバイトコードが入ることもできません。例えば、Oadd,1→¬Oxor,1とその逆が成り立ちます。
・そして、命令によって処理されれば、当然入力と出力の間に、add1なら「出力が入力+1」、xorなら「出力が入力1^入力2」という関係が成り立ちます。これも論理式として書き出しましょう。

こうして出来た巨大な論理式の束縛条件の下で、Oracleの入出力を満たす数字の組を探しましょう。こうした巨大な論理式を解くツールとして、SMTソルバというものが知られています。「これらの束縛条件を満たす」∧「Oracleの入出力を満たす」論理式をソルバに突っ込むと、答えが得られるか、あるいはこのlibraryでは決して解けないことが証明されます。このlibraryで解けないとわかったばあいは、libraryを拡張しましょう。

もし、有限個の入力についてだけでなく、全ての入力に対して仕様を満たすような解が欲しかったらどうするか? 以上でできたプログラムについて、今度は「仕様を満たさない解」をソルバに探させ、見つかったら今度はその解をOracleに追加して解きます。このループを繰り返せば、いつか解が見つかります。

何が問題で、我々はどうすべきであったか

……という論文を我々はICFPCで実装しましたが、スコアは芳しくないものでした。理由はif0の扱いです。ifの条件が満たされなかったほうの値は、何の制約も受けない変数となります。このため、問題空間がなかなか縮まず、特に解が見つからなかった時に多大な時間が掛かることとなります。if0を特別扱いし、うまく処理できれば、もう少しスコアがとれたと考えています。敗因は問題の性質を見誤ったこと、新技術の適用範囲を見極めずいきなり投入したこと、あたりでしょうか。しっかりとpostmortemしておきたいと思います。

[1] S. Gulwani, S. Jha, A. Tiwari, R. Venkatesan. Synthesis of Loop-free Programs. In: PLDI, 2011. (Link to CiteSeer)
[2] S. Jha, S. Gulwani, S.A. Seshia, A. Tiwari. Oracle-guided Component-based Program Synthesis. In: ICSE, 2010. (Link to CireSeer)
posted by chun at 02:55| 日記