Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む

Table of Contents

1 概要

本稿では Donald Knuth 先生の名著 The Art of Computer Programming (TAOCP)の 第4巻 Combinatorial Algorithms 中の 7.2.2.2 節 Satisfiability を テキストとして使用し,その一部について解説する.

1.1 注意

本稿は,作成中である.

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

1.2 Knuth先生について

1.3 TAOCPについて

At the end of 1999, these books were named among the best twelve physical-science monographs of the century by American Scientist, along with: Dirac on quantum mechanics, Einstein on relativity, Mandelbrot on fractals, Pauling on the chemical bond, Russell and Whitehead on foundations of mathematics, von Neumann and Morgenstern on game theory, Wiener on cybernetics, Woodward and Hoffmann on orbital symmetry, Feynman on quantum electrodynamics, Smith on the search for structure, and Einstein's collected papers. Wow! — Web page of The Art of Computer Programming by Donald E. Knuth

  • Volume 1: Fundamental Algorithms (3rd edition), 1997.
  • Volume 2: Seminumerical Algorithms (3rd Edition), 1997.
  • Volume 3: Sorting and Searching (2nd Edition), 1998.
  • Volume 4A: Combinatorial Algorithms, Part 1, 2011.
  • Volume 4B: Combinatorial Algorithms, Part 2, 準備中.
  • Volume 5: Syntactic Algorithms, 準備中.
  • Volume 6: 準備中.
  • Volume 7: 準備中.

1.4 進め方

"Preface" から "SAT examples—summary" (27ページ)までを対象とし, 以下のように進める.

  • 各自で,テキストを読む.
    • fasc6a-20150923.pdf ( 2015-09-23 Wed 版のドラフト.318ページ.アクセス制限有り)
  • 講義中で提示される課題に取り組む.
    • 基本的には,Knuth先生作のSATソルバーを利用する.
    • SATソルバーへの入力を生成するプログラムを各自で作成する. プログラミング言語は自分の好きなものを用いて良い. 本テキスト中ではJavaあるいはScalaのプログラムを回答例として示している.

1.4.1 練習問題に付いている印や数の意味

  • \(\blacktriangleright\) = recommended
  • M = Mathematically oriented
  • HM = Requiring "higher math"
  • 00 = Immediate
  • 10 = Simple (one minute)
  • 20 = Medium (quarter hour)
  • 30 = Moderately Hard
  • 40 = Term Project
  • 50 = Research Problem

1.5 Knuth先生作のSATソルバーの利用

Knuth先生作のSATソルバーは,以下に置かれている.

コンパイルには文芸的プログラミングのシステムCWEBが必要である.

Cのソースプログラムに変換したものを以下に置く(アクセス制限有り).

インストール手順は以下の通り.

$ cd
$ curl -O http://bach.istc.kobe-u.ac.jp/lect/soft/internal/sat-solvers-20150817.zip
$ unzip sat-solvers-20150817.zip
$ cd sat-solvers
$ gcc -O -o sat13 sat13.c gb_flip.c
$ ./sat13 h
Usage: ./sat13 [v<n>] [c<n>] ... < foo.sat

次に以下の内容のテキストファイル sample.sat を作成する.

p1 p2 p3
~p1 ~p2
~p1 ~p3
~p2 ~p3

