ソフトウェア科学特論: 命題論理とSAT

本Webページ(およびPDF)の作成には Emacs org-mode を用いており， 数式等の表示は MathJax を用いています． IEでは正しく表示されないことがあるため， Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください． また org-info.js を利用しており， 「m」キーをタイプするとinfoモードでの表示になります． 利用できるショートカットは「?」で表示されます．

• 井上克巳，田村直之: 特集「最近のSAT技術の発展」にあたって， 人工知能学会誌，25巻1号，pp.56，2010年．
  1. 井上克巳，田村直之: SATソルバーの基礎， 人工知能学会誌，25巻1号，pp.57-67，2010年．
  2. 鍋島英知，宋剛秀: 高速SATソルバーの原理， 人工知能学会誌，25巻1号，pp.68-76，2010年．
  3. 田村直之，丹生智也，番原睦則: 制約最適化問題とSAT符号化， 人工知能学会誌，25巻1号，pp.77-85，2010年．
  4. 岩沼宏治，鍋島英知: SMT：個別理論を取り扱うSAT技術， 人工知能学会誌，25巻1号，pp.86-95，2010年．
  5. 長谷川隆三，藤田博，越村三幸: モデル列挙とモデル計数， 人工知能学会誌，25巻1号，pp.96-104，2010年．
  6. 平山勝敏，横尾真: ＊-SAT: SATの拡張， 人工知能学会誌，25巻1号，pp.105-113，2010年．
  7. 鍋島英知: SATによるプランニングとスケジューリング， 人工知能学会誌，25巻1号，pp.114-121，2010年．
  8. 番原睦則，田村直之: SATによるシステム検証， 人工知能学会誌，25巻1号，pp.122-129，2010年．
• 番原睦則, 鍋島英知, 森畑明昌: 特集「SAT技術の進化と応用 〜パズルからプログラム検証まで〜」, 情報処理, 2016年8月号, 2016年.
  1. SAT技術の進化 (番原睦則・鍋島英知)
  2. SATとパズル—問題をいかにSATソルバーで解くか— (田村直之・宋　剛秀・番原睦則)
  3. SATとラムゼー数〜数学の未解決問題への挑戦〜 (藤田　博・越村三幸)
  4. SATとAI (井上克巳)
  5. SATソルバーの最近の進展 (鍋島英知・岩沼宏治・井上克巳)
  6. MaxSAT：SATの最適化問題への拡張—MaxSATソルバーの活用法— (越村三幸・藤田　博)
  7. SMTソルバーによるプログラム検証 (石井大輔・上田和紀)
• 宋剛秀, 田村直之: SATソルバーの最新動向と利用技術, 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 2017年.
• 田村直之，番原睦則，宋剛秀: SATソルバーは問題解決のための「銀の弾丸」か? (招待講演), 日本EDAベンチャー連絡会 (JEVeC) 第12回総会, 2016年.
• 田村直之: SAT Solver and its Application to Combinatorial Problems (招待講演), 実験計画法およびその周辺の組合せ構造2014, 2014年.
• 田村直之，丹生智也，番原睦則: SAT型制約ソルバーSugarについて (招待講演)， 第81 回人工知能基本問題研究会，2011年．
• 番原睦則, 宋剛秀, 田村直之, 井上克巳: 私のブックマーク：SAT ソルバー, 人工知能学会誌，28巻2号, 2013年.

通常，命題論理式は 連言標準形 (CNF; Conjunctive Normal Form)で与えられる．

• CNF式 は，複数の節の連言(AND)である．
• 節 (clause)は，複数のリテラルの選言(OR)である．
• リテラル (literal)は，命題変数またはその否定である．

標準的フォーマットとしては，DIMACS CNFが用いられる．

p cnf 9 7  ; Number of variables and clauses
1 2 0      ; a or b
9 3 0      ; c or d
1 8 4 0    ; a or e or f
-2 -4 5 0  ; -b or -f or g
-4 6 0     ; -f or h
-2 -6 7 0  ; -b or h or i
-5 -7 0    ; -g or -i

1. The SAT Game のページで， 表示されたSAT問題を充足する真理値割当を探せ． できれば「too hard」に挑戦!
   • 赤だけの節(すべてが偽のリテラル)ができないようにうまく選択する．
   • 緑のマス(真のリテラル)が一つでもあればその節は充足されている．
   • 青の三角が示された節は，残りの一つのリテラルを真にする必要がある．

DPLLアルゴリズムは1960年代に Davisらによって考案されたアルゴリズムである [Davis & Putnam 1960] [Davis, Logemann & Loveland 1962]．

DPLLアルゴリズムで基本となるのは， 単位伝播 (UP; unit propagation)である．

