日々の流転

λ. Tseitin encoding と pseudo boolean constraint

任意の命題論理式は Tseitin encoding というを使うと、元の論理式に対して線形サイズであるような equisatisfiable なCNFへと変形できる。

• SATソルバを使うためにCNFを作る - soutaroにっき
• 自分で昔書いたやつ

その際に、連言 l1∧…∧ln を表現するために、新たな変数cと ￢l1∨…∨￢ln∨c (すなわち l1∧…∧ln → c) および ￢c∨li (すなわち c→li) という形の節を導入し、もとの連言をcで置き換える。ただし、PB制約(Pseudo Boolean constraint)が使える場合には、後者の ￢c∨li という形のn個の節の代わりに n*c ≦ l1+…+ln という形の単一のPB制約を加えても良いことが知られている。

しかし、いずれの方法が効率が良いだろうか? DPLLで解くことを考えると、 制約数の増加はそれほど問題ではないので、unit propagation の効率から節を用いた方が良さそう。 一方、LP緩和と単体法を用いる場合、制約数の増加は結構問題になりそうなので、節にすることで緩和問題の実行可能領域が狭められるメリットと、制約数の増加のデメリットのトレードオフになりそう。

といっても、どれくらい狭まるのかピンとこなかったので、2つのリテラルの連言x∧yの場合について、Sageでプロットしてみた。 どちらの場合についても、新たに導入した変数の取りうる値の範囲は下に閉じていることは明らかなので、この変数の最大値を x, y に関してそれぞれプロットしている。それぞれ、色のついた面よりも下の部分が実行可能領域。

x, y = var('x,y,z')
plot3d(x+y / 2, (x,0,1), (y,0,1))

plot3d(min_symbolic(x,y), (x,0,1), (y,0,1))

こうしてみると、確かに範囲は限定されているねぇ。どれくらいのメリットがあるかは分からないけれど……