SHIINBLOG

楽しい楽しい SAT符号化

琉大情報工学科(知能情報コース) Advent Calendar 2018 10日目の記事です.

SAT 符号化についてまとめているところが無くて,とても苦労したのでまとめておく.

SAT符号化とは,制約充足問題や制約最適化問題などを SAT 問題(充足可能性問題:Satisfiability Problem)に変換することである.

近年, SAT問題を解く SATソルバーは高速になっている.
そのため,制約充足問題専用のソルバーを使用するより, SAT符号化を行い SATソルバー*1を使用した方が高速に解くことができる場合がある.
まず, SAT問題について説明する.

SAT問題

SAT問題(Satisfiability)は,与えられた命題論理式または関数が充足可能(SAT)であえるか,充足不能(UNSAT)であるかを判定する問題である.

充足可能とは,命題論理式の命題変数に対し,T または F を割り当てて,式全体が T となる割り当てが少なくとも1つ存在することを言う.

例えば,f=( A ∨ B) ∧ (¬ A ∨ B) ∧ (A ∨ ¬ B) という関数は,以下に示すように A = TB = T の時に関数f が真となる.つまり,関数f は充足可能である.

A B f
T T T
T F F
F T F
F F F

充足不能な例は, A ∧ ¬A などである.A ∧ ¬A は,A に T,F どちらを割り当てても式全体は F となる.


ハードウェアやソフトウェアの検証,制約充足問題,スケジューリング問題などの問題を SAT問題に置き換えることができる.そのため, SAT問題を解くアルゴリズムが研究されてきた. それにより,近年 SATソルバーの性能が向上し非常に高速に SAT問題が解けるようになった.

そこで,制約充足問題などを SAT問題へ符号化し, SATソルバーで解を求める SAT符号化の研究もされるようになった.

SAT問題は,連言標準形(Conjunctive Normal Form: CNF)の論理式を与えられることが多い. CNF は,節の連言(∧)であり,節はリテラル(命題変数またはその否定)の選言(∨)である. 具体例としては,上で出てくる ( A ∨ B) ∧ (¬ A ∨ B) ∧ (A ∨ ¬ B) などである.

これ以降は,連言を省略して節を並べて表記する.


SAT符号化

SAT符号化は,直接符号化法順序符号化法,対数符号化法 などが提案されている*2



直接符号化法

x = 0 を表す命題変数p(x=0) を導入する.

x が 0 から 4 の範囲を取る場合(x ∈ [0,4]),
p(x=0) から p(x=4) までを導入する. x は 0 から 4 のどれかの値を取るため,次のような式をたてる.

p(x=0) ∨ p(x=1) ∨ p(x=2) ∨ p(x=3) ∨ p(x=4)

これで,0 から 4 のどれかであるという命題変数が真となる必要がある. at-least-one 節と呼ばれるもの.少なくとも1つを満たす必要がある.

また,0 から 4 が同時に成り立つことは無いため,排他になるようにする.

¬p(x=0) ∨ ¬p(x=1)
¬p(x=0) ∨ ¬p(x=2)
¬p(x=0) ∨ ¬p(x=3)
        ⋮
¬p(x=2) ∨ ¬p(x=3)
¬p(x=2) ∨ ¬p(x=4)
¬p(x=3) ∨ ¬p(x=4)

こんな感じ これは,A → B(A ならば B) の変形 ¬A ∨ B と考えることができる. p(x=0) ならば ¬p(x=1) である.
これが, at-most-one 節と呼ばれるもの.最大で1つのみが真となる.


他に x ≦ 2 などの制約がある場合,その制約に違反する点をあげる.

¬p(x=3)
¬p(x=4)

となる.

x ∈ [0,4] と x ≦ 2 を符号化したものを全て SATソルバーに与えると, SAT であるという答えと一緒に

p(x=0) ¬p(x=1) ¬p(x=2) ¬p(x=3) ¬p(x=4)

など SAT な解の1つを返してくれる.

x+1 ≦ y なども,違反点をあげていけば符号化できる.

¬p(y=1) ∨ ¬p(x=1)
¬p(y=1) ∨ ¬p(x=2)
       ⋮

という感じ. p(y=1) ならば ¬p(x=1) (y=1 のとき, x=1 なら x+1 ≦ y が成り立たないので) y=2 のときなども全部違反点を上げるため節がとても多くなる…



順序符号化法

x ≦ 0 を表す命題変数p(x≦0) を導入する.

同じように x ∈ [0,4] を表すと,

¬p(x≦0) ∨ p(x≦1)
¬p(x≦1) ∨ p(x≦2)
¬p(x≦2) ∨ p(x≦3)

という感じ. p(x≦4) は常に真となるので,不要.

この命題変数の真理値表を書くと,数が表現できていることが分かる.

p(x≦0) p(x≦1) p(x≦2) p(x≦3) x
F F F F 4
F F F T 3
F F T T 2
F T T T 1
T T T T 0

命題変数の組み合わせは上の表しかなく, x の値を判断できる.

こちらは,直接符号化法の at-least-one 節や, at-most-one 節は,不要で, 節数も少なく表現できる.


x ≦ 2 などは違反する範囲をあげれば良い.

¬p(x≦3)

直接符号化法は違反点をあげるのに対し,順序符号化法は違反範囲をあげるため, 線形制約は簡単に符号化ができる.


x+1 ≦ y は少しだけ複雑になる.

y=1 のとき,p(y≦0) が偽,p(y≦1) が真となるので,
y=1 は, ¬p(y≦0) ∧ p(y≦1) である.

つまり,(¬p(y≦0) ∧ p(y≦1))→ p(x≦0)(y=1 ならば, x は 0 以下である)という形になって,
A→B = ¬A ∨ B の変形とド・モルガンを適用して変形すると,p(y≦0) ∨ ¬p(y≦1) ∨ p(x≦0) となる.

y=1 のときは,恩恵が微妙だけど, y=3 のときなどは,
p(y≦2) ∨ ¬p(y≦3) ∨ p(x≦2) だけで違反する範囲をあげることができるので,
少ない節数で表現できる.



対数符号化法

x や y などの変数を2進表記で考える符号化である.
{ \displaystyle
x = (x_2, x_1,x_0)_2
} として表現する.

x ∈ [0,4] は,違反するビットを否定する.
¬{ \displaystyle x_2} ∨ ¬{ \displaystyle x_0}
¬{ \displaystyle x_2} ∨ ¬{ \displaystyle x_1}

こんな感じで, 5(101)や6(110),7(111)が現れないようにする.

全て偽の場合は,0 となるので,こちらも at-least-one 節や, at-most-one 節と呼ばれるものはない.


x ≦ 2 なんかは,上と同じように違反するビットを否定すれば良い.
¬{ \displaystyle x_2}
¬{ \displaystyle x_1} ∨ ¬{ \displaystyle x_0}



この程度なら良いのだけど,
( x+5 ≦ y ) ∨ ( y+8 ≦ x) みたいなやつがたくさんあると,
対数符号化法 上手くいかない…
辛い…


誰かこの記事見て面白いと思った人一緒に考えてくれ〜〜〜 @e145755 リプライ待ってます_(:3」∠)_

論理学も勉強中なので,一緒に勉強してくれる人居たら声かけて_(:3」∠)_