• 与えられたCNF式を表す節集合を \(S\) とし， \(v\) を部分真理値割当とする．
• \(S\) 中の節 \(C = \{L_1,L_2,\ldots,L_n\}\) において， あるリテラル \(L_i\) を除いた他のリテラル \(L_j\) に対して \(v(L_j) = \FV\) であり， \(v(L_i)\) が未定義ならば， \(v(L_i) = \TV\) となるように \(v\) を拡張する．

単位伝播が行えない場合は， 部分真理値割当 \(v\) の定義域に含まれていない命題変数 \(p\) を一つ選択し， \(v(p) = \FV\) と拡張する場合と \(v(p) = \TV\) と拡張する場合の双方を試す．

このようにして， \(S\) 中のすべての節 \(C\) において， \(v(L) = \TV\) となるリテラル \(L\) が存在するような真理値割当 \(v\) を求める．

DPLLアルゴリズムをScala風に記述すると以下のようになる．

 1:  def solve(clauses: Set[Clause], assignment: Map[Bool,Boolean]): Boolean = {
 2:    val a = unitPropagation(clauses, assignment)
 3:    if (clauses に部分真理値割当 a を適用した結果，空節が含まれている)
 4:      false
 5:    else if (clauses に部分真理値割当 a を適用した結果，全節が恒真である)
 6:      true
 7:    else {
 8:      val p = select(clauses, a)
 9:      solve(clauses, a + (p -> false)) || solve(clauses, a + (p -> true))
10:    }
11:  }

• solve は，節集合 clauses と部分真理値割当 assignment を引数として， assignment を拡張した真理値割当で clauses が充足可能な時 true を返し， 充足不能の時 false を返す．
• 2行目で，単位伝播により拡張された部分真理値割当 a を求めている．
• 3–4行目で，部分真理値割当 a により空節が生じれば false を返す．
• 5–6行目で，部分真理値割当 a により全ての節が恒真になれば true を返す．
• 8行目では，まだ真理値が未定義の命題変数を一つ選択し p としている．
• 9行目で，まず p を false とした場合を調べ， 充足不能なら(すなわち false が返ってくれば) p を true とした場合を調べる．

• 最新のSATソルバー では， 以下の技術がDPLLに導入され，大幅な性能向上が実現されている．
  • 矛盾からの節学習 (CDCL; Conflict Driven Clause Learning) [Silva 1996]
  • 非時間順バックトラック法 [Silva 1996]
  • ランダム・リスタート [Gomes 1998]
  • 監視リテラル [Moskewicz & Zhang 2001]
  • 変数選択ヒューリスティック [Moskewicz & Zhang 2001]
• ChaffとzChaffは，1桁から2桁の速度改善を実現した [Moskewicz & Zhang 2001]．
• SAT競技会およびSATレースが2002年から開催され， SATソルバーの実現技術の進歩に貢献している．
• MiniSatソルバーは，C++で1000行以内のコードで， 2005年のSAT競技会で素晴らしい成績を収めた．
• 最新のSATソルバーは，10⁶ 以上の変数，10⁷ 以上の節を 取り扱うことができる．

ここでは MiniSat 2.2.0 を使用する． 自分でダウンロードしてmakeするのでも良いが， 情報基盤センターのiMac上でmakeしたバイナリを以下の手順でダウンロードする．

$ curl -O http://www2.kobe-u.ac.jp/~tamura/soft/minisat/core/minisat
$ chmod +x minisat
$ ./minisat --help

次に以下の内容のCNFファイル sample.cnf を作成する．

p cnf 3 4
1 2 3 0
-1 -2 0
-1 -3 0
-2 -3 0

これは \(\{p_1, p_2, p_3\}\), \(\{\neg p_1, \neg p_2\}\), \(\{\neg p_1, \neg p_3\}\), \(\{\neg p_2, \neg p_3\}\) という4つの節からなる節集合を表している． これは \(p_1\), \(p_2\), \(p_3\) のうち，ちょうど一つだけが真になる条件を表現している．

この sample.cnf に対して，以下のように MiniSat を実行する．

$ ./minisat sample.cnf sample.out
$ cat sample.out

結果のファイル sample.out は， 与えられたCNFが充足可能であること(一行目のSAT)， また充足する真理値割当を表している (\(p_1=\FV\), \(p_1=\TV\), \(p_1=\FV\))．

SAT
-1 2 -3 0

前述の prop-sat11.scala を用いた実行例は以下の通りである．

$ scalac prop-sat11.scala
$ scala sat.DPLL sample.cnf -d
Set({-1, -3}, {-1, -2}, {-2, -3}, {1, 2, 3})
Decide : -1 -> false
Propagate : -3 -> true
Propagate : -2 -> true
SAT
1 -2 -3 0

