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

Table of Contents

1 概要

本稿では,命題論理とSATについて説明する.

1.1 注意

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

1.2 参考文献

2 SAT

SAT (Boolean Satisfiability Testing)は 与えられた命題論理式について, それが充足可能か否かを判定する問題である.

  • SATは,理論上も実際上も計算機科学の中心的課題である.
  • SATは,NP完全であることが初めて示された問題でもある [Cook 1971].
  • 近年になって,非常に高速なSATソルバーが開発された(MiniSat等).
  • それを背景として,多くの分野でSATソルバーの利用が活発になっている.

2.1 SATの入力

通常,命題論理式は 連言標準形 (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

2.2 練習問題

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

3 SATソルバー

SATソルバー (SAT solver)は, 与えられたCNFの命題論理式が, 充足可能(SAT)か充足不能(UNSAT)かを判定するプログラムである.

  • 答えが SAT の場合,SATソルバーは値割当ても解として出力する.
  • 系統的(systematic)SATソルバーは,SATかUNSATかを答える.
    • 多くは DPLLアルゴリズム を用いている.
  • 確率的(stochastic)SATソルバーは,SATのみを答える(UNSATは答えない).
    • 局所探索アルゴリズムが用いられる.

3.1 DPLLアルゴリズム

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 とした場合を調べる.

3.1.1 Scalaのプログラム例

prop-sat11.scala にプログラム例を示す. このプログラムはアルゴリズムの概要を示すものであり, 効率は考慮されていない.

3.2 最新のSATソルバー

  • 最新の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ソルバーは,106 以上の変数,107 以上の節を 取り扱うことができる.

3.2.1 矛盾からの節学習 (CDCL)

  • 矛盾が生じたら,矛盾の原因が節として抽出され, 学習節 (learnt clause)として記憶される.
  • 学習節は,その後の探索で探索空間を大幅に削減する.
  • 学習節は,後ろ向きに導出(resolution)を行うことで生成できる.
  • 後ろ向きの導出は,First UIP (Unique Implication Point) で停止するのが最も効果的である [Moskewicz & Zhang 2001].

3.3 SATソルバーの利用例

ここでは 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

4 SAT型システム

元の問題をSAT問題に 符号化 (SAT encoding)し, SATソルバーをバックエンドとして利用する SAT型システム (SAT-based system)が, 困難な組合せ問題を解くための方法として広く用いられるようになっている.

  • プランニング (SATPLAN, Blackbox) [Kautz & Selman 1992]
  • 自動テストパターン生成 [Larrabee 1992]
  • ジョブ・ショップ・スケジューリング [Crawford & Baker 1994]
  • ソフトウェア仕様 (Alloy) [ 1998]
  • 有界モデル検査 (BMC; Bounded Model Checking) [Biere 1999]
  • ソフトウェアパッケージの依存性解析 (SATURN)
    • SAT4Jは,Eclipse 3.4に用いられている.
  • 書換え系 (Aprove, Jambox)
  • Answer Set Programming (ASP) (clasp, Cmodels-2)
  • 一階論理の定理証明系 (iProver, Darwin)
  • 一階論理のモデル発見機 (Paradox)
  • 制約充足問題 (CSP; Constraint Satisfaction Problem) (Sugar) [Tamura et al. 2006]

5 SAT符号化

整数上の制約をSAT符号化については, 種々の方法が提案されている.

  • 直接符号化 (Direct encoding)は,最も広く用いられている方法である [de Kleer 1989].
  • 順序符号化 (Order encoding)は,多くの問題に対して優れた性能を示す新しい方法である [Tamura et al. 2006].
  • 多値符号化 (Multivalued encoding) [Selman 1992]
  • 支持符号化 (Support encoding) [Kasif 1990]
  • 対数符号化 (Log encoding) [Iwama 1994]
  • 対数支持符号化 (Log-support encoding) [Gavanelli 2007]
  • コンパクト順序符号化 (Compact order encloding) [Tanjo et al. 2010]

各種符号化の詳細については参考文献を参照のこと.

6 グラフ彩色問題のSAT符号化

6.1 グラフ彩色問題

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

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

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

6.2 グラフ彩色問題の例

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

images/png_ce34bf1c4131d9d68826170a7f28b190968e821c.png

  • \(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

6.3 グラフ彩色問題の制約モデル

決定問題としてのグラフ彩色問題は制約充足問題 (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*}

6.4 グラフ彩色問題の直接符号化

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

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

各頂点に対応する整数変数 \(v_i\) のそれぞれについて, 取り得る値 \(a\) (\(a=1,2,\ldots,k\) )に応じて, \(k\) 個の命題変数 \(p_{i,a}\) を用意する. 各命題変数 \(p_{i,a}\) は以下を表す. \begin{eqnarray*} p_{i,a} & \Llra & v_i = a \end{eqnarray*} 各整数変数 \(v_i\) がいずれかの値を少なくとも一つ取るという意味の以下の節を加える (at-least-one節). \begin{eqnarray*} & p_{i,1} \lor p_{i,2} \lor \cdots \lor p_{i,k} \end{eqnarray*} 各整数変数 \(v_i\) が2つ以上の値を同時に取らないという意味の以下の \(k(k-1)/2\) 個の節を加える. (at-most-one節). \begin{eqnarray*} & \neg p_{i,a} \lor \neg p_{i,b} & \quad (1 \le a < b \le k) \end{eqnarray*}

6.4.2 各辺の符号化

各辺に対応する制約 \(v_i \ne v_j\) のそれぞれについて, 以下の \(k\) 個の節を加える. \begin{eqnarray*} \neg p_{i,a} \lor \neg p_{j,a} & \quad (1 \le a \le k) \end{eqnarray*}

6.4.3 符号化の結果

前の例で色数を3とした場合の符号化の結果は以下のようになる. \begin{eqnarray*} & p_{i,1} \lor p_{i,2} \lor p_{i,3} & \quad (i=1,2,3,4) \\ & \neg p_{i,1} \lor \neg p_{i,2} & \quad (i=1,2,3,4) \\ & \neg p_{i,1} \lor \neg p_{i,3} & \quad (i=1,2,3,4) \\ & \neg p_{i,2} \lor \neg p_{i,3} & \quad (i=1,2,3,4) \\ & \neg p_{1,a} \lor \neg p_{2,a} & \quad (a=1,2,3) \\ & \neg p_{1,a} \lor \neg p_{3,a} & \quad (a=1,2,3) \\ & \neg p_{2,a} \lor \neg p_{3,a} & \quad (a=1,2,3) \\ & \neg p_{2,a} \lor \neg p_{4,a} & \quad (a=1,2,3) \\ & \neg p_{3,a} \lor \neg p_{4,a} & \quad (a=1,2,3) \end{eqnarray*}

6.4.4 符号化を行うプログラム

以下はグラフ彩色問題の直接符号化を行うScalaプログラムの例である (gcp01.scala).

 1:  case class GCP(nodes: Int, edges: Set[(Int,Int)], colors: Int) {
 2:    val variables = nodes * colors
 3:    val clauses = nodes * (1 + colors*(colors-1)/2) + edges.size * colors
 4:    def p(i: Int, a: Int) = (i-1) * colors + a
 5:    def printClause(lits: Seq[Int]) {
 6:      println(lits.mkString(" ") + " 0")
 7:    }
 8:    def encode {
 9:      println("p cnf " + variables + " " + clauses)
10:      for (i <- 1 to nodes) {
11:        printClause((1 to colors).map(a => p(i, a)))
12:        for (Seq(a,b) <- (1 to colors).combinations(2))
13:          printClause(Seq(-p(i,a), -p(i,b)))
14:      }
15:      for ((i, j) <- edges; a <- 1 to colors)
16:        printClause(Seq(-p(i,a), -p(j,a)))
17:    }
18:  }
19:  object GCP {
20:    def main(args: Array[String]) {
21:      val gcp = GCP(4, Set((1,2), (1,3), (2,3), (2,4), (3,4)), 3)
22:      gcp.encode
23:    }
24:  }
6.4.5 実行

以下のようにして実行する.

$ scalac gcp01.scala
$ scala GCP >gcp.cnf
$ cat gcp.cnf

以下が表示される.

p cnf 12 31
1 2 3 0
-1 -2 0
-1 -3 0
-2 -3 0
4 5 6 0
-4 -5 0
-4 -6 0
-5 -6 0
7 8 9 0
-7 -8 0
-7 -9 0
-8 -9 0
10 11 12 0
-10 -11 0
-10 -12 0
-11 -12 0
-1 -7 0
-2 -8 0
-3 -9 0
-4 -10 0
-5 -11 0
-6 -12 0
-4 -7 0
-5 -8 0
-6 -9 0
-7 -10 0
-8 -11 0
-9 -12 0
-1 -4 0
-2 -5 0
-3 -6 0

以下のようにMiniSatを実行する.

$ ./minisat gcp.cnf gcp.out
$ cat gcp.out

たとえば以下の結果が表示される.

SAT
-1 -2 3 -4 5 -6 7 -8 -9 -10 -11 12 0

\(p_{1,3}\), \(p_{2,2}\), \(p_{3,1}\), \(p_{4,3}\) が真であるので, \(v_1 = 3\), \(v_2 = 2\), \(v_3 = 1\), \(v_4 = 3\) が解として得られていることがわかる.

6.5 練習問題

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

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

7 ラテン方陣のSAT符号化

7.1 ラテン方陣

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

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

12345
45123
23451
51234
34512

7.2 ラテン方陣の制約モデル

ラテン方陣の \(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*}

7.3 ラテン方陣の直接符号化

\(\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}\) であることがわかる.

7.3.1 符号化を行うプログラム

以上の対応に基づいて, ラテン方陣をグラフ彩色問題に変換し符号化するプログラムを作成すると, latin02.scala のようになる.

 1:  case class GCP(nodes: Int, edges: Set[(Int,Int)], colors: Int) {
 2:    val variables = nodes * colors
 3:    val clauses = nodes * (1 + colors*(colors-1)/2) + edges.size * colors
 4:    def p(i: Int, a: Int) = (i-1) * colors + a
 5:    def printClause(lits: Traversable[Int]) {
 6:      println(lits.mkString(" ") + " 0")
 7:    }
 8:    def encode {
 9:      println("p cnf " + variables + " " + clauses)
10:      for (i <- 1 to nodes) {
11:        printClause((1 to colors).map(a => p(i, a)))
12:        for (a <- 1 to colors; b <- a+1 to colors)
13:          printClause(-p(i,a) :: -p(i,b) :: Nil)
14:      }
15:      for ((i, j) <- edges) {
16:        for (a <- 1 to colors)
17:          printClause(-p(i,a) :: -p(j,a) :: Nil)
18:      }
19:    }
20:  }
21:  object Latin {
22:    def main(args: Array[String]) {
23:      val n = 5
24:      var edges: Set[(Int,Int)] = Set.empty
25:      def v(i: Int, j: Int) = n*(i-1) + j
26:      def alldiff(vs: Seq[Int]) {
27:        for (k <- 0 until vs.size; l <- k+1 until vs.size)
28:          edges += Pair(vs(k), vs(l))
29:      }
30:      for (i <- 1 to n)
31:        alldiff((1 to n).map(j => v(i,j)))
32:      for (j <- 1 to n)
33:        alldiff((1 to n).map(i => v(i,j)))
34:      val gcp = GCP(n*n, edges, n)
35:      gcp.encode
36:    }
37:  }
7.3.2 実行

以下のようにして実行する.

$ scalac latin02.scala
$ scala Latin >latin5x5.cnf

latin5x5.cnf の内容 (一部)は以下の通りである.

p cnf 125 775
1 2 3 4 5 0
-1 -2 0
-1 -3 0
-1 -4 0
-1 -5 0
-2 -3 0
-2 -4 0
-2 -5 0
-3 -4 0
-3 -5 0
-4 -5 0
.....
-1 -6 0
-2 -7 0
-3 -8 0
-4 -9 0
-5 -10 0
.....

以下のようにMiniSatを実行する.

$ ./minisat latin5x5.cnf latin5x5.out
$ cat latin5x5.out

たとえば以下の結果が表示される.

SAT
-1 2 -3 -4 -5 -6 -7 8 -9 -10 ...

得られた解をラテン方陣として表すと以下のようになる.

23154
41235
12543
35412
54321

7.4 練習問題

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

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

Date:

Author: 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0