上のCNFは \(\{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\) のうち,ちょうど一つだけが真になる条件を表現している.

Knuth先生のSATソルバーは,DIMACS形式ではなく独自形式の入力を受け取る. 変数名は8文字以下の任意の文字列で,負リテラルの前には ~ を付ける.

実行すると以下のように,結果が表示される.

$ ./sat13 <sample.sat
(3 variables, 4 clauses, 9 literals successfully read)
!SAT!
 ~p2 ~p3 p1
Altogether 250+80 mems, 5539 bytes, 2 nodes, 0 clauses learned, 17 memcells.
(0 restarts.)

上記のパッケージにはKnuth先生形式のファイルとDIMACS形式のファイルを相互変換する dimacs-to-sat, sat-to-dimacs が含まれている.

1.6 MiniSatの利用

基本的には,Knuth先生作のSATソルバーを利用するが, MiniSat 2.2.0 を使用する方法も説明しておく.

自分でダウンロードしてmakeするのでも良いが, 情報基盤センターのiMac上でmakeしたバイナリを以下の手順でダウンロードする.

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

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

p cnf 3 4
1 2 3 0
-1 -2 0
-1 -3 0
-2 -3 0
  • 1行目はヘッダで,3は変数の個数,4は節の個数を表す.
  • 以下の4行は,各行が1つの節に対応する. 行の最後には0が加わっている.
  • 正の数は正のリテラル(数が変数番号),負の数は負のリテラル(絶対値が変数番号)を表す.

上のCNFは \(\{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
SAT
-1 2 -3 0

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

1.7 Coprisの利用

sat13 や MiniSat などのSATソルバーでなく, 制約ソルバーを使う方法もある.

Copris は制約ソルバーであるが,内部的にはSATソルバー Sat4j を用いている. インストールおよび利用方法は Coprisによる制約プログラミング入門 を参照.

1.8 参考資料

2 Preface

2.1 田村が興味を持った文章

下線は田村が追加.

  • 「(if the FORCE stays with me).」
  • 「exercise 223 is also currently unsolved, although I've rated it only `40' because I once thought of an answer (which I have since forgotten!).」
  • 「I hope you will see why I've found this topic to be such a fascinating story;」
  • 「Wow—Section 7.2.2.2 has turned out to be the longest section, by far, in The Art of Computer Programming.」
  • 「The SAT problem is evidently a " killer app ," because it is key to the solution of so many other problems.」
  • 「I wrote more than three hundred computer programs while preparing this material, because I find that I don't understand things unless I try to program them.」

3 Definition

3.1 田村が興味を持った文章

下線は田村が追加.

  • 「Section 7.1.1 discussed the embarrassing fact that nobody has ever been able to come up with an efficient algorithm to solve the general satisfiability problem,」
  • 「The author of this book, however, suspects that \(N^{O(1)}\)-step algorithms do exist, yet they're unknowable.」
  • 「We now have algorithms that are much more efficient than anyone had dared to believe possible before the year 2000.」

3.2 定義

  • variable (変数): \(x_1\), \(x_2\), …, \(a\), \(b\), \(c\), …, \(d'''_{74}\) 等で表す
    • しばしば 1, 2, 3 などの数そのものを用いる. つまり \(x_j\) の代わりに単に \(j\) を用いる.
  • literal (リテラル): 変数あるいはそのcomplement
    • \(v\) が変数なら \(v\) も \(\bar{v}\) もliteral
    • literal \(l\) の complement は \(\bar{l}\) . すなわち \(\bar{\bar{l}} = l\) .
    • \(|l|\) はliteral \(l\) の変数を表す. すなわち変数 \(v\) について \(|v|=|\bar{v}|=v\) .
    • \(\pm v\) はliteral \(v\) あるいは \(\bar{v}\) を表す. また \(\sigma\) が \(\pm 1\) の時, \(\sigma v\) でliteralを表す.
    • \(|l|=l\) の時,literal \(l\) は positive, \(|l|=\bar{l}\) の時,literal \(l\) は negative と呼ばれる.
    • ふたつのliteral \(l\), \(l'\) は, \(l \ne l'\) の時 distinct である. \(|l| \ne |l'|\) の時 strictly distinct である.
  • literalのORがclauseで,clauseのANDがCNF formulaである.
    • \(F = (x_1 \lor \bar{x}_2) \land (x_2 \lor x_3) \land (\bar{x}_1 \lor \bar{x}_3) \land (\bar{x}_1 \lor \bar{x}_2 \lor x_3)\) \(\quad\mbox{(式1)}\)
    • \(G = F \land (x_1 \lor x_2 \lor \bar{x}_3)\) \(\quad\mbox{(式2)}\)
  • clauseをliteralの集合,CNF formulaをclauseの集合で表すこともできる.
    • \(F = \{\{1,\bar{2}\},\{2,3\},\{\bar{1},\bar{3}\},\{\bar{1},\bar{2},3\}\}\)
    • \(G = F \cup \{\{1,2,\bar{3}\}\}\)

    さらにclauseを表すためのカッコやコンマを省略する.

    • \(F = \{1\bar{2},23,\bar{1}\bar{3},\bar{1}\bar{2}3\}\), \(G = F \cup \{12\bar{3}\}\) \(\quad\mbox{(式3)}\)
  • satisfiability problemは covering problem と同等である.
    • CNF formula \(F = \{C_1,...,C_m\}\) で, 各 \(C_i\) はclause,現れている変数が \(\{x_1,...,x_n\}\) とする.
    • また \(T_n = \{\{x_1,\bar{x}_1\},...,\{x_n,\bar{x}_n\}\}\) (式4)とする.
    • \(F \cup T_n\) の各clauseが \(L\) 中のliteralを含んでるという意味で, \(F \cup T_n\) を "cover" する \(n\) 個のliteralからなる集合 \(L\) を見つける問題は, \(F\) のsatisfiabilityと同等である. \(T_n\) をcoverする \(n\) 個のliteralだから,各 \(x_i\) について \(x_i\) か \(\bar{x}_i\) が \(L\) に含まれる.
    • つまり \(F \cup T_n\) 中の各集合と必ず共通要素を持っているような \(L\) が存在すれば \(F\) はsatisfiableであり,また逆も成り立つ.
    • たとえば上の例の \(F\) と \(T_3\) は \(L=\{\bar{1},\bar{2},3\}\) でcoverできるから, \(F\) はsatisfiableである.
    • また \(G\) と \(T_3\) を同時にcoverする \(L\) は存在しないから, \(G\) はunsatisfiableである.
    • \(F\) をcoverする \(n\) 個のstrictly distinctなliteralからなる集合 \(L\) を見つける問題と いいかえることも可能である.
  • \(F\) 中のいくつかの変数をそのcomplementで置き換えた任意の式を \(F'\) とすると, \(F\) と \(F'\) のsatisfiabilityが同等であることは明らかだ.
    • たとえば \(1\) を \(\bar{1}\) で置き換え, \(2\) を \(\bar{2}\) で置き換えると, 上の例の \(F\), \(G\) から以下が得られる.
      • \(F' = \{\bar{1}2,\bar{2}3,1\bar{3},123\}\)
      • \(G' = F \cup \{\bar{1}\bar{2}\bar{3}\}\)
    • \(F'\) は trivially satisfiableである. なぜなら各clauseにpositive literalが含まれており, \(L\) をpositive literalの集合とすると,それでcoverできる.
  • \(F\) のunsatisfiabilityは \(\bar{F}\) がtautologyであることと同等である.
    • \(\bar{F} = (\bar{x}_1 \land x_2) \lor (\bar{x}_2 \land \bar{x}_3) \lor (x_1 \land x_3) \lor (x_1 \land x_2 \land \bar{x}_3)\) \(\quad\mbox{(式5)}\)
  • すべてのclauseの長さが \(k\) 以下のSATを \(k\textrm{SAT}\) (あるいは \(k\textrm{CNF}\))という.
    • 長さ1のclauseを unit clause ,長さ2のclauseを binary clause という. 以下 ternary clause, quaternary clause, …
    • 長さ0のclauseを empty clause といい \(\epsilon\) で表す. empty clauseはunsatisfiableである.
    • 長さ2のclause \((x \lor y)\) は,新しい変数 \(z\) を使い, 同等の \((x \lor y \lor z)\land(x \lor y \lor \bar{z})\) に置き換えることで長さ3にできる. したがって \(k\textrm{SAT}\) を,すべてのclauseの長さが \(k\) に等しいと定義することも可能である.
  • literal \(v\) と \(\bar{v}\) の両方を含むclauseはtautologicalであり,常にsatisfiableである. tautological clauseは \(\wp\) で表される.

3.2.2 練習問題

  1. The SAT Game のページで, 表示されたSAT問題を充足する真理値割当を探せ. できれば「too hard」に挑戦!
    • 赤だけの節(すべてが偽のリテラル)ができないようにうまく選択する.
    • 緑のマス(真のリテラル)が一つでもあればその節は充足されている.
    • 青の三角が示された節は,残りの一つのリテラルを真にする必要がある.
  2. 変数 \(x\) について,positive literalかnegative literalかの どちらか一方しか現れていない場合, \(x\) を含む節を取り除いても satisfiability は同等である.なぜか.
    (解答例)

    positive literalしか現れていない場合は \(x=1\) としてもsatisfiabilityは同等である. また,negative literalしか現れていない場合は \(x=0\) としてもsatisfiabilityは同等である. したがって,どちらの場合でも \(x\) を含む節を取り除くことができる.

  3. 与えられたCNF式がtautologyかどうかは簡単に判定できる.なぜか.
    (解答例)

    すべてのclauseがtautologicalかどうかを調べれば良い. すべてがtautologicalなら,CNF式はtautologyである. tautologicalでないclause \(\{l_1,l_2,\ldots,l_n\}\) が存在すれば, \(l_i=0\) とするassignmentで偽になるから,tautologyではない.

  4. 与えられたDNF式の satisfiability は簡単に判定できる.なぜか.
    (解答例)

    CNF式の場合とdualに考えれば良い.

  5. 任意のCNFは satisfiability が同等な3SATに変換できることを示せ.
    (解答例)

    長さが3以上のclause \((x_1 \lor \cdots \lor x_{n-2} \lor x_{n-1} \lor x_n)\) があれば, 新しい変数 \(z\) を使い, 同等の \((x_1 \lor \cdots \lor x_{n-2} \lor z) \land (\bar{z} \lor x_{n-1} \lor x_n)\) に 置き換えることで,長さを \(n-1\) にできる.

3.2.3 関連するExercise

  • Exercise 1 \(\;\) [ 10 ]
  • Exercise 2 \(\;\) [ 20 ]

3.3 The shortest interesting formula in 3CNF

以下の \(R\) は the shortest interesting formula in 3CNF である. \(R\) から最後のclauseを除いた \(R'\) はsatisfiableである. 最後でなく,どれを除いてもsatisfiableになる. \begin{eqnarray*} R & = & \{12\bar{3},23\bar{4},341,4\bar{1}2,\bar{1}\bar{2}3,\bar{2}\bar{3}4,\bar{3}\bar{4}\bar{1},\bar{4}1\bar{2}\} \quad\mbox{(式6)} \\ R' & = & \{12\bar{3},23\bar{4},341,4\bar{1}2,\bar{1}\bar{2}3,\bar{2}\bar{3}4,\bar{3}\bar{4}\bar{1}\} \quad\mbox{(式7)} \end{eqnarray*}

  • \(R\) はunsatisfiableであり \(R'\) はsatisfiableである.
  • R. L. Rivestのassociative block design ABD\((k,w)\) が元になっている.
  • ABD(4,3) の例 \begin{eqnarray*} & \begin{array}{cccc} 0 & 0 & 1 & * \\ {}* & 0 & 0 & 1 \\ 0 & * & 0 & 0 \\ 1 & 0 & * & 0 \\ 1 & 1 & 0 & * \\ {}* & 1 & 1 & 0 \\ 1 & * & 1 & 1 \\ 0 & 1 & * & 1 \end{array} \end{eqnarray*}
    • 4 列,23=8 行.各列に*が2つ,各行に*が1つ現れている.
    • 各*を0,1に置き換えると,16パターンすべてが丁度1回現れる. つまり 0000 から 1111 のいずれも,どれか1行にマッチする.
  • \(i\) 列目を変数 \(x_i\) で表す.
  • \(x_1=0\), \(x_2=0\), \(x_3=1\) の時, すなわち \(\bar{x}_1 \land \bar{x}_2 \land x_3\) の時,1行目にマッチする. 同様に \(\bar{x}_2 \land \bar{x}_3 \land x_4\) の時,2行目にマッチする.
  • \(x_1\), …, \(x_4\) がどのような値でも,8行中のいずれかにマッチするので, 以下の式 \(F\) はtautologyである. \begin{eqnarray*} F & = & (\bar{x}_1 \land \bar{x}_2 \land x_3) \lor (\bar{x}_2 \land \bar{x}_3 \land x_4) \lor \cdots \lor (\bar{x}_1 \land x_2 \land x_4) \end{eqnarray*}
  • したがって \(R = \bar{F}\) はunsatisfiableである.

3.3.1 参考資料

3.3.2 練習問題

  1. \(R\) がunsatisfiableであることをSATソルバーで確かめよ.
    (解答例)

    以下の内容のファイル abd43.sat を作成する.

    1 2 ~3
    2 3 ~4
    3 4 1
    4 ~1 2
    ~1 ~2 3
    ~2 ~3 4
    ~3 ~4 ~1
    ~4 1 ~2
    

    sat13で実行する.

    $ ./sat13 <abd43.sat
    (4 variables, 8 clauses, 24 literals successfully read)
    ~
    UNSAT
    Altogether 301+670 mems, 5804 bytes, 3 nodes, 3 clauses learned (ave 1.3->1.3), 60 memcells.
    (2 clauses were subsumed on-the-fly.)
    (1 restart.)
    

    MiniSatで実行する場合は, 以下の内容のファイル abd43.cnf を作成する.

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

    MiniSatで実行する.

    $ ./minisat abd43.cnf
    

    Copris のプログラム prog/taocp001.scala を用いる. 実行方法は以下の通り.

    $ scala -cp copris-all-v2-2-5.jar
    scala> :load taocp001.scala
    scala> abd43
    scala> find
    res: Boolean = false
    
  2. \(R\) がunsatisfiableであることをresolutionで確かめよ.
    (解答例)
    1. 最初の3つの節 \(12\bar{3}\), \(23\bar{4}\), \(341\) から2ステップのresolutionで \(12\) が得られる(確認せよ). 2番目以降の3つの節 \(23\bar{4}\), \(341\), \(4\bar{1}2\) からも2ステップのresolutionで \(23\) が得られる. 同様に \(34\), \(4\bar{1}\), \(\bar{1}\bar{2}\), \(\bar{2}\bar{3}\), \(\bar{3}\bar{4}\), \(\bar{4}1\) が得られる.
    2. \(\{12, 23, 34, 4\bar{1}, \bar{1}\bar{2}, \bar{2}\bar{3}, \bar{3}\bar{4}, \bar{4}1\}\) から resolutionでempty clauseを導出できる(確認せよ).
      • \(12\) と \(\bar{1}\bar{2}\) は \(1 = \bar{2}\) を意味していることに注意. \(1\bar{3}\) と \(\bar{1}3\) が導出できれば \(1 = 3\) を示したことになる.
  3. (式7)の解はいくつあるか? (式6)から別の節を1つ除いた場合はどうか.
    (解答例)

    2つある.別の節を除いた場合も同様に2つの解を持つ. ABD(4,3)の各行が,0000から1111の2通りにマッチすることに対応する.

  4. 他にどんなunsatisfiableなCNF formulaが考えられるだろうか?
    (解答例)

    3 variablesの3SAT \(\{123,12\bar{3},1\bar{2}3,1\bar{2}\bar{3},\bar{1}23,\bar{1}2\bar{3},\bar{1}\bar{2}3,\bar{1}\bar{2}\bar{3}\}\) は 明らかにunsatisfiable (\(R\) ほどinterestingではない).

    \(\{12,13,23,\bar{1}\bar{2},\bar{1}\bar{3},\bar{2}\bar{3}\}\) もunsatisfiable. \(x_1+x_2+x_3 \ge 2\) かつ \(x_1+x_2+x_3 \le 1\) を表している. \(x_1+x_2+x_3+x_4+x_5 \ge 3\) かつ \(x_1+x_2+x_3+x_4+x_5 \le 2\) を考えると, \(\{123,124,125,134,135,145,234,235,245,345, \bar{1}\bar{2}\bar{3},\bar{1}\bar{2}\bar{4},\bar{1}\bar{2}\bar{5},\bar{1}\bar{3}\bar{4},\bar{1}\bar{3}\bar{5}, \bar{1}\bar{4}\bar{5},\bar{2}\bar{3}\bar{4},\bar{2}\bar{3}\bar{5},\bar{2}\bar{4}\bar{5},\bar{3}\bar{4}\bar{5}\}\) が得られる.

    4 variablesでは \(R\) 以外にどんなformulaがあるだろうか?

  5. \((p+q+r \ge 2) \land (p+q+r \le 1)\) を表すCNF formulaがunsatisfiableであることをsat13で確かめよ.

3.3.3 関連するExercise

  • \(\blacktriangleright\) Exercise 10 \(\;\) [ 21 ]
  • Exercise 11 \(\;\) [ 27 ]

4 Example Applications

4.1 A simple example (van der Waerden number)

  • 長さ8の0と1の列 \(x_1x_2\cdots x_8\) で, どの3つの0も等距離で並ばず, どの3つの1も等距離で並ばないようにできるだろうか. つまり \(x_i = x_{i+d} = x_{i+2d}\) となる \(i\), \(d\) が存在してはならない.
  • 長さ8で条件を満たす列は存在する.
  • では長さ9の列は存在するだろうか? 条件をCNF formulaで書いてみる.
    • \(x_i = x_{i+d} = x_{i+2d} = 0\) でないことは \(x_i \lor x_{i+d} \lor x_{i+2d}\) と書ける.
    • \(x_i = x_{i+d} = x_{i+2d} = 1\) でないことは \(\bar{x}_i \lor \bar{x}_{i+d} \lor \bar{x}_{i+2d}\) と書ける.
    • したがって長さ9の列の条件は(式9)で表せる.
    • (式9)はunsatisfiableであり,長さ9の列は存在しない.
  • B. L. van der Waerden は, 任意の \(j\), \(k\) について, \(n\) が十分に大きい時,binary sequence \(x_1x_2\cdots x_n\) は必ず \(j\) 個の等間隔の0か, \(k\) 個の等間隔の1を含むことを示した. そのような最小の \(n\) を \(W(j,k)\) で表す.
    • 実際には B. L. van der Waerden は,0と1の2種類の数だけでなく, \(b\) 種類の数について同様の定理を証明した.
    • たとえば \(W(3,3,3)=27\) である. 長さ26の列としては 10100112002021122112020021 などがある.
  • binary sequence \(x_1x_2\cdots x_n\) が \(j\) 個の等間隔の0も \(k\) 個の等間隔の1も含まないことを意味する formula \(\textit{waerden}(j,k;n)\) は(式10)で与えられる.
    • \(\textit{waerden}(j,k;n)\) は \(n < W(j,k)\) の時だけ satisfiable である.
  • \(W(j,k)\) の値はかなりmysteriousである.
    • \(j=3\), \(k>4\) の時 \(W(j,k) < k^2\) のように見えるが, \(W(3,24) = 593 > 576 = 24^2\) である.
  • \(\textit{waerden}(j,k;n)\) 中のclauseはmonotonicである. すなわち,どのclauseもpositive literalかnegative literalだけを含む.
    • monotonicなSAT問題は簡単に解けるのだろうか? 実は,そうではない. Exercise 10で,どんなSAT問題もmonotonicな問題に変換できることを証明する.

4.1.1 参考資料

4.1.2 練習問題

  1. SATソルバーを用いて,(式9)がunsatisfiableであることを確かめよ.
    (解答例)

    以下の内容のファイル waerden-3-3-9.sat を作成する.

    1 2 3
    2 3 4
    3 4 5
    4 5 6
    5 6 7
    6 7 8
    7 8 9
    1 3 5
    2 4 6
    3 5 7
    4 6 8
    5 7 9
    1 4 7
    2 5 8
    3 6 9
    1 5 9
    ~1 ~2 ~3
    ~2 ~3 ~4
    ~3 ~4 ~5
    ~4 ~5 ~6
    ~5 ~6 ~7
    ~6 ~7 ~8
    ~7 ~8 ~9
    ~1 ~3 ~5
    ~2 ~4 ~6
    ~3 ~5 ~7
    ~4 ~6 ~8
    ~5 ~7 ~9
    ~1 ~4 ~7
    ~2 ~5 ~8
    ~3 ~6 ~9
    ~1 ~5 ~9
    

    sat13で実行する.

    $ ./sat13 <waerden-3-3-9.sat
    (9 variables, 32 clauses, 96 literals successfully read)
    ~
    UNSAT
    Altogether 663+2816 mems, 7025 bytes, 6 nodes, 6 clauses learned (ave 1.7->1.7), 219 memcells.
    (2 clauses were subsumed on-the-fly.)
    (2 restarts.)
    
  2. SATソルバーを用いて,長さ8の場合の解を1つ求めよ.
    (解答例)

    waerden-3-3-9.sat からvariable 9を含むclausesを削除し, waerden-3-3-8.sat として保存する.

    1 2 3
    2 3 4
    3 4 5
    4 5 6
    5 6 7
    6 7 8
    1 3 5
    2 4 6
    3 5 7
    4 6 8
    1 4 7
    2 5 8
    ~1 ~2 ~3
    ~2 ~3 ~4
    ~3 ~4 ~5
    ~4 ~5 ~6
    ~5 ~6 ~7
    ~6 ~7 ~8
    ~1 ~3 ~5
    ~2 ~4 ~6
    ~3 ~5 ~7
    ~4 ~6 ~8
    ~1 ~4 ~7
    ~2 ~5 ~8
    

    sat13で実行する.

    $ ./sat13 <waerden-3-3-8.sat
    (8 variables, 24 clauses, 72 literals successfully read)
    !SAT!
     6 ~5 ~4 3 ~2 8 ~7 1
    Altogether 561+666 mems, 6660 bytes, 5 nodes, 1 clauses learned (ave 3.0->3.0), 157 memcells.
    (1 restart.)
    

    この解は列 10100101 を表している.

  3. 上で求めた以外の解をSATソルバーで求めるにはどうすれば良いか.
    (解答例)

    waerden-3-3-8.sat に以下の1行を加える.

    ~1 2 ~3 4 5 ~6 7 ~8
    

    sat13で実行する.

    $ ./sat13 <waerden-3-3-8.sat
    (8 variables, 25 clauses, 80 literals successfully read)
    !SAT!
     6 ~5 ~4 3 2 ~1 7 ~8
    Altogether 576+1009 mems, 6736 bytes, 5 nodes, 2 clauses learned (ave 4.0->3.0), 176 memcells.
    (1 restart.)
    

    この解は列 01100110 を表している.

  4. (式10) \(\textit{waerden}(j,k;n)\) を生成するプログラムを作成せよ.
    (解答例)

    Javaのプログラムを prog/java/Waerden.java に示す.

    $ javac Waerden.java
    $ java Waerden 3 3 9 | ./sat13
    $ java Waerden 3 3 8 | ./sat13
    

    Scalaのプログラムを prog/sat001.scala に示す. このプログラムを scalac でコンパイルした後,以下のように実行する.

    $ scalac sat001.scala
    $ scala waerden 3 3 9 | ./sat13
    $ scala waerden 3 3 8 | ./sat13
    

    Copris のプログラムを prog/taocp001.scala に示す. 実行方法は以下の通り.

    $ scala -cp copris-all-v2-2-5.jar
    scala> :load taocp001.scala
    scala> waerden(3, 3, 9)
    scala> find
    res: Boolean = false
    

    長さ8の場合,答えは6通りある.

    scala> waerden(3, 3, 8)
    scala> solutions.foreach(println)
    scala> cancel
    scala> solutions.foreach(sol => println((1 to 8).map(i => if (sol(x(i))) 1 else 0).mkString))
    
  5. \(\textit{waerden}(4,4;34)\) の解の1つを求めよ.
    (解答例)

    以下のようにする.

    $ java Waerden 4 4 34 | ./sat13
    (34 variables, 352 clauses, 1408 literals successfully read)
    !SAT!
     12 10 ~18 17 ~19 ~22 15 ~20 21 24 16 ~31 ~3 ~14 26 ~11 27 ~33 ~30 ~9 ~25 32 6 4 28 13 ~8 ~7 ~29 2 5 23 ~1 34
    Altogether 4857+141856 mems, 21974 bytes, 132 nodes, 77 clauses learned (ave 7.5->6.7), 3225 memcells.
    (13 learned clauses were discarded.)
    (3 clauses were subsumed on-the-fly.)
    (25 restarts.)
    

    この解は,以下の列を表している.

    0101110001011011100010110111000101
    

    以下のようにすると実行にかかったCPU時間を求められる.

    $ java Waerden 4 4 34 | time ./sat13
    
  6. \(\textit{waerden}(5,5;177)\) はいくつのclausesになり,どれぐらいの時間で解が求められるか.
    (解答例)

    以下のようにする.

    $ java Waerden 4 4 34 | wc -l
    7656
    $ java Waerden 4 4 34 | time ./sat13
    
  7. \(\textit{waerden}(3,4;17)\) で 00 から始まる解はあるか.
  8. 同様の問題にラムゼー数がある(Wikipedia:ラムゼーの定理). 一例は「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」として知られている. すなわち,6頂点の完全グラフの辺を2色(たとえば赤と青)で塗り分けた時, どのように塗り分けても同色の辺からなる3角形が生じる. そのような3角形が現れない条件をCNF formulaで記述し, それがunsatisfiableであることを示せ.
    (解答例)

    頂点 \(i\) と頂点 \(j\) を結ぶ辺の色をvariable \(e_{ij}\) で表す (\(1 \le i < j \le 6\)). \(e_{ij}=0\) は赤, \(e_{ij}=1\) を青とする.

    どの3角形も,どれかの辺が青になることは以下のclausesで表せる. $$ e_{ij} \lor e_{jk} \lor e_{ik} \quad (1 \le i < j < k \le 6) $$

    どの3角形も,どれかの辺が赤になることは以下のclausesで表せる. $$ \bar{e}_{ij} \lor \bar{e}_{jk} \lor \bar{e}_{ik} \quad (1 \le i < j < k \le 6) $$

  9. Two-hundred-terabyte maths proof is largest ever

4.1.3 関連するExercise

  • Exercise 3 \(\;\) [ M21 ]
  • Exercise 4 \(\;\) [ 22 ]
  • Exercise 5 \(\;\) [ M46 ]
  • \(\blacktriangleright\) Exercise 6 \(\;\) [ HM37 ]
  • Exercise 7 \(\;\) [ 21 ]
  • \(\blacktriangleright\) Exercise 8 \(\;\) [ 20 ]
  • Exercise 9 \(\;\) [ 24 ]

4.2 Exact covering

  • Section 7.2.2.1 ではexact cover問題を "dancing links" を用いて解いたが, SATに定式化するのも簡単だ.
    • Exact cover問題は,与えられた集合 \(X\) と集合族 \(S \subset 2^X\) について, \(X\) の分割である \(S^* \subset S\) を選び出す問題である. \(S^*\) をexact coverと呼ぶ.
    • たとえば \(X = \{1,2,3,4,5,6,7\}\) で, \(S = \{\{1,4,7\}, \{1,4\}, \{4,5,7\}, \{3,5,6\}, \{2,3,6,7\}, \{2,7\}\}\) の時, \(S^* = \{\{1,4\}, \{3,5,6\}, \{2,7\}\}\) は \(X\) のexact coverである.
    • この問題は,以下の0-1行列で,各列に1が丁度1回現れるように,行を選ぶ問題である.
      1234567
      \(\{1,4,7\}\)1001001
      \(\{1,4\}\)1001000
      \(\{4,5,7\}\)0001101
      \(\{3,5,6\}\)0010110
      \(\{2,3,6,7\}\)0110011
      \(\{2,7\}\)0100001
    • 行を選んだ結果は以下のようになる.
      1234567
      \(\{1,4\}\)1001000
      \(\{3,5,6\}\)0010110
      \(\{2,7\}\)0100001
  • Langford pairの問題を考えよう.
    • Langford pair問題は,\(1,1,2,2,\ldots,n,n\) の \(2n\) の数を並び替えて, 各数 \(k\) について2つの \(k\) 間の距離が \(k\) になっている列を探す問題である. 詳しくはVolume 4Aの最初に述べられている.
    • \(n=3\) の時,列 231213 は条件を満たしている (2つある1の間の距離は1,2の距離は2,3の距離は3になっている). 41312432 は \(n=4\) の時, 46171435623725 は \(n=7\) の時の解の例である.
    • Langford pair問題は \(n=4m-1\) か \(n=4m\) の時だけ解を持つ. \(n=3,4\) の時の解は1つ(左右対称解を除く), \(n=7\) の時の解は26ある.
  • Langford pair問題はexact cover問題として定式化できる.
    • \(n=3\) として \(d_i\) (\(1\le i\le n\)), \(s_j\) (\(1\le j \le 2n\)) を行列の列とする. 数 \(i\) が \(j\) と \(k\) の位置に現れることを \(d_i s_j s_k\) で表し, 可能な \(d_i s_j s_k\) を行にする.
    • 以下の行列で,各列に1が丁度1回現れるように行を選択すれば良い. ただし,対称性から \(d_3 s_2 s_6\) の行は除去している.
      \(d_1\)\(d_2\)\(d_3\)\(s_1\)\(s_2\)\(s_3\)\(s_4\)\(s_5\)\(s_6\)
      \(d_1 s_1 s_3\)100101000
      \(d_1 s_2 s_4\)100010100
      \(d_1 s_3 s_5\)100001010
      \(d_1 s_4 s_6\)100000101
      \(d_2 s_1 s_4\)010100100
      \(d_2 s_2 s_5\)010010010
      \(d_2 s_3 s_6\)010001001
      \(d_3 s_1 s_5\)001100010
    • \(j\) 行目を選択することを \(x_j\) (\(1\le j\le 8\))で表す.
    • \(d_1\) の列を見ると1-4列のどれかひとつを選択するので \(x_1+x_2+x_3+x_4 = 1\) である.
    • 他の列も同様に考えると(式12)が得られる. ただし \(S_1(y_1,...,y_p)\) は \(\sum_{i=1}^p y_i = 1\) を表している.
    • \(\sum_{i=1}^p y_i = 1\) をCNF formulaにする最も簡単な方法は以下の通りである.
      • \(y_1\), …, \(y_p\) の少なともひとつは1なので \(y_1 \lor \cdots \lor y_p\) . これは \(\sum_{i=1}^p y_i \ge 1\) を表す.
      • \(y_1\) と \(y_2\) のどちらかは0なので \(\bar{y}_1 \lor \bar{y}_2\) . 2変数を選ぶ他の組合せについても同様なので, 結局 \(\bigwedge_{j=1}^{p-1}\bigwedge_{k=j+1}^{p} \bar{y}_j \lor \bar{y}_k\) . これは \(\sum_{i=1}^p y_i \le 1\) を表す.
      • この方法では,一般に \(S_1(y_1,...,y_p)\) は \(\binom{p}{2}+1\) 個のclause (式13)になる.
    • (式14)が \(n=3\) の場合のCNF formulaになる. 一般の \(n\) に対するCNF formulaを \(\textit{langford}(n)\) で表す.
    • \(S_1(y_1,...,y_5)\) 中の \((\bar{y}_1 \lor \bar{y}_4) \land (\bar{y}_1 \lor \bar{y}_5)\) は, 新しいvariable \(t\) を利用して \((\bar{y}_1 \lor \bar{t}) \land (t \lor \bar{y}_4) \land (t \lor \bar{y}_5)\) と表すことができる.
      • 新しいCNF式から,元のCNF式がresolutionで導出できることを確認せよ.
      • これは元のCNF式と同値な \((\bar{y}_1 \lor (\bar{y}_4 \land \bar{y}_5))\) において, \((\bar{y}_4 \land \bar{y}_5)\) の部分を \(\bar{t}\) で置き換えるTseitin変換に対応する.
    • 同じvariable \(t\) を使い, \((\bar{y}_2 \lor \bar{y}_4) \land (\bar{y}_2 \lor \bar{y}_5)\) を \((\bar{y}_2 \lor \bar{t})\) で, \((\bar{y}_3 \lor \bar{y}_4) \land (\bar{y}_3 \lor \bar{y}_5)\) を \((\bar{y}_3 \lor \bar{t})\) で 置き換えることができる. 結果は10個の節から成るCNF式になり,元の(式13)での11節より少なくなる.
    • Exercise 12で \(S_1(y_1,...,y_p)\) を, \(\lfloor (p-3)/2 \rfloor\) 個の新しいvariableと \(3p-5\) 個のclauseで表す方法を示す. これを用いた場合を \(\textit{langford}'(n)\) で表す.

4.2.2 練習問題

  1. \(n=3\) の時の行列で,各列に1が丁度1回現れるように行を選択せよ.
    (解答例)

    2,7,8行目を選択すれば良い.

    \(d_1\)\(d_2\)\(d_3\)\(s_1\)\(s_2\)\(s_3\)\(s_4\)\(s_5\)\(s_6\)
    \(d_1 s_2 s_4\)100010100
    \(d_2 s_3 s_6\)010001001
    \(d_3 s_1 s_5\)001100010
    これは解 312132 を表している.
  2. Knuthのdancing linksのアルゴリズム (Wikipedia:Knuth's Algorithm X)を \(n=3\) の行列に適用して見よ.
  3. \(n=4\) の行列はどのようになるか.(式12)に相当する式はどうなるか.
    (解答例)

    以下の17行12列の行列になる.

    \(d_1\)\(d_2\)\(d_3\)\(d_4\)\(s_1\)\(s_2\)\(s_3\)\(s_4\)\(s_5\)\(s_6\)\(s_7\)\(s_8\)
    \(d_1 s_1 s_3\)100010100000
    \(d_1 s_2 s_4\)100001010000
    \(d_1 s_3 s_5\)100000101000
    \(d_1 s_4 s_6\)100000010100
    \(d_1 s_5 s_7\)100000001010
    \(d_1 s_6 s_8\)100000000101
    \(d_2 s_1 s_4\)010010010000
    \(d_2 s_2 s_5\)010001001000
    \(d_2 s_3 s_6\)010000100100
    \(d_2 s_4 s_7\)010000010010
    \(d_2 s_5 s_8\)010000001001
    \(d_3 s_1 s_5\)001010001000
    \(d_3 s_2 s_6\)001001000100
    \(d_3 s_3 s_7\)001000100010
    \(d_3 s_4 s_8\)001000010001
    \(d_4 s_1 s_6\)000110000100
    \(d_4 s_2 s_7\)000101000010
    (式12)に相当する式は,以下から成る.
    • \(S_1(x_{1},x_{2},x_{3},x_{4},x_{5},x_{6})\)
    • \(S_1(x_{7},x_{8},x_{9},x_{10},x_{11})\)
    • \(S_1(x_{12},x_{13},x_{14},x_{15})\)
    • \(S_1(x_{16},x_{17})\)
    • \(S_1(x_{1},x_{7},x_{12},x_{16})\)
    • \(S_1(x_{2},x_{8},x_{13},x_{17})\)
    • \(S_1(x_{1},x_{3},x_{9},x_{14})\)
    • \(S_1(x_{2},x_{4},x_{7},x_{10},x_{15})\)
    • \(S_1(x_{3},x_{5},x_{8},x_{11},x_{12})\)
    • \(S_1(x_{4},x_{6},x_{9},x_{13},x_{16})\)
    • \(S_1(x_{5},x_{10},x_{14},x_{17})\)
    • \(S_1(x_{6},x_{11},x_{15})\)
  4. \(\textit{langford}(n)\) を生成するプログラムを作成せよ.
    (解答例)

    Javaのプログラムを prog/java/Langford.java に示す.

    $ javac Langford.java
    $ java Langford 3 | ./sat13
    (8 variables, 32 clauses, 70 literals successfully read)
    !SAT!
     8 ~6 ~3 ~5 ~1 2 ~4 7
    Altogether 748+171 mems, 6600 bytes, 0 nodes, 0 clauses learned, 92 memcells.
    (0 restarts.)
    

    これは2,7,8行目を選択することを表している.

    Scalaのプログラムを prog/sat001.scala に示す.

    $ scalac sat001.scala
    $ scala langford 3 | ./sat13
    
  5. \(\textit{langford}'(n)\) を生成するプログラムを作成せよ.
    (解答例)

    Scalaのプログラムを prog/sat001.scala に示す.

    $ scalac sat001.scala
    $ scala langford1 3 | ./sat13
    
  6. \(y_1 + \cdots + y_p = 1\) あるいは \(y_1 + \cdots + y_p \ge 1\) や \(y_1 + \cdots + y_p \le 1\) の条件を用いると, 多くの問題を表現できる. 例えば エイト・クイーン の問題はどのように表現できるだろうか.

4.2.3 関連するExercise

  • Exercise 12 \(\;\) [ 21 ]
  • Exercise 13 \(\;\) [ 24 ]

4.3 Coloring a graph

  • 与えられたグラフの各頂点を \(d\) 色で塗り分け,辺で結ばれている頂点が異なる色に なるようにする問題.
  • \(G(V,E)\) を \(n\) 頂点からなるグラフとする.
  • 各頂点 \(v \in V\), 各値 \(1 \le j \le d\) に対しvariable \(v_j\) を導入する. \(v_j\) は,頂点 \(v\) が色 \(j\) で塗られていることを表す.
  • clauseは以下のようになる.
    • \((v_1 \lor \cdots \lor v_d)\) for \(v \in V\)
    • \((\bar{u}_j \lor \bar{v}_j)\) for \(u\)—\(v\), \(1 \le j \le d\)
  • 以下の exclusion clauses を加えても良い. しかし,頂点が2色以上で塗られていても問題ないため,不要である.
    • \((\bar{v}_i \lor \bar{v}_j)\) for \(v \in V\), \(1 \le i<j \le d\)
  • Fig. 33はthe McGregor graph of order 10である.
    • 110の領域(頂点), 324の辺(隣接している境界)を持っている.
    • Martin Gardnerが1975年4月のScientific Americanで四色問題の反例 (5色が必要な例)だとして,エイプリルフールの冗談で示したものである. その後,四色問題は証明され四色定理となっている.
    • このグラフの4彩色を求めるのは簡単である.
  • Randal Bryantは,色1を7回だけ使うという条件を加えても,Fig. 33を4彩色できることを示した.
  • 色1を7回以下使うという制約は,様々に表すことができる.
    • 110頂点から任意の8頂点を選び,いずれかは色1でない,とすれば良い. しかしこれは \(\binom{100}{8} = 409,705,619,895\) にもなる.
  • この \(x_1 + \cdots + x_n \le r\) のような制約 (at-most-\(r\) 基数制約と呼ばれる) をうまく表現する方法にはいくつかある.
    • C. Sinzの方法 (式18), (式19)
    • O. Bailleux and Y. Boufkhadの方法 (式20), (式21)
  • \(x_1 + \cdots + x_n \ge r\) (at-least-\(r\) 基数制約)も同様にできる.
    • \(S_{\ge r}(x_1,\ldots,x_n) = S_{\le n-r}(\bar{x}_1,\ldots,\bar{x}_n)\)

4.3.2 練習問題

  1. Exercise 15のグラフが4彩色可能かどうかをSATソルバーで判定せよ.
    (解答例)

    prog/mcgregor3-4.sat を用いる. 以下のように4彩色可能である.

    $ ./sat13 <mcgregor3-4.sat
    (48 variables, 204 clauses, 432 literals successfully read)
    !SAT!
     ~2.1=3 ~2.1=4 ~2.1=2 2.1=1 ~2.2=1 ~3.1=1 ~3.2=1 ~2.0=1 ~1.2=1 ~3.1=4 ~3.1=2 3.1=3 ~3.2=3 ~3.0=3 ~2.0=3 ~1.0=3 ~0.0=3 2.0=4 ~2.2=4 ~3.0=4 ~1.1=4 ~2.0=2 ~1.0=2 ~1.1=1 3.0=2 ~1.1=2 ~0.0=2 ~3.0=1 1.1=3 ~1.2=3 ~2.2=3 ~0.1=3 2.2=2 ~1.2=2 1.2=4 ~3.2=4 ~0.2=4 ~0.1=4 3.2=2 ~0.2=2 ~0.1=2 0.1=1 ~0.2=1 ~0.0=1 0.2=3 0.0=4 ~1.0=4 1.0=1
    Altogether 4209+5721 mems, 14140 bytes, 25 nodes, 3 clauses learned (ave 6.7->6.7), 473 memcells.
    (2 restarts.)
    
  2. Fig. 33のMcGregorグラフが4彩色可能かどうかをSATソルバーで判定せよ.
    (解答例)

    Scalaのプログラム prog/sat001.scala を用いる. このプログラムを以下のようにコンパイル・実行する.

    $ scalac sat001.scala
    $ scala mcgregor 10 4 | ./sat13
    

    どのように彩色されたかは以下でわかる.

    $ scala mcgregor 10 4 | ./sat13 | tr " " "\n" | grep -v '^~' | sort -n
    

    あるいは以下のようにする.

    $ scala mcgregor 10 4 | ./sat13 | scala mcgregorDecode
    

    3彩色はできない.

    $ scala mcgregor 10 3 | ./sat13
    
  3. at-most-\(r\) 基数制約をSinzの方法で符号化するプログラムを作成せよ.
    (解答例)

    Scalaのプログラム prog/sat001.scala を用いる. このプログラムを以下のように実行する.

    $ scala sinz 10 4 | ./sat13
    
  4. Sinzの方法を用いて,McGregorグラフで色1が7回以下の彩色を求めよ.
  5. at-most-\(r\) 基数制約をBailleux and Boufkhadの方法で符号化するプログラムを作成せよ.
  6. 数独はグラフ彩色問題の一種である.数独の問題をSAT問題に符号化するプログラムを作成せよ.

4.3.3 関連するExercise

  • Exercise 14 \(\;\) [ 22 ]
  • Exercise 15 \(\;\) [ 24 ]
  • Exercise 16 \(\;\) [ 21 ]
  • Exercise 17 \(\;\) [ 26 ]
  • \(\blacktriangleright\) Exercise 18 \(\;\) [ 28 ]
  • \(\blacktriangleright\) Exercise 19 \(\;\) [ 29 ]
  • Exercise 20 \(\;\) [ 40 ]
  • Exercise 21 \(\;\) [ 22 ]
  • Exercise 22 \(\;\) [ 20 ]
  • Exercise 23 \(\;\) [ 20 ]
  • \(\blacktriangleright\) Exercise 24 \(\;\) [ M32 ]
  • Exercise 25 \(\;\) [ 21 ]
  • Exercise 26 \(\;\) [ 22 ]
  • Exercise 27 \(\;\) [ 20 ]
  • \(\blacktriangleright\) Exercise 28 \(\;\) [ 20 ]
  • \(\blacktriangleright\) Exercise 29 \(\;\) [ 20 ]
  • \(\blacktriangleright\) Exercise 30 \(\;\) [ 22 ]
  • \(\blacktriangleright\) Exercise 31 \(\;\) [ 28 ]
  • Exercise 32 \(\;\) [ 15 ]
  • Exercise 33 \(\;\) [ 21 ]
  • Exercise 34 \(\;\) [ HM26 ]
  • Exercise 35 \(\;\) [ 22 ]
  • \(\blacktriangleright\) Exercise 36 \(\;\) [ 22 ]
  • Exercise 37 \(\;\) [ 20 ]
  • Exercise 38 \(\;\) [ M25 ]
  • Exercise 39 \(\;\) [ M46 ]

4.4 Factoring integers

  • \(z\) を \((m+n)\) ビットの2進数 \((z_{m+n}\ldots z_2 z_1)_2\) とする.
  • \(z=x\times y\) となる \(m\) ビットの2進数 \(x=(x_m\ldots x_2 x_1)_2\) と \(n\) ビットの2進数 \(y=(y_n\ldots y_2 y_1)_2\) は存在するだろうか?
  • \(m=2\), \(n=3\), \(z=21=(10101)_2\) の時,(式22)を満たす解は存在するが, \(z=19=(10011)_2\) の時は存在しない.
  • (式22)は,(式23)で表すことができる. \(\oplus\) は排他的論理和(XOR)である.
  • (式23)は,(式24)を用いて49個のclausesで表すことができ, \(z=21\) は5つのclauseで表すことができる.
    • (式24)と同様の方法はTseytin encodingと呼ばれる.
  • 49+5 clauses は効率が悪そうに見えるかも知れない. あとで \(6mn\) より少ない variables, \(20mn\) より少ない clauses で表せることを示す.
  • (式23)は「ネイピアの骨」の方法を近代化したLuigi Daddaの方法で導き出すことができる.
    • 複数のビットを蓄える場所として \(bin[2], \ldots, bin[m+n]\) を準備する.
    • 各 \(x_i \land y_j\) を \(bin[i+j]\) に入れる.
    • \(k=2,3,\ldots\) の順に \(bin[k]\) を見る.
    • \(bin[k]\) 中のビットが1つの場合,それが \(b\) の時 \(z_{k-1} \leftarrow b\) とする.
    • \(bin[k]\) 中のビットが2つの場合,それらが \(b\), \(b'\) の時 \(z_{k-1} \leftarrow b\oplus b'\) とし, \(bin[k+1]\) に \(b\land b'\) を入れる.
    • \(bin[k]\) 中のビットが3つ以上の場合,それらが \(b\), \(b'\), \(b''\) の時 \(r \leftarrow b\oplus b'\oplus b''\), \(c \leftarrow \langle b b' b''\rangle\) とし, \(r\) を \(bin[k]\) に \(c\) を \(bin[k+1]\) に入れる. ただし \(\langle b b' b''\rangle\) は \(b\), \(b'\), \(b''\) の median を表す (Volume 4AのSection 7.1.1を参照).
  • \(bin[k]\) からどのようにビットを取り出すかで,様々な方法が考えられる.
    • \(\textit{factor_fifo}(m,n,z)\): FIFOキュー
    • \(\textit{factor_lifo}(m,n,z)\): LIFOキュー
    • \(\textit{factor_rand}(m,n,z,s)\): ランダム (\(s\) は乱数シード)
  • 整数論に関する何の知識も用いずに factoring が行えていることに注意!

4.4.2 練習問題

  1. \(z=21\) に対し(式23)から得られるSAT問題の解を求めよ.
    (解答例)

    prog/mult-2-3-21.sat を用いる. 以下のように2-bit x 3bit にfactoring可能である.

    $ ./sat13 <mult-2-3-21.sat
    
  2. 上のSAT問題を修正し \(z=19=(10011)_2\) の時にUNSATとなることを確認せよ.
  3. \(\textit{factor_fifo}(m,n,z)\) を作成せよ.
    (解答例)

    Scalaのプログラム prog/sat001.scala を用いる. このプログラムを以下のように実行すると,乗算回路の(式23)が表示される.

    $ scala prod 2 3
    

    以下のようにするとSATに符号化され,factoringが実行される.

    $ scala prod 2 3 | scala daddaEncode 5 10101 | ./sat13
    

    ここで daddaEncode の引数の5は z のビット数,10101は z の2進表現である.

    ただしこのプログラムは上で示したDaddaの方法とは少し異なっており, \(z\) の \(i\) ビット目が \(bin[i]\) に入るようにしている.

  4. 上のプログラムを使って,やや大きな素数の積を素因数分解してみよう. たとえば素数 \(32719=111111111001111_2\) と素数 \(32749=111111111101101_2\) の積は \(1071514531=111111110111100000001110100011_2\) である.
    (解答例)

    Scalaのプログラム prog/sat001.scala を用いる.

    $ scala prod 15 15 | scala daddaEncode 30 111111110111100000001110100011 | ./sat13
    

    以下のようにすると x と y のビット表現がわかる.

    $ scala prod 15 15 | scala daddaEncode 30 111111110111100000001110100011 | ./sat13 >/tmp/out
    $ tr ' ' '\n' </tmp/out | grep x
    $ tr ' ' '\n' </tmp/out | grep y
    

    以下のプログラムも用意されている.

    $ scala daddaDecode </tmp/out
    x = 111111111101101 (32749)
    y = 111111111001111 (32719)
    z = 111111110111100000001110100011 (1071514531)
    
  5. 上のプログラムを使って \(z=x^2\) を表すにはどうすれば良いか?
    (解答例)

    すべての \(x_i \land x_j\) を \(bin[i+j]\) に入れた後, Dadda のアルゴリズムを実行すれば良い.

    ただし prog/sat001.scala のDaddaクラスを用いる場合は, すべての \(x_i \land x_j\) を \(bin[i+j-1]\) に入れる.

  6. 平方数で2進表現が回文になっているものを探せ.
    (解答例)

    \(z=x^2\) が \(n\) ビットの時, \(z_1=z_n\), \(z_2=z_{n-1}\), \(\ldots\) を満たせば良い. また最上位ビット \(z_n=1\) として良い (すなわち \(z_1=1\) でもある).

    \(n=1\) の時 \(z=1^2=1=1_2\) は回文, \(n=4\) の時 \(z=3^2=9=1001_2\) は回文になっている. 他にあるだろうか?

    \(n\) が奇数の場合があることに注意する. \(n=2m\) の時の \(x\) は \(m\) ビットだが, \(n=2m-1\) の時の \(x\) も \(m\) ビットである.

  7. 上のプログラムを使って \(z=x^2+y^2\) を表すにはどうすれば良いか?
    (解答例)

    すべての \(x_i \land x_j\) を \(bin[i+j]\) に入れ, すべての \(y_i \land y_j\) を \(bin[i+j]\) に入れた後, Dadda のアルゴリズムを実行すれば良い.

    ただし prog/sat001.scala のDaddaクラスを用いる場合は, \(bin[i+j-1]\) に入れる.

  8. 上のプログラムを使って \(z=x^3\) を表すにはどうすれば良いか?
    (解答例)

    すべての \(x_i \land x_j \land x_k\) を \(bin[i+j+k-1]\) に入れた後, Dadda のアルゴリズムを実行すれば良い.

    ただし prog/sat001.scala のDaddaクラスを用いる場合は, \(bin[i+j+k-2]\) に入れる.

  9. 三角数で2進表現が回文になっているものを探せ.
  10. \(\sqrt{2}\) を計算するにはどうすれば良いか?

4.4.3 関連するExercise

  • Exercise 40 \(\;\) [ 01 ]
  • Exercise 41 \(\;\) [ M21 ]
  • Exercise 42 \(\;\) [ 21 ]
  • \(\blacktriangleright\) Exercise 43 \(\;\) [ 21 ]
  • \(\blacktriangleright\) Exercise 44 \(\;\) [ 30 ]
  • Exercise 45 \(\;\) [ 20 ]
  • Exercise 46 \(\;\) [ 30 ]

4.5 TODO Fault testing

  • 回路の故障を検出する問題を考える. 故障としては1箇所の信号が 0 か 1 かにstuckされる場合を対象とする (single-stuck-at fault).
  • Fig. 34は(式23)の回路である.
    • \(z_5z_4z_3z_2z_1\) が出力 \(y_3y_2y_1x_2x_1\) が入力
    • 15個のAND, OR, XOR gates (それぞれ2入力1出力)
    • 15箇所のfanout gates (ドットで示されている.1入力を2出力に)
    • したがって50個の信号を持つ (50箇所の各wire毎)
    • 一般に \(m\) outputs, \(n\) inputs, \(g\) gates から成る回路は \(g+m-n\) fanout gates, \(3g+2m-n\) wires を持つ.
  • Fig. 34は100通りのsingle-stuck-at faultの可能性がある.
    • 50箇所のwireのうち,あるwireが0にstuckする場合と1にstuckする場合
  • Table 1は \(x_2x_1=11\), \(y_3y_2y_1=110\) の場合の各信号の値の表である. 左端OKの列は正しい場合を表している. 残りの100個の列は,100通りのsingle-stuck-at faultに対応する.
    • \(x^1_1\) が0にstuckしている場合, 出力 \(z_5z_4z_3z_2z_1\) は 01100 となり,正しい結果 10010 とは異なる. したがってこの入力で \(x^1_1\) が0にstuckするエラーは検出可能である.
    • \(x_2x_1=11\), \(y_3y_2y_1=110\) の入力パターンで44通りのfaultを検出できる.
  • \(2^5\) 通りのすべてのテストパターンに対する出力を調べれば,あらゆる single-stuck-at faultを検出できるだろう.
    • 実際には "\(s^2\) stuck at 1" は絶対に検出できない.
    • つまり(式23)で \(q \leftarrow s \land c_1\), \(c_2 \leftarrow p \lor q\) は冗長なので, \(c_2 \leftarrow p \lor c_1\) とできる.
  • しかしうまくテストパターンを選べば,もっと少ない組合せですべてのfaultを検出できる.
    • Fig. 34の場合 5つのテストパターンで良い(Exercise 49).
  • 32ビット2入力,64ビット1出力の乗算回路 \(prod(32,32)\) を考えよう.
    • 上記の \(\textit{factor_fifo}\) を用いると, 64 inputs, 64 outputs, 3660 AND gates, 1203 OR gates, 2145 XOR gates および 7008 fanout gatees, 21088 wires を持つ回路が得られる.
    • 42176通りのfaultsをいくつのテストパターンでカバーできるだろうか?
    • ランダムに選んだテストパターンでも多くの場合をカバーする.
      • \(x={}^{\#}3243F6A8\), \(y={}^{\#}885A308D\) のテストパターンは14733通りを検出する.
      • \(x={}^{\#}2B7E1516\), \(y={}^{\#}28AED2A6\) はさらに6918通りを検出する.
      • 例えば,ランダムに選んだ243のテストパターンで140通りを残してカバーできる.
    • 残りの140通りをカバーするテストパターンをSATソルバーを用いて探してみよう.
  • 以下,作成中

4.5.2 関連するExercise

  • \(\blacktriangleright\) Exercise 47 \(\;\) [ 20 ]
  • Exercise 48 \(\;\) [ 20 ]
  • Exercise 49 \(\;\) [ 24 ]
  • Exercise 50 \(\;\) [ 24 ]
  • Exercise 51 \(\;\) [ 40 ]

4.6 TODO Learning a Boolean function

  • 作成中

4.7 TODO Bounded model checking

  • 作成中

4.8 TODO Applications to mutual exclusion

  • 与えられたアルゴリズムが正しい(あるいは間違っている)ことを示すためにBMCを応用する.
    • 最も挑戦的な課題のひとつは,並行動作する並列プロセスの同期の検証の問題である.
  • AliceとBobは,アパートをシェアして,各自の部屋と共用の部屋がある.
    • 共用部屋には各自の部屋から繋がるふたつのドアがある.
    • 共用部屋に一方が居る時,他方が共用部屋に入らないようにしたい.
    • そこでライトを使うことにした.
  • 以下 prog/sat010.scala を使用する
  • プロトコル (式40)
    $ scalac sat010.scala
    $ scala protocol40 5 | ./sat13 | scala protocolDecode
    $ scala protocol40 6 | ./sat13 | scala protocolDecode
    
    • 相互排除できていない
  • プロトコル (式43)
    $ scala protocol43 100 | ./sat13 | scala protocolDecode
    
    • 相互排除できているが,交互にしか共用部屋を利用できない
  • プロトコル (式44)
    • ライトを2つ使うことにした
      $ scala protocol44 5 | ./sat13 | scala protocolDecode
      $ scala protocol44 6 | ./sat13 | scala protocolDecode
      
    • 相互排除できていない
  • プロトコル (式45)
    $ scala protocol45 100 | ./sat13 | scala protocolDecode
    
    • 相互排除できているが,deadlockが生じうる
  • プロトコル (式46)
    • Edsger Dijkstraのアルゴリズム
    • 相互排除できておりdeadlockは生じない
      $ scala protocol46 100 | ./sat13 | scala protocolDecode
      
    • starvationが生じうる
      $ scala protocol46s 8 | ./sat13 | scala protocolDecode
      
      • \(X_2 = X_8\) であり,Aliceは A1→A2→A3→A1 とloopしている
  • プロトコル (式49)
    • G. L. Petersonのアルゴリズム
    • 相互排除できておりdeadlock, starvationは生じない
      $ scala protocol49 50 | ./sat13 | scala protocolDecode
      $ scala protocol49s 50 | ./sat13 | scala protocolDecode
      

4.8.2 関連するExercise

  • Exercise 87 \(\;\) [ 21 ]
  • Exercise 88 \(\;\) [ 18 ]
  • Exercise 89 \(\;\) [ 21 ]
  • Exercise 90 \(\;\) [ 20 ]
  • Exercise 91 \(\;\) [ M21 ]
  • Exercise 92 \(\;\) [ 20 ]
  • Exercise 93 \(\;\) [ 20 ]
  • \(\blacktriangleright\) Exercise 94 \(\;\) [ 21 ]
  • Exercise 95 \(\;\) [ 20 ]
  • Exercise 96 \(\;\) [ 22 ]
  • Exercise 97 \(\;\) [ 20 ]
  • \(\blacktriangleright\) Exercise 98 \(\;\) [ M23 ]
  • Exercise 99 \(\;\) [ 25 ]
  • Exercise 100 \(\;\) [ 22 ]
  • \(\blacktriangleright\) Exercise 101 \(\;\) [ 31 ]
  • Exercise 102 \(\;\) [ 22 ]

4.9 TODO Digital tomography

  • 作成中

4.10 TODO

?????

Date:

Author: 神戸大学 情報基盤センター 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0