グラフ彩色問題 (GCP; Graph Coloring Problem)は， 与えられたグラフに対して隣接する頂点が異なる色になるように各頂点を彩色する時， 必要となる最小の色数 (彩色数, chromatic number)を求める問題である．

また，グラフおよび色数を与えて，その色数以内で彩色可能かどうかを判定する 決定問題 (decision problem)として定式化することもできる．

無線の周波数割当問題，コンパイラでのレジスタ割付問題などは グラフ彩色問題の一種である．

• Graph Coloring and its Generalizations

以下のグラフの彩色数は3である． すなわち，3色あれば隣接する頂点が異なる色になるようにできる．

• \(v_1=1\), \(v_2=2\), \(v_3=3\), \(v_4=1\) と彩色すれば良い．
• 2色では彩色できない．

DIMACSフォーマットでの記述は以下のようになる．

p edges 4 5
e 1 2
e 1 3
e 2 3
e 2 4
e 3 4

決定問題としてのグラフ彩色問題は制約充足問題 (CSP)として定式化できる． 前述のグラフで色数を3とした場合，以下のCSPとして定式化される． \begin{eqnarray*} v_1 & \in & \{1,2,3\} \\ v_2 & \in & \{1,2,3\} \\ v_3 & \in & \{1,2,3\} \\ v_4 & \in & \{1,2,3\} \\ v_1 & \ne & v_2 \\ v_1 & \ne & v_3 \\ v_2 & \ne & v_3 \\ v_2 & \ne & v_4 \\ v_3 & \ne & v_4 \end{eqnarray*}

グラフ彩色問題の制約モデルを直接符号化によりSAT問題に変換する．

• 各頂点 \(v_i \in \{1,2,\ldots,k\}\) の符号化
• 各辺 \(v_i \ne v_j\) の符号化

上のプログラムを改良し，以下に答えよ．

1. 上の例で，色数を2とすると充足不能となることを確認せよ．
2. 上の例で，v1 と v4 を結ぶ辺を追加し色数を4とした場合の結果を確認せよ．
3. 上の例で，v1=1 とした場合の解を求めるにはどうすれば良いか．
4. 立方体(正6面体)の各頂点に彩色する時，最小彩色数はいくつになるか調べよ．
5. 正8面体ではどうなるか．
6. MiniSatの出力ファイルからSAT問題の解を読み込み， グラフ彩色問題の解として表示するプログラムを作成せよ．

ラテン方陣 (Latin Square)は， \(n \times n\) 行列の各成分が 1 から \(n\) の値を取る時， どの行，どの列にも 1 から \(n\) の値がちょうど一度現れるように配置する問題である．

以下は \(5 \times 5\) のラテン方陣の例である．

• ラテン方陣

ラテン方陣の \(i\) 行目 \(j\) 列目の成分を \(a_{ij}\) で表す． 各 \(a_{ij}\) について \(a_{ij} \in \{1..n\}\) である．

次に制約の記述を簡潔にするため， 与えられた引数がすべて互いに異なることを表す \(\mbox{alldifferent}\) 制約を導入する． 引数が \(x_1, x_2, \ldots, x_m\) の時の \(\mbox{alldifferent}\) 制約は，以下のように定義される． \begin{eqnarray*} \mbox{alldifferent}(x_1, x_2, \dots, x_m) & \Longleftrightarrow & \bigwedge_{1 \le i < j \le m} x_i \ne x_j \end{eqnarray*} この \(\mbox{alldifferent}\) 制約を利用すると， ラテン方陣の制約モデルは以下のように記述できる． \begin{eqnarray*} & a_{ij} \in \{1..n\} & (i=1..n, j=1..n) \\ & \mbox{alldifferent}(a_{i1}, a_{i2}, \dots, a_{in}) & (i=1..n) \\ & \mbox{alldifferent}(a_{1j}, a_{2j}, \dots, a_{nj}) & (j=1..n) \end{eqnarray*}

\(\mbox{alldifferent}\) 制約は \(\ne\) で表すことができるから， ラテン方陣のSAT符号化はグラフ彩色問題のSAT符号化の一種である．

ここではラテン方陣の成分 \(a_{ij}\) を グラフの頂点 \(v_k\) に対応させる． \(k = n(i-1)+j\) と置くことで， \(a_{11}\) から \(a_{nn}\) の各成分が \(v_1\) から \(v_{n^2}\) の頂点に対応する． 逆に \(i = ((k-1) \mathop{\mbox{div}}\,n)+1\), \(j = ((k-1) \bmod n)+1\) とすれば， 頂点 \(v_k\) に対応する成分が \(a_{ij}\) であることがわかる．

上のプログラムを改良し，以下に答えよ．

1. \(9 \times 9\) のラテン方陣を求めよ．
2. MiniSatの出力ファイルからSAT問題の解を読み込み， ラテン方陣の解として表示するプログラムを作成せよ．