一通り道具は揃ったはずなので、とりあえずプログラムっぽく整えてみる。

k-CNF の充足可能な(つまり、全ての clause が真になるような真偽値の)割り当てを求める問題は k-SAT(Satisfiability Problem)と呼ばれる。同書にならって 3-SAT を考える。問題としては、これまた同書でユーリが「僕」に示した問題で行ってみよう。まず変数…