SATとは
SAT(Satisfiability Problem)は
ブール関数(f)がtrueと評価されるようにfの変数の割り当てを決定,
またはそのような割り当てが存在しないことを証明すること.
(発展的な話題としてP,NP問題につながる)
n変数の論理式で,f=1となる組み合わせがあるかどうかは真理値表を書くことで確認可能
ただし,その計算時間は$O(2^n)$となり,多項式時間では解けない.
(1変数に対して1or0の可能性があるため）
一方で，論理式$x_1, x_2, ..., x_n$に0か1を代入して,fが1か0となるかを確認することはすぐにできる.
このようにSATで考えることで計算時間が(すべての場合を考えるときに比べて)非常に短くなるという利点がある.
多くの問題はSAT問題に変換することができるので,コンピュータが普通に解く分には難しい問題をSAT問題として扱うことで,効率よく解くことができるのではないかと考えるケースが多い.
定義
真偽値をとる論理変数$x_1, x_2, ...$および論理演算しで論理式を構成
論理否定
論理否定($\bar{x}$)...$x_1$が真ならば偽.偽ならば真
| $x_1$ | $\bar{x_1}$ |
|---|---|
| 0 | 1 |
| 1 | 0 |
論理和
論理和($x_1∨x_2$)
| $x_1$ | $\bar{x_1}$ | $x_1 ∨ \bar{x_1}$ |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 1 |
論理積
論理積($x_1∧x_2$)
| $x_1$ | $x_2$ | $x_1 ∧ x_2$ |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 0 |
| 1 | 0 | 0 |
| 1 | 1 | 1 |
リテラル
リテラル...論理変数($x_1$)またはその否定($\bar{x_1}$)のこと
節
節...リテラルの論理和のこと
問題の例
$f = (x_1 ∨ x_2 ∨ \bar{x_3}) ∧ (\bar{x_1} ∨x_3) ∧ (\bar{x_2} ∨ x_3)$に対して$f$が真となるような$x_1, x_2, x_3$の真偽値の組み合わせは存在するか?
存在する例
$x_1 = 1, x_2 = 1, x_3 = 1$の場合満たされる
理由
第一節$(x_1 ∨ x_2 ∨ \bar{x_3})$,第二節$(\bar{x_1} ∨x_3)$,第三節$(\bar{x_2} ∨ x_3)$に注目する
第一節について,これは$1∨ 1∨ 0$となるので第一節は真
第二節について,これは$0 ∨ 1$となるので第二節は真
第三節について,これは$0∨ 1$となるので第三節は真
したがって,$f = 1 ∧ 1 ∧ 1$となるので,$f$は真となり,その時の変数割り当ては
$x_1 = 1, x_2 = 1, x_3 = 1$となる.
真とならない例
$x_1 = 1, x_2 = 0, x_3 = 0$の場合満たされない
理由
第一節,第二節,第三節に注目する
第一節について,これは$1∨ 0∨ 1$となるので第一節は真
第二節について,これは$0 ∨ 0$となるので第二節は偽
第三節について,これは$1∨ 0$となるので第三節は真
したがって,$f = 1 ∧ 0 ∧ 1$となるので,$f$は偽となる.
SATソルバー
SAT問題を解くとなったとき,
SATソルバーと呼ばれるSAT問題を効率的に解くためのツールがある.
数百万の変数の組み合わせにも対応しているようなSATソルバーもあり,その目的は
1.式が満たされるか(解が存在するか)を判定すること
2.解が存在する場合は,その変数割り当てを返すこと
となる.
SAT制約
SATソルバーを通じてSAT問題を解くとき,SAT制約を考えて解くことになる.
SAT制約は,論理式の形で表現され,これを考えることで
考えるべき変数の組み合わせを減らすことができる.
SAT制約の例
例:グラフの彩色問題
「隣接する2つの頂点が同じ色にならないように3色で彩色する」問題の場合
- 頂点を$V_1, V_2, ... $として,各頂点が赤、青、緑のいずれかになる制約
- $V_1$が赤なら$x_{1, red} = 1$, 青なら$x_{1,blue} = 1$(変数の定義)
- 制約例:頂点$V_1$は一つの色しか持たない(以下の論理式で表現可能)
($x_{1, red} ∨ x_{1, blue} ∨ x_{1,green}$)∧($\bar{x_{1,red}} ∨ \bar{x_{1, blue}}$)- 前半について:真ならば頂点$V_1$がいずれかの色に彩色されていることを表す
- 後半について:真ならば赤と青を同時に持っていないことを表す
- そのほかに青と緑,赤と緑を同時の持たないことを表す論理式を追加することで
頂点$V_1$について,一つの色しか持たないことを表せる
- 制約例:$V_1, V_2$が同じ色にならない制約(隣接頂点間の制約)
($\bar{x_{1,red}}∨ \bar{x_{2,red}}$) ∧ ($\bar{x_{1,blue}}∨ \bar{x_{2,blue}}$) ∧($\bar{x_{1,green}}∨ \bar{x_{2,green}}$)- 論理式について:偽ならば頂点$V_1, V_2$で同じ色を持っていることになる
→頂点$V_1, V_2$についての論理式しか例として挙げていないが,考えられる全ての頂点,頂点の組み合わせに対して制約は考える必要がある.
こうした制約をSATソルバーに入力することで解が存在するか否かが判別可能
最後に
SATについて簡単にまとめてみた.
次回は数独に対して,SATソルバーを実際に使ってみようと思う.