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

Table of Contents

1 概要

本稿では Donald E. 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先生とTAOCPについて

1.2.1 Knuth先生について

  • 略歴
  • 主な研究業績
  • 主な著作
    • The Art of Computer Programming (TAOCP)
    • Computers & Typesetting
      • Volume A: The TeXbook
      • Volume B: TeX: The Program
      • Volume C: The METAFONTbook
      • Volume D: METAFONT: The Program
      • Volume E: Computer Modern Typefaces
    • 『文芸的プログラミング』
    • 『超現実数 数学小説』
    • Mathematical Writing (『クヌース先生のドキュメント纂法』)

1.2.2 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

Coders at Work でも多くのプログラマはTAOCPを読むべき本として挙げている.

原著は以下の通りの構成である. 最初の出版は1968年だから,すでに50年が経過している!

  • 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, 準備中.
    • Fascicle 5: Mathematical Preliminaries Redux; Backtracking; Dancing Links, 2018 (出版予定).
    • Fascicle 6: Satisfiability, 2015.
  • Volume 4C: Combinatorial Algorithms, Part 3, 準備中.
  • Volume 4D: Combinatorial Algorithms, Part 4, 準備中.
  • Volume 5: Syntactic Algorithms, 準備中.
  • Volume 6: 準備中.
  • Volume 7: 準備中.

4A-4D巻は,まず分冊の形で出版され,その後,巻にまとめられる方法が取られている. 日本語訳は アスキードワンゴ から出版されている. また,最新のドラフト版の一部は https://www-cs-faculty.stanford.edu/~knuth/news.html あるいは Wikipedia: The Art of Computer Programming からダウンロードできる.

1.3 進め方

  • 各自で,テキストを読む.
  • 原著の演習問題に取り組む.
    • 演習問題に付いている印や数の意味については,下記を参照.
  • 下のそれぞれの節で示している練習問題に取り組む.
    • (★) 印の付いている練習問題は,講義全体の最終課題としてお薦めのものである.
    • 基本的には,Knuth先生作のSATソルバーを利用する.
    • 解答例は「 Knuth版SATソルバーのインストール 」にしたがってプログラムがインストールされ, Desktop/taocp-sat/prog フォルダで実行するものと仮定している.
    • プログラムを各自で作成する場合,プログラミング言語は自分の好きなものを用いて良い. 本テキスト中ではScalaのプログラムを解答例として示している場合がある.
  • 可能なら以下に挑戦する.

1.3.1 原著の演習問題に付いている印や数の意味

  • ► = 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

2 序文 (PREFACE)

2.1 序文

2.1.1 概要

  • Knuthがなぜ充足可能性問題を重要と思っているのかが述べられている.

2.1.2 注釈

  • 段落1: 本書は4B巻としてまとめられる前の分冊である.
  • 段落7: SATソルバーの速度は2001年頃に非常に速くなり, それまでのプログラムと比較して数百倍の速度向上が実現された. 現代的なSATソルバー (Modern SAT solvers)は,数百万個の変数,数千万個の節を含む問題でも取り扱うことができる.
  • 段落8: アルゴリズムWはWalkSAT, アルゴリズムLはmarch, アルゴリズムCはMiniSATなどの CDCL (Conflict Driven Clause Learning)型ソルバーに対応している.
  • 段落10: Knuth版プログラムのインストールについては「 Knuth版SATソルバーのインストール 」を参照のこと. インストール後のpdfディレクトリ中に説明文書があり,原著では述べられていない詳細がわかる.
  • 段落12: 原著の間違いなどの報告方法については「 The Art of Computer Programming 」中に記載がある. 最初の報告者に対しては knuth-check-20150910.png のような小切手が届き, The Bank of San Serriffe に名前が記載される. この銀行はPincus星にあるとされている架空の銀行である. 特にKnuthは, https://www-cs-faculty.stanford.edu/~knuth/news.html にリストされている演習問題の回答の 確認を希望している.

代表的なCDCL型SATソルバーとしては,以下が挙げられる. いずれも,安定して優れた性能を示している.

2.1.3 参考資料

2.1.4 練習問題

  1. 序文を読んで興味を持った文章はあるか.
  2. SATソルバーとその応用についてWebで検索し調べ,自分の興味がある応用を探せ.
  3. SATソルバーの実装についてWebで検索し調べよ.どのソルバーが速いと思うか.
    (解答例)

    定期的にSATソルバーの性能を競い合う SAT競技会 が開催されている. その上位のソルバーは,優れた性能を持つといえる. 特に,Main track (あるいはApplication track)の SAT+UNSAT で優秀なものを選ぶと良い.

  4. 命題論理 を復習すること.
    • 充足可能,恒真,連言標準形 (乗法標準形),選言標準形 (加法標準形),Tseitin変換
  5. 命題論理の推論体系 を復習すること.
    • 融合原理 (導出原理)
  6. Knuth版SATソルバーのインストール 」を参照し,Knuth版プログラムをインストールせよ.
  7. knuth/pdf/sat0.pdf の最初のページを読み,Knuth版SATソルバーの入力形式を調べよ.
  8. knuth/pdf/sat13.pdf の3ページ目を読み,sat13に対するオプションを調べよ.
  9. 上に挙げたGlueMiniSat, Sat4jなどのSATソルバーでは,DIMACS CNFが入力形式として用いられている. DIMACS CNF形式についてWebで検索し調べよ.

3 充足可能性 (SATISFIABILITY)

3.1 定義

3.1.1 概要

  • リテラル,節,CNFなどの定義が述べられている.

3.1.2 注釈

  • 段落1: 命題論理については,4A巻「7.1.1 Boole演算の基礎」以降で説明されている.
  • 段落1: Boole式 (Boolean formula)は,通常はブール式や命題論理式という. 本シリーズでは,人名などの固有名詞は原則として原文のまま綴っている. ``Boolean''の語源は,人名のGeorge Booleなので,本シリーズの翻訳方針にしたがい 他の巻と同様にBoole式と呼ぶ.
  • 段落1: 乗法標準形は,連言標準形,論理積標準形,和積標準形と呼ばれることもある.
  • 段落2: 充足可能性問題 (satisfiability problem)は, 充足可能性判定問題 (satisfiability testing problem)ということも多い. 充足可能性問題の具体的問題は,通常,乗法標準形で与えられる. 良く知られているように,どんなBoole式も同値な乗法標準形の式に変換できる. また,後述のTseytin変換を用いれば,任意のBoole式は充足可能性が同等な乗法標準形の式に線形時間で変換できる. なお,加法標準形のBoole式の充足可能性は直ちに判定できるから,問題としての意味がない.
  • 段落2: 充足可能性問題がNP-完全 (NP-complete)であることは,1971年にStephen Cookが証明した. したがって現時点では充足可能性問題を判定する多項式時間のアルゴリズムは知られていない. 一方, \(n\) 個の変数を含む命題論理式に対する可能は値割当ては \(2^n\) 通りあり, それらすべてを調べれば充足可能性は必ず判定できるから,指数時間のアルゴリズムは存在する.
  • 段落3: 百万個の変数を含む問題について, 基本的に調べるべき組合せの数は \(2^{1000000}\) すなわち約 \(10^{300000}\) であり,とんでもなく大きな数だ. 核時間 (光が水素原子を横切る時間であり約 \(10^{-18}\) 秒)で1通りを調べることができるとし, 1日を \(10^5\) 秒として \(10^{300000-18-5} = 10^{299977}\) 日がかかる. さらに宇宙にある原子個 (\(10^{80}\) と考えられている)の並列計算が可能だとしても,わずかに80桁が減るだけだ. 充足可能性問題などに対しては,アルゴリズムの改良なしにはスーパー・コンピュータといえども役に立たない. 量子コンピュータだとどうだろうか.
  • 段落5: 変数の補元は,通常の数理論理学の用語では,変数 \(x\) の否定 (negation) \(\lnot x\) のことである. 4A巻7.1.1では,補元 ではなく補数としている.
  • 段落9: \(L\) が \(n\) 個のリテラルの集合で, \(T_n\) を被覆しているなら, 各 \(i\) について \(x_i\) か \(\bar x_i\) のどちらか一方が \(L\) に含まれている点に注意する.
  • 段落10: ここで,節の族 (family)と書かれているが,節の集合 (set)と理解して問題ない. 節が集合の場合,集合の集合となるので族と説明されている.
  • 段落12: De Morganの法則は,日本語訳4A巻48ページにある. トートロジー(あるいは同語反復)とは,常に真となる論理式のことを指す. 式(5)は加法標準形 (disjunctive normal form; DNF)の式である.
  • 段落13: SAT problemは充足可能性問題そのものを指し, SAT instanceはその具体的問題を指す.
  • 段落14: 空節は \(\Box\) で表されることも多い.
  • 段落15: 演習問題28でも述べられているように, SATのどんな具体的問題も3SATの形式に容易に変換できる. 例えば,長さ \(n\ge 4\) の節 \((x_1\lor x_2\lor x_3\lor\cdots\lor x_n)\) は, 新しい変数 \(z\) を導入し, 2つの節 \((z\lor x_3\lor\cdots\lor x_n)\), \((\bar z\lor x_1\lor x_2)\) に置き換えることができる. これによって節の長さ \(n\) は1減少するから,この置き換えを繰り返すことで, すべての節の長さを3以下にできる. なお,すべての節が2個のリテラルからなる2SATは,多項式時間で解けることがわかっている.
  • 段落16: つまり,SATの具体的問題中にトートロジー的な節があった場合, 単にそれらを取り除けば良い.

3.1.4 関連する原著の演習問題

  • Exercise 1  [ 10 ] 

3.1.5 練習問題

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

    \((\bar{x} \lor \bar{y}) \land (x \lor y)\) など.

  3. \(x \imp y\) が「 \(x\) ならば \(y\) 」を表す時, \((x \imp y) \land (y \imp x)\) と同値なCNFは何か.
    (解答例)

    \(x \imp y\) は \(\bar{x} \lor y\) と同値である. したがって \((\bar{x} \lor y) \land (y \lor \bar{x})\) と書ける.

  4. \((x_1 \land x_2) \imp (y_1 \lor y_2)\) と同値なCNFは何か.
    (解答例)

    \(\bar{x}_1 \lor \bar{x}_2 \lor y_1 \lor y_2\) など.

  5. \((x_1 \land x_2) \imp (y_1 \land y_2)\) と同値なCNFは何か.
    (解答例)

    \((\bar{x}_1 \lor \bar{x}_2 \lor y_1) \land (\bar{x}_1 \lor \bar{x}_2 \lor y_2)\) など.

  6. \(\{\bar{1}\bar{2}, \bar{1}2, 1\bar{2}, 12\}\) は充足可能か.
    (解答例)

    充足不能.

  7. 式(7)と \(T_4\) を被覆する4個のリテラルの集合は何か.
    (解答例)

    \(\{4,\bar{1},2,3\}\) と \(\{4,\bar{1},2,\bar{3}\}\) がある.

  8. 原著の演習問題1を解け.
  9. 与えられたCNFがトートロジーかどうかは簡単に判定できる.なぜか.
    (解答例)

    すべての節がトートロジー的かどうかを調べれば良い. すべてがトートロジー的なら,CNF式はトートロジーである. トートロジー的でない節 \(\{l_1,l_2,\ldots,l_n\}\) が存在すれば, \(l_i=0\) とする値割当てで偽になるから,トートロジーではない.

  10. 与えられたDNFの充足可能性は簡単に判定できる.なぜか.
    (解答例)

    CNFの場合と双対に考えれば良い.

  11. CNFで,ある変数 \(x\) が,正リテラルか負リテラルかのどちらか一方としてしか現れていない場合, \(x\) を含む節を取り除いても充足可能性は同値である.なぜか.
    (解答例)

    正リテラルとしてしか現れていない場合, \(x=1\) としても充足可能性は同値である. また,負リテラルとしてしか現れていない場合は \(x=0\) としても充足可能性は同値である. したがって,どちらの場合でも \(x\) を含む節を取り除くことができる.

  12. 任意のCNFは充足可能性が同値な3SATに変換できることを示せ.
    (解答例)

    長さが3以上の節 \((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 Rivestの式

3.2.1 概要

  • Rivestの連想ブロック計画に基づいた「最も短く面白い3CNF」が紹介されている.

3.2.2 注釈

  • 段落17: Rivestの連想ブロック計画は日本語訳3巻6.5節に, またRivestの式はA巻53ページに現れる. 式(6)は,変数列 \(x_1x_2x_3x_4\) に対する0000から1111の16通りあるどの値割り当てに対しても, ちょうど1つの節だけが偽になる. 例えば,0000の場合は節 \(341\) だけが偽になり,0001の場合は節 \(23\bar 4\) だけが偽になる. 他の14通りの場合も同様である.
  • 式(6)は,R. L. Rivestの連想ブロック計画 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列 2^3=8行で,各列に*が2つ,各行に*が1つ現れている.各*は0,1のどちらにもマッチすることを意味する.
    • 0000から1111の16通りのパターンは,いずれもどれか1行にマッチする.
    • 000*など,*が1つ現れるパターンは,いずれも1行か2行にマッチする.
    • *が2つ現れるパターンは,いずれも3行にマッチする.
    • *が3つ現れるパターンは,いずれも5行にマッチする.
  • ABD(4,3)の \(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\) はトートロジーとなり,その否定 \(R = \bar{F}\) は充足不能である. \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*}

3.2.3 参考資料

3.2.4 関連する原著の演習問題

  • Exercise 2  [ 20 ] 

3.2.5 練習問題

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

    以下の内容のファイル rivest-unsat.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 <rivest-unsat.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.)
    

    その他 sat0, sat0w, sat8, sat9, sat10, sat11k で実行してみると良い. どれが最もメモリーアクセス数が少ないだろうか.

  2. \(R'\) が充足可能 (SAT)であることをSATソルバーで確かめよ.
    (解答例)

    rivest-unsat.sat の最後の行を除いたファイル rivest-sat.sat を作成し, sat13で実行する.

    $ sat13 <rivest-sat.sat
    (4 variables, 7 clauses, 21 literals successfully read)
    !SAT!
     3 ~1 2 4
    Altogether 291+138 mems, 5752 bytes, 2 nodes, 0 clauses learned, 47 memcells.
    (0 restarts.)
    

    その他 sat0, sat0w, sat8, sat9, sat10, sat11k で実行してみると良い. どれが最もメモリーアクセス数が少ないだろうか.

  3. \(R\) が充足不能であることを導出 (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\) を示したことになる.
  4. \(R'\) の解はいくつあるか? \(R\) から別の節を1つ除いた場合はどうか.
    (解答例)

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

  5. \(R'\) の解の個数をSATソルバーを用いて確かめるにはどうすれば良いか.
    (解答例)

    sat13を用いて得られた \(R'\) の最初の解 3 ~1 2 4 は \(\bar{1}\land 2\land 3\land 4\) を意味する. これを否定すると節 \(1\lor\bar{2}\lor\bar{3}\lor\bar{4}\) が得られる. そこで 1 ~2 ~3 ~4rivest-sat.sat の最後の行として追加する. 再びsat13を実行すると別の解 ~3 2 ~1 4 が得られる. これを否定した 1 ~2 3 ~4 をさらに追加し,再びsat13を実行する. UNSATが出力されるから,これ以上の解はない.

  6. \(R\) 以外に,他にどんな充足不能なCNFが考えられるか.
    (解答例)

    3変数の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}\}\) は 明らかに充足不能.

    \(\{12,13,23,\bar{1}\bar{2},\bar{1}\bar{3},\bar{2}\bar{3}\}\) も充足不能である. これは \(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変数では \(R\) 以外にどんなCNFがあるだろうか?

  7. 「怠け者」,「幸福」,「不健康」,「ダンサー」をそれぞれ変数1から4で表し,原著の演習問題2に解答せよ.

4 応用例 (EXAMPLE APPLICATIONS)

4.1 単純な例 (A simple example)

4.1.1 概要

長さ8の二進列00110011を見ると,どの3つの0も等間隔に現れておらず, どの3つの1も等間隔に現れていない. 同様の性質を持つ長さ9の二進列は,存在するだろうか? SATソルバーを用いて調べる方法を学ぶ.

この問題は,集合 \({1,2,\ldots,9}\) を2つに分割し, どちらにも長さ3の等差数列が現れないようにする問題と述べることもできる.

4.1.2 注釈

  • 段落5: \(W(3,3)=9\) だから, \(\textit{waerden}(3,3;8)\) は充足可能で, \(\textit{waerden}(3,3;9)\) は充足不能である. 逆に \(\textit{waerden}(3,3;8)\) が充足可能より \(W(3,3)>8\) がわかり, \(\textit{waerden}(3,3;9)\) が充足不能より \(W(3,3)\le9\) がわかる.
  • 段落6: \([k\,\rm が偶数]\) など \([F]\) の形式の式は, \(F\) が成り立てば1で成り立たなければ0の値を取る.
  • 段落6: \(W(1,k)=k\) および \(W(2,k)=2k-[k\,\rm が偶数]\) の証明は以下の練習問題を参照.
  • 段落6: 通常,SATソルバーにとって,充足不能であることを証明するのは, 充足可能を示すより何倍も難しい. したがって,ここでは下界のみが示されている.

4.1.3 参考資料

4.1.4 関連する原著の演習問題

演習問題3–10

  • Exercise 3  [ M21 ] 
  • Exercise 4  [ 22 ] 
  • Exercise 5  [ M46 ] 
  • ► Exercise 6  [ HM37 ]  局所補題 (Local Lemma)を用いて \(W(3,k)=\Omega\bigl(k^2\!/(\log k)^3\bigr)\) を示せ.
  • Exercise 7  [ 21 ] 
  • ► Exercise 8  [ 20 ]  \(n<W(k_0,k_1,\ldots,k_{b-1})\) の時,かつその時に限り充足可能となる 節 \(\textit{waerden}(k_0,k_1,\ldots,k_{b-1};n)\) を定義せよ.
  • Exercise 9  [ 24 ] 
  • ► Exercise 10  [ 21 ]  \(m\) 個の節と \(n\) 個の変数からなる任意の充足可能性問題は, \(m+n\) 個の節と \(2n\) 個の変数からなる同等で単調 (monotonic)な問題に 変換できることを示せ. 最初の \(m\) 個の節は負のリテラルだけを持ち, 後の \(n\) 個は2つの正のリテラルからなる二項節である.

4.1.6 Scala版プログラム

4.1.7 練習問題

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

    prog/waerden-3-3-9.sat を用いて,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つ求めよ.
    (解答例)

    prog/waerden-3-3-9.sat から変数9を含む節を削除し, waerden-3-3-8.sat として保存して,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)\) を生成するプログラムを作成せよ.
    (解答例)

    Knuth版は sat-waerden である.以下のように実行する.

    $ sat-waerden 3 3 9 | sat13
    $ sat-waerden 3 3 8 | sat13
    

    Scala版のプログラムは prog/src/main/scala/waerden.scala である. 以下のように実行する.

    $ ./taocpsat waerden 3 3 9 | sat13
    $ ./taocpsat waerden 3 3 8 | sat13
    
  5. \(\textit{waerden}(4,4;34)\) の解の1つを求めよ.
    (解答例)

    以下のようにする.

    $ sat-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
    
  6. \(\textit{waerden}(5,5;178)\) はいくつの節になり,sat13で充足不能を示すのにどれぐらいの実行時間がかかるか. それより難しい問題はどうか.
    (解答例)

    以下のようにする.

    $ sat-waerden 5 5 178 | wc -l
    7745
    $ sat-waerden 5 5 178 | time sat13
    

    7745行あるが最初の行はコメントなので,7744節がある. 実行時間は2分程度かかる.それより難しい問題は,すぐには終わらない.

  7. \(\textit{waerden}(3,4;17)\) で 00 から始まる解はあるか.
    (解答例)

    まず,以下のようにして waerden-3-4-17.sat ファイルを作成する.

    $ sat-waerden 3 4 17 >waerden-3-4-17.sat
    

    このファイルの最後に ~1~2 の2行を追加し,sat13で実行する. 結果はUNSATなので,そのような解は存在しない.

  8. \(W(1,k)=k\) および \(W(2,k)=2k-[k\rm が偶数]\) を示せ.
    (解答例)

    \(W(1,k)\) の場合,0が現れることはできず, \(k-1\) 個の連続した1の列だけが条件を満たす. したがって, \(W(1,k)=k\) がわかる. \(W(2,k)\) の場合,0は2個以上現れることはできない. したがって, \(1^{k-1}01^{k-1}\) が最長の二進列の候補になる. これは, \(k\) が奇数の場合はうまくいく. 例えば, \(k=3\) の時, \(11011\) は等間隔に並ぶ3個の1を含まない. したがって, \(k\) が奇数の場合, \(W(2,k)=2k\) である. しかし \(k\) が偶数,例えば4の時, \(1110111\) には1つ置きに並ぶ4個の1があり,条件に違反する. したがって,1を1つ減らした \(1^{k-1}01^{k-2}\) が最長になる. つまり, \(k\) が偶数の場合, \(W(2,k)=2k-1\) である.

  9. (★) 同様の問題にラムゼー数がある(Wikipedia:ラムゼーの定理). 一例は「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」として知られている. すなわち,6頂点の完全グラフの辺を2色(たとえば赤と青)で塗り分けた時, どのように塗り分けても同色の辺からなる3角形が生じる. そのような3角形が現れない条件をCNFで記述し, それが充足不能であることを示せ. また,一般にはどのようにできるか.
    (解答例)

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

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

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

  10. Two-hundred-terabyte maths proof is largest ever を読め.
    (解答例)

    \(a^2+b^2=c^2\) を満たす正の整数 \((a,b,c)\) をピタゴラスの3つ組 (Pythagorean triple)という. Marijn Heule, Oliver Kullmann, Victor Marekは, 集合 \(\{1,2,\ldots,n\}\) を2つの集合に分割し, どちらにもピタゴラスの3つ組が現れないようにできるかという問題について, \(n\le 7824\) の場合には可能で, \(n\ge 7825\) の場合には不可能であることをSATソルバーを用いて示した. SATソルバーによる後者の証明が200テラバイトにもなったということから, 紹介記事がNatureに掲載された. また,以下も最近発表された.

    • Marijn J. H. Heule, Oliver Kullmann: The Science of Brute Force, Communications of the ACM, August 2017, Vol. 60 No. 8, pages 70-79.
  11. Erdösのdiscrepancy問題について調べよ.
    (解答例)

    https://en.wikipedia.org/wiki/Sign_sequence などを参照. Knuth版のプログラムおよび knuth/sat-examples/README も参照.

  12. 式(1)の \(F\) を単調な問題にするとどうなるか.
    (解答例)

    演習問題10の方法を用いれば, \(\{\bar1'\bar2, \bar2'\bar3', \bar1\bar3, \bar1\bar2\bar3', 11', 22', 33'\}\) が得られる.

4.2 厳密被覆 (Exact covering)

4.2.1 概要

数列312132には,1から3の数が2つずつ現れており, 各数 \(i\) の間はちょうど \(i\) 個だけ離れている. 一般に,このような数列 (Langford対と呼ばれる)を求める問題は,厳密被覆問題として定式化できる. 厳密被覆問題をSATソルバーを用いて解く方法を学ぶ.

4.2.2 注釈

  • 段落1: Langford対の問題は,4A巻7章の最初でも取り上げられている. Langford対問題は \(n=4m-1\) か \(n=4m\) の時だけ解を持つ. 本書でも「制約の節への符号化」で,SAT解法アルゴリズムの性能比較に利用されている.
  • 段落1: ダンシング・リンク (dancing links)は,厳密被覆問題を効率良く解くために考えられた データ構造およびアルゴリズムである. 7.2.2.1小項で説明されるが,現時点で未出版である (2018年出版予定).
    • 厳密被覆問題は,与えられた集合 \(X\) と集合族 \(S \subset 2^X\) について, \(X\) の分割である \(S^* \subset S\) を選び出す問題である. \(S^*\) を厳密被覆と呼ぶ.以下,Wikipediaの例を示す.
    • たとえば \(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\) の厳密被覆である.
    • この問題は,以下の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
  • 段落1:
    • Langford対の問題は,\(1,1,2,2,\ldots,n,n\) の \(2n\) の数を並び替えて, 各数 \(k\) について2つの \(k\) 間の距離が \(k\) になっている列を探す問題である. 詳しくは4A巻の最初に述べられている.
    • \(n=3\) の時,列 231213 は条件を満たしている (2つある1の間の距離は1,2の距離は2,3の距離は3になっている). 41312432 は \(n=4\) の時, 46171435623725 は \(n=7\) の時の解の例である.
    • Langford対の問題は \(n=4m-1\) か \(n=4m\) の時だけ解を持つ. \(n=3,4\) の時の解は1つ(左右対称解を除く), \(n=7\) の時の解は26ある.
  • 段落1: Langford対の問題は厳密被覆問題として定式化できる. 例えば,オプション `\(d_1 s_1 s_3\)' は, 数字1を1と3の位置に配置する選択を意味する. このオプションを選択した時,数字1に対する他のオプション, すなわち \(d_1\) を含む他のオプション `\(d_1 s_2 s_4\)' などは選択できなくなる. また,1と3の位置を利用する他のオプション, すなわち \(s_1\) あるいは \(s_3\) を含む他のオプション `\(d_2 s_1 s_4\)', `\(d_2 s_3 s_6\)' なども選択できなくなる.
    • \(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\) を表している.
  • 段落2: \(S_1\) などの対称的Boole関数については,日本語訳4A巻71ページに説明がある. なお,後述のように \([y_1+\cdots+y_p=k]\), \([y_1+\cdots+y_p\ge k]\), \([y_1+\cdots+y_p\le k]\) などは 基数制約と呼ばれる.これらも対称的Boole関数である.
  • 段落3: 式(17)右辺の \((y_1\lor\cdots\lor y_p)\) は \(y_1+\cdots+y_p\ge 1\) (at-least-one)を表し, \(\bigwedge_{1\le j<k\le p}(\bar y_j\lor\bar y_k)\) は \(y_1+\cdots+y_p\le 1\) (at-most-one)を表している.
  • 段落3: 節 \(\bar1\bar3\) は \(S_1(x_1,x_2,x_3,x_4)\) と \(S_1(x_1,x_3,x_7)\) があるから重複し, 節 \(\bar2\bar4\) は \(S_1(x_1,x_2,x_3,x_4)\) と \(S_1(x_2,x_4,x_5)\) があるから重複している. \(S_1(x_1,x_2,x_3,x_4)\) は項目 \(d_1\) に, \(S_1(x_1,x_3,x_7)\) は項目 \(s_3\) に, \(S_1(x_2,x_4,x_5)\) は項目 \(s_4\) に対応している. つまり, オプション1の `\(d_1 s_1 s_3\)' と3の `\(d_1 s_3 s_5\)' で項目 \(d_1\) と \(s_3\) が共通し, オプション2の `\(d_1 s_2 s_4\)' と4の `\(d_1 s_4 s_6\)' で項目 \(d_1\) と \(s_4\) が共通している.

4.2.4 関連する原著の演習問題

演習問題11-13

  • Exercise 11  [ 27 ] 
  • Exercise 12  [ 21 ] 
  • Exercise 13  [ 24 ] 

4.2.7 練習問題

  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)\) を生成するプログラムを作成せよ.
    (解答例)

    Knuth版は langford が厳密被覆問題を出力し,それを sat-dance でCNFに変換する. 以下のように実行する.

    $ langford 3 | sat-dance | sat13
    

    Scala版のプログラムは prog/src/main/scala/langford.scala, prog/src/main/scala/sat_dance.scala である. 以下のように実行する.

    $ ./taocpsat langford 3 | ./taocpsat sat_dance | sat13
    
  5. \(S_1(y_1,...,y_5)\) で新しい変数 \(t\) を用いたCNFから, \(t\) を用いていない元のCNFを導出 (resolution)で導き出せ.
  6. \(\textit{langford}'(n)\) を生成するプログラムを作成せよ.
    (解答例)

    Knuth版は langford が厳密被覆問題を出力し,それを sat-dance-heule でCNFに変換する. 以下のように実行する.

    $ langford 3 | sat-dance-heule | sat13
    

    Scala版のプログラムは prog/src/main/scala/langford.scala, prog/src/main/scala/sat_dance_heule.scala である. 以下のように実行する.

    $ ./taocpsat langford 3 | ./taocpsat sat_dance_heule | sat13
    
  7. 原著の演習問題13を参照し, \(\textit{langford}(n)\) を生成するプログラムを 無駄な節が生成されないように修正せよ.
  8. (★) \(y_1 + \cdots + y_p = 1\) (exact-one), \(y_1 + \cdots + y_p \ge 1\) (at-least-one), \(y_1 + \cdots + y_p \le 1\) (at-most-one)の条件を用いると, 多くの問題を表現できる. 例えば エイト・クイーン の問題はどのように表現できるだろうか. また,一般のNクイーンだとどうなるか.
    (解答例)

    Boole変数 \(x_{ij}\) で \(i\) 行 \(j\) 列にクイーンを配置することを表すとすると, 各行および各列について \(x_{ij}\) の和が1に等しく, 各対角線について \(x_{ij}\) の和が1以下という条件を定めれば良い.

4.3 グラフ彩色 (Coloring a graph)

4.3.1 概要

図33の地図を,隣接する領域が異なる色になるように4色で塗り分けることはできるだろうか. SATソルバーを用いて解を探す方法を学ぶ.

4.3.2 注釈

  • 段落1: グラフ彩色には,無線の周波数割当てやコンパイラでのレジスタ割当てなどの応用がある. 時間割問題やパズルの数独なども関連する. 日本語訳4A巻7章の最初で説明されている. 本書でも「制約の節への符号化」で,SAT符号化の性能比較に利用されている.
  • 段落1: \(u\)—\(v\) は,頂点 \(u\) と \(v\) が辺で結ばれていることを表す記法である.
  • 段落1: 式(15)は \(v_1+v_2+\cdots+v_d\ge1\) という制約(at-least-one制約と呼ぶ)を表しており, (17)のある頂点に対する \(d\choose2\) 個の節は \(v_1+v_2+\cdots+v_d\le1\) という制約(at-most-one制約と呼ぶ)を表している. 頂点 \(v\) が1から \(d\) のいずれかの値を持つ整数変数と考えた場合, この符号化方法は直接符号化 (direct encoding)と呼ばれており, 式(15)だけを用いる方法は多値符号化 (multivalued encoding)と呼ばれている. 整数変数のその他の符号化方法については,この後の 「制約の節への符号化」で詳しく説明されている.
  • 段落1: \(v_1=v_2=1\) となる解が得られたとすれば,頂点 \(v\) を色1で塗っても 色2で塗ってもどちらも解になる.
  • 段落3: 四色定理は平面グラフに対してのものであって, 一般のグラフが常に4色以下で塗り分けられるわけではない. 例えば, \(n\) 次の完全グラフ \(K_n\) を塗り分けるには \(n\) 色が必要になる.
  • 段落4: Randal Bryantは,日本語訳4A巻7.1.4項で詳しく取り上げられているBDD (二分決定図)で著名な研究者である. Bryantの彩色方法については http://www.cs.cmu.edu/~bryant/boolean/macgregor.html を参照.
  • 段落5: 異なる8個の領域(頂点)を \(a\), \(b\), \(c\), \(d\), \(e\), \(f\), \(g\), \(h\) とすると, それらのすべてが1の色で彩色されているのではないことを表す節は \(\bar a_1\lor\bar b_1\lor\cdots\lor\bar h_1\) となる. \(a\), …, \(h\) を選ぶ組合せは, \(110\choose 8\) 通りがあり得る. しかし,例えば \(a\) と \(b\) が隣接している場合,両方が同じ色になることはないから, \(a_1\) あるいは \(b_1\) の少なくとも一方は偽になり,上記の節は不要になる. したがって,独立した8個の頂点だけを選ぶので良い. なお,グラフにおける独立した頂点集合とは,互いに隣接していない(辺で結ばれていない) 頂点の集合のことであり,4A巻7章の始めに説明がある.
  • 段落6: Sinzによるこの方法はSequential Counterと呼ばれている. ここでの補助変数 \(s_j^k\) の使い方は,オリジナルとは異なっている. \(1\le m\le n\), \(1\le l\le \min(m-1,r)\) に対し, \(x_1+\cdots+x_m\ge l\) となるように \(s_m^l\) を導入できる(要確認).
  • 段落7: BailleuxとBoufkhadによるこの方法はTotalizerと呼ばれている.
  • 段落8: 基数制約,あるいはブール基数制約 (Boolean cardinality constraints)をSATの節に符号化する方法は, 上記のSinzのSequential Counter, BailleuxとBoufkhadのTotalizer以外にも多数が提案されているが, 実用上は,この2種類が良いことが多い.

4.3.4 関連する原著の演習問題

演習問題14–39

  • ► Exercise 18  [ 28 ]  演習問題17で見つけた彩色方法を調べ, 任意の次数 \(n\) のMcGregorグラフを4-彩色する明確な方法で, 色のうちの1つが高々 \({5\over6}n\) 回だけ利用される方法を定義せよ. ヒント: 構成方法は \(n\mod6\) の値に依存する.
  • ► Exercise 19  [ 29 ]  演習問題17に続けて,2色を同時に取り得る領域の最大個数を \(h(n)\) と置く (節(17)を利用しない). \(h(n)\) を調べよ.
  • ► Exercise 24  [ M32 ]  省略.
  • ► Exercise 28  [ 20 ]  \(x_1+\cdots+x_n\ge1\) を保証したい場合,(18)と(19)からどんな節が得られるか? (この特別の場合は,任意の節を3SAT節に変換する.)
  • ► Exercise 29  [ 20 ]  単一の制約 \(x_1+\cdots+x_n\le r\) の代わりに, \(1\le i\le n\) に対する制約の列 \(x_1+\cdots+x_i\le r_i\) を課したいと仮定する. 追加の節や補助変数を用いて,これをうまく実現できるか?
  • ► Exercise 30  [ 22 ]  式(18)と(19)で \(x_1+\cdots+x_n\le r\) とするために 補助変数 \(s_j^k\) が用いられ, 他方, \(\bar x_1+\cdots+\bar x_n\le n-r\) とするために \(s^{\prime k}_j\) が用いられている場合, \(1\le j\le n-r\), \(1\le k\le r\) に対して \(s^{\prime j}_k=\smash{\overline{s_j^k}}\) とすることで, これらを統合できることを示せ. 式(20)と(21)は同様に統合できるか?
  • ► Exercise 31  [ 28 ]  \(x_1+\cdots+x_n=r\) で \(t\) 個の等間隔に並ぶ1が含まれていないビットベクトル \(x_1\ldots x_n\) が存在する最小の \(n\) を \(F_t(r)\) と置く. 例えば, 唯一の解101100011010000000010110001101があるから, \(F_3(12)=30\) である. SATソルバーの助けを借りて, どのように \(F_t(n)\) を効率良く計算したら良いかを述べよ.
  • ► Exercise 36  [ 22 ]  \(L(2,1)\) ラベリングとしても知られている, グラフの無線彩色 (radio coloring)とは, 頂点への整数の色の割り当てで, \(u\)—\(v\) なら \(u\) と \(v\) の色が2以上異なり, \(u\) と \(v\) が共通の近傍を持てば1以上異なっているものである. (この考えは,1988年にFred Robertsによって導入された. 無線伝送器で,「近い」伝送器からの干渉を避け,また 「非常に近い」伝送器からの強い干渉を避けるようにチャンネル割り当て をする問題が動機となっている.) 図33で,連続した色を16個だけ使用する無線彩色を求めよ.

4.3.6 Scala版プログラム

以下のようにすると,McGregorグラフをDIMACS Graphフォーマットで出力できる.

$ ./taocpsat mcgregor graph 10
c McGregor graph of order 10
p edge 110 324
v 0.0
v 0.1
v 0.2
v 0.3
.....
e 0.0 1.0
e 0.0 10.1
e 0.0 10.2
e 0.0 10.3
e 0.0 10.4
.....

"v" で始まる行は頂点を表し,"e" で始まる行は辺を表している.

4.3.7 練習問題

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

    prog/mcgregor3-4.sat を用いる. 変数 \(i.j.c\) は,領域 \(i.j\) を色 \(c\) で塗ることを表している. 以下のように4彩色可能である.

    $ sat13 <mcgregor3-4.sat
    (48 variables, 132 clauses, 288 literals successfully read)
    !SAT!
     ~0.0.4 ~3.2.1 ~0.0.3 ~0.0.2 0.0.1 ~1.0.1 ~3.1.1 ~1.1.1 ~0.1.1 ~3.0.1 ~0.1.3 ~0.1.2 0.1.4 ~1.2.4 ~3.2.4 ~1.1.4 ~0.2.4 ~2.0.3 ~1.2.3 ~3.2.3 3.2.2 ~3.1.2 ~2.1.2 ~1.2.2 ~1.0.2 ~0.2.2 1.2.1 ~2.2.1 ~2.1.1 ~0.2.1 0.2.3 ~3.1.4 3.1.3 ~3.0.3 ~2.1.3 ~1.0.3 2.1.4 ~2.2.4 ~2.0.4 1.0.4 ~2.0.2 2.0.1 ~2.2.2 2.2.3 ~1.1.3 1.1.2 ~3.0.2 3.0.4
    Altogether 3201+10458 mems, 12988 bytes, 37 nodes, 6 clauses learned (ave 7.3->7.3), 329 memcells.
    (3 restarts.)
    

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

    $ sat13 <mcgregor3-4.sat | tr " " "\n" | grep -v '^~' | sort -n
    .....
    0.0.1
    0.1.4
    0.2.3
    1.0.4
    1.1.2
    1.2.1
    2.0.1
    2.1.4
    2.2.3
    3.0.4
    3.1.3
    3.2.2
    
  2. 任意の次数のMcGregorグラフを生成するプログラムを作成し,図33のMcGregorグラフが4彩色可能かどうかをSATソルバーで判定せよ. Knuthの mcgregor-graph プログラムを参考にせよ.
    (解答例)

    Knuth版は mcgregor-graph がグラフのファイル mcgregor10.gb を生成し, sat-color がその彩色問題をCNFに変換する. 以下のように実行する.

    $ mcgregor-graph 10
    $ sat-color mcgregor10.gb 4 | sat13
    

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

    $ sat-color mcgregor10.gb 4 | sat13 | tr " " "\n" | grep -v '^~' | sort -n
    

    3彩色はできない.

    $ sat-color mcgregor10.gb 3 | sat13
    

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

    $ ./taocpsat mcgregor color 10 4 | sat13
    

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

    $ ./taocpsat mcgregor 10 4 | sat13 | tr " " "\n" | grep -v '^~' | sort -n
    
  3. (★) 以下のサイトなどにあるDIMACS Graphフォーマットで記述されたグラフが,指定された色数で彩色可能かどうか調べるプログラムを作れ.

    たとえば queeen5_5.col は,5x5のクイーングラフで,5色で彩色可能である.

  4. (★) 数独はグラフ彩色問題の一種である.数独の問題をSAT問題に符号化するプログラムを作成せよ.
    (解答例)

    SATとパズル を参照.そこで示されている方法を用いれば25x25など大きなサイズの問題も非常に簡単に解ける.

  5. クイーン・グラフ彩色問題について調べよ.
    (解答例)

    SATソルバーの使い方 を参照. Knuth版のプログラムおよび knuth/sat-examples/README も参照.

  6. Sinzの方法を用いて,McGregorグラフで色1が7回以下の彩色を求めよ.
    (解答例)

    Knuth版のプログラムの場合,以下のようにして実行する.

    $ mcgregor-graph 10
    $ sat-color mcgregor10.gb 4 > /tmp/mcg10.sat
    $ sat-threshold-sinz-graphs 110 7 mcgregor10.gb 4 > /tmp/mcg10le7.sat
    $ cat /tmp/mcg10.sat /tmp/mcg10le7.sat | sat13
    (1161 variables, 2944 clauses, 6726 literals successfully read)
    !SAT!
     S33.1 S34.1 S35.1 S36.1 S37.1 .....
    Altogether 70563+166289897 mems, 662097 bytes, 21080 nodes, 15484 clauses learned (ave 28.1->18.3), 125859 memcells.
    (4946 learned clauses were trivial.)
    (82 learned clauses were discarded.)
    (71 clauses were subsumed on-the-fly.)
    (1 restart.)
    

    Scala版の場合,以下のように実行すれば,どの領域が色1で彩色されたかは以下でわかる.

    $ ./taocpsat mcgregor color_sinz 10 4 7 | sat13 | tr ' ' '\n' | grep -v '~' | egrep '\.1$'
    (1161 variables, 2944 clauses, 6726 literals successfully read)
    !SAT!
    Altogether 70563+51468352 mems, 423865 bytes, 9736 nodes, 6494 clauses learned (ave 24.8->16.0), 66301 memcells.
    (1791 learned clauses were trivial.)
    (36 learned clauses were discarded.)
    (42 clauses were subsumed on-the-fly.)
    (1 restart.)
    7.3.1
    10.9.1
    5.2.1
    9.4.1
    3.1.1
    10.2.1
    10.6.1
    
  7. BailleuxとBoufkhadの方法を用いて,McGregorグラフで色1が7回以下の彩色を求めよ.
    (解答例)

    Knuth版のプログラムの場合,以下のようにして実行する.

    $ mcgregor-graph 10
    $ sat-color mcgregor10.gb 4 > /tmp/mcg10.sat
    $ sat-threshold-bb-graphs 110 7 mcgregor10.gb 4 > /tmp/mcg10le7.sat
    $ cat /tmp/mcg10.sat /tmp/mcg10le7.sat | sat13
    (839 variables, 2622 clauses, 6082 literals successfully read)
    !SAT!
     ~5.5.1 ~7.0.3 ~7.0.4 ~5.5.4 ~4.4.4 .....
    Altogether 56901+20012951 mems, 304759 bytes, 4404 nodes, 3205 clauses learned (ave 24.0->16.9), 46587 memcells.
    (831 learned clauses were trivial.)
    (23 learned clauses were discarded.)
    (14 clauses were subsumed on-the-fly.)
    (2 restarts.)
    

    Scala版の場合,以下のように実行すれば,どの領域が色1で彩色されたかは以下でわかる.

    $ ./taocpsat mcgregor color_bb 10 4 7 | sat13 | tr ' ' '\n' | grep -v '~' | egrep '\.1$'
    (839 variables, 2622 clauses, 6082 literals successfully read)
    !SAT!
    Altogether 56901+54398437 mems, 421279 bytes, 12166 nodes, 7804 clauses learned (ave 22.5->16.3), 75717 memcells.
    (1722 learned clauses were trivial.)
    (139 learned clauses were discarded.)
    (81 clauses were subsumed on-the-fly.)
    (6 restarts.)
    5.2.1
    7.3.1
    3.1.1
    10.9.1
    9.4.1
    10.2.1
    10.6.1
    
  8. (★) 原著の演習問題19に取り組め.
  9. (★) 原著の演習問題21に取り組め.
  10. (★) 原著の演習問題31に取り組め.
    (解答例)

    https://oeis.org/A065825 参照.

  11. (★) 原著の演習問題36に取り組め.
  12. 原著の演習問題17の解答で \(f(16)=12\) と示されている. \(f(17)\) の値はいくつか?
    (解答例)

    Scala版のプログラムの場合,以下のようにして調べることができる.

    $ ./taocpsat mcgregor color_bb 17 4 13 | sat13 h9 >/dev/null
    $ ./taocpsat mcgregor color_bb 17 4 12 | sat13 h9 >/dev/null
    

4.4 整数の因数分解 (Factoring integers)

4.4.1 概要

与えられた自然数 \(z\) を,2つの自然数の積 \(x\cdot y\) に因数分解したい. SATソルバーを用いれば,\(z = x\cdot y\) の条件を記述するだけで,解を求めることができる.

4.4.2 注釈

  • 段落1: ここでは,5ビットの値を2ビットと3ビットの積に分解しているのであって, 素因数分解を行っているわけでない点に注意する. \(z=7=(00111)_2\) は \(x=1=(01)_2\) と \(y=7=(111)_2\) の積に分解できる. \(z=22=(10110)_2\) は, \(2\times 11\) に等しいが,2ビットと3ビットの積には 分解できないから充足不能になる. 演習問題40も参照.
  • 段落2: Boole連鎖の説明は日本語訳4A巻7.1.2項に, 7.1.2–(23)と(24)は日本語訳4A巻102ページにある. \(x\xor y\) は, \(x\) と \(y\) の排他的論理和 (XOR)を表す. \(t\gets u\land v\) についての節は, \(t\Leftrightarrow(u\land v)\) ,すなわち \((t\Rightarrow(u\land v))\land((u\land v)\Rightarrow t)\) を展開することで得られる. なお, \(A\Rightarrow B\) は \(\bar A\lor B\) に等しい.
  • 段落3: TseytinはTseitinと綴られることが多い.
  • 段落4: \(\langle x y z\rangle\) は,7.1.1項で導入されている中央値演算である. \(x\), \(y\), \(z\) の多数決の値を表す. 上記の方法で,積 \(x_i\land y_j\) を \(\textit{bin}[i+j]\) ではなく, \(\textit{bin}[i+j-1]\) に入れるように変更したほうがわかりやすい. この場合,積の \(i\) ビット目が \(\textit{bin}[i]\) に保存される.

4.4.4 関連する原著の演習問題

演習問題40–46

  • ► Exercise 43  [ 21 ]  整数 \(n\ge2\) について, 奇数の回文 (palindromic)二進数 \(x=(x_n\ldots x_1)_2=(x_1\ldots x_n)_2\) と \(y=(y_n\ldots y_1)_2=(y_1\ldots y_n)_2\) で, それらの積 \(xy=(z_{m+n}\ldots z_1)_2=(z_1\ldots z_{m+n})_2\) も 回文になるものが存在するか?
  • ► Exercise 44  [ 30 ]  \(\nu x+\nu y+\nu(xy)\) の可能な最大値, すなわち32ビットの二進数 \(x\) と \(y\) の乗算すべてのうちで ビット1の現れる個数の合計の最大値を見つけよ. 《訳注: \(\nu x\) は \(x\) の二進表現中に現れるビット1の個数を表し, 横方向の和 (sideways sum)という.2巻4.6.3項で説明されている.》

4.4.6 Scala版プログラム

4.4.7 練習問題

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

    式(23)のBoole連鎖の最後に \(z=21=(10101)_2\) に相当する連鎖を追加した prog/prod-2-3-21-bchain.txt を利用し,以下のようにして実行する.

    $ ./taocpsat bchain encode <prod-2-3-21-bchain.txt | sat13
    (20 variables, 54 clauses, 130 literals successfully read)
    !SAT!
     Z5 ~Z4 Z3 ~Z2 Z1 C2 B3 Y3 X2 Y1 X1 A3 B1 A2 Y2 C1 B2 ~S ~Q P
    Altogether 1262+470 mems, 8456 bytes, 0 nodes, 0 clauses learned, 211 memcells.
    (0 restarts.)
    

    X2=X1=1, Y3=Y2=Y1=1 だから \(x=3\), \(y=7\) である.

    Knuth版のプログラムの場合,以下のようにして実行する.

    $ sat-dadda 2 3 21 | sat13
    (20 variables, 54 clauses, 130 literals successfully read)
    !SAT!
     Z5 ~Z4 Z3 ~Z2 Z1 A5.2 A5.1 Y3 X2 Y1 X1 A3.2 A4.1 A3.1 Y2 A4.3 A4.2 ~S4.1 ~Q4.1 P4.1
    Altogether 1262+583 mems, 8456 bytes, 0 nodes, 0 clauses learned, 211 memcells.
    (0 restarts.)
    
  2. 上で \(z=19\) の時にUNSATとなることを確認せよ.
    (解答例)

    式(23)のBoole連鎖の最後に \(z=19=(10011)_2\) に相当する連鎖を追加した prog/prod-2-3-19-bchain.txt を利用し,以下のようにして実行する.

    $ ./taocpsat bchain encode <prod-2-3-19-bchain.txt | sat13
    (20 variables, 54 clauses, 130 literals successfully read)
    ~
    UNSAT
    Altogether 1262+395 mems, 8456 bytes, 0 nodes, 0 clauses learned, 211 memcells.
    (0 restarts.)
    

    Knuth版のプログラムの場合,以下のようにして実行する.

    $ sat-dadda 2 3 19 | sat13
    (20 variables, 54 clauses, 130 literals successfully read)
    ~
    UNSAT
    Altogether 1262+468 mems, 8456 bytes, 0 nodes, 0 clauses learned, 211 memcells.
    (0 restarts.)
    
  3. \(x=(x_2x_1)_2\) , \(z=(z_4z_3z_2z_1)_2\) の時, \(z=x^2\) に対するBoole連鎖を記述せよ.
    (解答例)

    Scala版のプログラム prog/src/main/scala/dadda.scala を用いて, YX に置き換えれば良いが, 冗長な連鎖になる.

    $ ./taocpsat dadda factor_fifo 2 2 . | sed -e "s/Y/X/"
    Z1 = X1 and X1
    _1 = X1 and X2
    _2 = X2 and X1
    Z2 = _1 xor _2
    _3 = X2 and X2
    _4 = _1 and _2
    Z3 = _3 xor _4
    Z4 = _3 and _4
    

    これを簡単にすると prog/sq-2-4-bchain.txt のように書ける.

  4. \(\textit{factor_fifo}(m,n,z)\) を作成せよ.
    (解答例)

    Knuth版のプログラムは sat-dadda である.

    Scala版のプログラム prog/src/main/scala/dadda.scala を示す. 以下のようにして実行する.

    $ ./taocpsat dadda factor_fifo 2 3 10101 | ./taocpsat bchain encode | sat13
    (20 variables, 54 clauses, 130 literals successfully read)
    !SAT!
    Z5 ~Z4 Z3 ~Z2 Z1 _10 _9 Y3 X2 Y1 X1 _3 _2 _1 Y2 _5 _4 ~_6 ~_8 _7
    Altogether 1262+470 mems, 8456 bytes, 0 nodes, 0 clauses learned, 211 memcells.
    (0 restarts.)
    

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

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

    Knuth版のプログラムの場合,以下のようにして実行する.

    $ sat-dadda 15 15 1071514531 | sat13
    (1260 variables, 4125 clauses, 10665 literals successfully read)
    !SAT!
    .....
    Altogether 81994+3347124 mems, 237980 bytes, 641 nodes, 276 clauses learned (ave 14.9->8.1), 18066 memcells.
    (66 learned clauses were trivial.)
    (7 learned clauses were discarded.)
    (1 clause was subsumed on-the-fly.)
    (6 restarts.)
    

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

    $ sat-dadda 15 15 1071514531 | sat13 >/tmp/out
    $ tr ' ' '\n' </tmp/out | grep X
    $ tr ' ' '\n' </tmp/out | grep Y
    

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

    $ sat-dadda 15 15 1071514531 | sat13 | ./taocpsat decode log X Y Z
    (1260 variables, 4125 clauses, 10665 literals successfully read)
    !SAT!
    Altogether 81994+3347124 mems, 237980 bytes, 641 nodes, 276 clauses learned (ave 14.9->8.1), 18066 memcells.
    (66 learned clauses were trivial.)
    (7 learned clauses were discarded.)
    (1 clause was subsumed on-the-fly.)
    (6 restarts.)
    X(15..1) = 111111111101101_2 = 32749
    Y(15..1) = 111111111001111_2 = 32719
    Z(30..1) = 111111110111100000001110100011_2 = 1071514531
    

    Scala版のプログラムの場合,以下のようにして実行する.

    $ ./taocpsat dadda factor_fifo 15 15 111111110111100000001110100011 | ./taocpsat bchain encode | sat13 | ./taocpsat decode log X Y Z
    (1260 variables, 4125 clauses, 10665 literals successfully read)
    !SAT!
    Altogether 81994+1471931 mems, 237616 bytes, 409 nodes, 119 clauses learned (ave 14.8->7.8), 17975 memcells.
    (31 learned clauses were trivial.)
    (2 restarts.)
    X(15..1) = 111111111101101_2 = 32749
    Y(15..1) = 111111111001111_2 = 32719
    Z(30..1) = 111111110111100000001110100011_2 = 1071514531
    
  6. (★) 原著の演習問題43に取り組め.
    (解答例)

    Scala版のプログラムで以下のようにして実行すれば \(n=2\) で \(z\) が4ビットの場合の解を探せる.

    $ ./taocpsat dadda ex43 2 4 | ./taocpsat bchain encode | sat13 | ./taocpsat decode log X Y Z
    

    Bashスクリプト prog/ex43.sh を実行すると, \(n=8\) の時の解 \(x=195\), \(y=231\), \(z=45045\) などがあることがわかる.

  7. (★) 原著の演習問題44に取り組め.
  8. 上のプログラムを使って \(z=x^2\) を表すにはどうすれば良いか (原著の演習問題45)?
    (解答例)

    すべての \(x_i \land x_j\) を \(bin[i+j]\) に入れた後, Dadda のアルゴリズムを実行すれば良い. ただしScala版のプログラムを用いる場合は, \(bin[i+j]\) ではなく \(bin[i+j-1]\) に入れる.

  9. 平方数で2進表現が回文になっているものを探せ (原著の演習問題46). 小さいものから 0, 1, 9 がある. それより大きいものはあるか.
    (解答例)

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

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

    Scala版のプログラムの場合,以下のようにして実行すれば,解がわかる.

    $ ./taocpsat dadda square_palindrome 13 25 | ./taocpsat bchain encode | sat13 | ./taocpsat decode log X Z
    (923 variables, 3055 clauses, 7902 literals successfully read)
    !SAT!
    Altogether 60813+1416656 mems, 176307 bytes, 277 nodes, 179 clauses learned (ave 17.8->6.3), 13287 memcells.
    (49 learned clauses were trivial.)
    (8 learned clauses were discarded.)
    (3 clauses were subsumed on-the-fly.)
    (2 restarts.)
    X(13..1) = 1000110101011_2 = 4523
    Z(26..1) = 01001110000010100000111001_2 = 20457529
    

    すなわち \(x = 1000110101011_2 = 4523\) の時 \(x^2 = 20457529\) の2進表現は回文になっている.

    平方数が59ビットなら,比較的すぐに実行できる.

    $ ./taocpsat dadda square_palindrome 30 59 | ./taocpsat bchain encode | sat13 h14 b1000 T50000000000 | ./taocpsat decode log X Z
    (5190 variables, 17250 clauses, 44758 literals successfully read)
    !SAT!
    Altogether 341671+3806024856 mems, 2206350 bytes, 133263 nodes, 104133 clauses learned (ave 69.0->15.1), 384530 memcells.
    (77228 learned clauses were trivial.)
    (246 learned clauses were discarded.)
    (440 clauses were subsumed on-the-fly.)
    (2 restarts.)
    X(30..1) = 100000010111001110011001011111_2 = 542959199
    Z(60..1) = 010000010111010110110100111000100011100101101101011101000001_2 = 294804691778721601
    

    SATソルバーで何ビットぐらいまで求められるだろうか? なお,普通にScalaのプログラムで探すなら以下のようにできるが, \(x\) を30ビット以下としてもすぐには終わらない.

    scala> def p(x: BigInt) = { val s = x.toString(2); s == s.reverse }
    scala> for (x <- BigInt(0) to BigInt(2).pow(30); if p(x*x)) println(x)
    0
    1
    3
    4523
    11991
    18197
    141683
    1092489
    3168099
    6435309
    12489657
    17906499
    68301841
    .....
    
  10. (★) 奇数 \(x=2m+1\) の2乗は \(x^2=(2m+1)^2=4m(m+1)+1\) だから8で割った余りが1になる. すなわち \(z=x^2\) の最後の3ビットは001に等しい. この事実を利用すると,上のプログラムを高速化できるだろうか?
    (解答例)

    prog/src/main/scala/dadda.scalasquare_palindrome の最後に以下を追加する.

    println(v("Z",1) + " = 1")
    println(v("Z",2) + " = 0")
    println(v("Z",3) + " = 0")
    

    以下のようにコンパイルして再実行する.

    $ cd ~/Desktop/taocp-sat/prog
    $ scalac -d target/taocpsat-1.0.jar src/main/scala/*.scala
    $ ./taocpsat dadda square_palindrome 30 59 | ./taocpsat bchain encode | sat13 h14 b1000 T50000000000 | ./taocpsat decode log X Z
    (5190 variables, 17253 clauses, 44761 literals successfully read)
    !SAT!
    Altogether 341683+908634434 mems, 1608098 bytes, 39793 nodes, 29171 clauses learned (ave 61.7->16.5), 234967 memcells.
    (18650 learned clauses were trivial.)
    (136 learned clauses were discarded.)
    (271 clauses were subsumed on-the-fly.)
    (2 restarts.)
    X(30..1) = 100000010111001110011001011111_2 = 542959199
    Z(60..1) = 010000010111010110110100111000100011100101101101011101000001_2 = 294804691778721601
    

    以前の3806024856 memsと比較すると908634434 memsで,4倍以上高速になっている. さらに \(x\) を4で割った余りで分類すると,どのように高速化できるだろうか.

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

    すべての \(x_i \land x_j\) を \(bin[i+j]\) に入れ, すべての \(y_i \land y_j\) を \(bin[i+j]\) に入れた後, Dadda のアルゴリズムを実行すれば良い. ただしScala版のプログラムを用いる場合は, \(bin[i+j]\) ではなく \(bin[i+j-1]\) に入れる.

  12. (★) \(n\) 番目の三角数 \(t_n=n(n+1)/2\) で, \(n\) と \(t_n\) の2進表現が両方とも回文になっているものはあるか?

4.5 故障試験 (Fault testing)

4.5.1 概要

図34のような回路では,特定の結線が0か1に固定されてしまう故障が起こりえる (縮退故障). このような故障を検出するには,テストの入力を与え,正しい出力が得られているかどうかを調べれば良い. しかし,すべての入力パターン (図34の場合は \(2^5\) 通り)は普通は膨大で,実際にはテストできない. そこで,縮退故障が高々1箇所だけだと仮定する (単一縮退故障). 例えば,表1のテストなら,100通りありえる単一縮退故障のうち,44通りを検出できる. 最小で何通りのテストを行えば,すべての単一縮退故障を検出できるか. SATソルバーを用いてその答えを探す.

4.5.2 注釈

  • 段落3: 表1の入力は \(y_3y_2y_1x_2x_1=11011_2\) で, デフォールトの値は \(z_5z_4z_3z_2z_1=10010_2\) である. \(b_2^1\) が0縮退した場合の出力は10110であり,デフォールトと一致しない.
  • 段落10: \(F\) や \(F'\) は1つの節ではなく複数の節であるので,``clauses''を「節集合」と訳している.
  • 段落10: 厳密には,式(23)のBoole連鎖ではなく,表1の左にある長さ50のBoole連鎖を用いるべきだろう (Knuth版プログラムgates-stuck参照). この場合, \(F\) の節の個数は119になる.
  • 段落10: \(z_i\ne z_i'\) は \(z_i\xor z_i'\) と等しいから,式(24)のTseytin変換を用いて一つの変数 \(t\) で表現できる.

4.5.4 関連する原著の演習問題

演習問題47–51

  • ► Exercise 47  [ 20 ]  図34のような回路で, \(m\) 個の出力, \(n\) 個の入力, 2つの信号を1つに変換する \(g\) 個のゲート, 1つの信号を2つに変換する \(h\) 個のゲートがあるとする. 結線の合計数を2種類の方法で表すことで, \(g\) と \(h\) の関係を見つけよ.

4.5.6 Scala版プログラム

表1中の各 \(z_i\) の値は以下の通りである (一番左は正しい値).

val zs = Seq(
  "00000000000000000000001010000000000000001000000000000000000000000000000000000000000000000000000000000",
  "10101110111111111111110111001011111111111010111111111101011111111111111011111111111111111111111111111",
  "01010000010101000100001000110001010100000000000101000010001101000000000000101000101000001000000000000",
  "01010000010000000101000000010001000101000000000100010000000100010101000000000000000001000001010000100",
  "10101111101010111010111111101110101010111111111011101111111011101011101111111111111110111110111011101")

4.5.7 練習問題

  1. \(x_1^1\), \(x_1^2\), \(x_1^3\), \(x_1^4\) は,図34のどの結線に対応しているか.
    (解答例)

    \(x_1^1\) は \(x_1\) から左に伸びる結線, \(x_1^2\) は \(x_1\) から下に伸びる結線に対応し, \(x_1^3\) は \(x_1^1\) から \(a_2\) へ入る結線, \(x_1^4\) は \(x_1^1\) から \(a_3\) へ入る結線に対応している.

  2. 表1のテストパターンで, \(z_1\) の正しい値は0である. 100通りある単一縮退故障のうち,どの場合に \(z_1=1\) となるか.
    (解答例)

    \(z_1\) の行で1となっている列を探すと \(y_1=1\), \(y_1^1=1\), \(z_1=1\) の3通りがある. したがって \(x_2x_1=11\), \(y_3y_2y_1=110\) のテストパターンは, \(y_1\), \(y_1^1\), \(z_1\) のいずれかが1に縮退する故障を発見できる.

  3. 上の練習問題より,表1のテストパターンを用いた場合, 3通りの単一縮退故障に対し \(z_1\) が間違った値になることがわかった. では,同じテストパターンで \(z_2\) に関して何通りの単一縮退故障を発見できるか. \(z_3\), \(z_4\), \(z_5\) はどうか.
    (解答例)

    例えば,以下のようにして \(z_2\) について12通りあることが確認できる.

    scala> val zs = Seq(
      "00000000000000000000001010000000000000001000000000000000000000000000000000000000000000000000000000000",
      "10101110111111111111110111001011111111111010111111111101011111111111111011111111111111111111111111111",
      "01010000010101000100001000110001010100000000000101000010001101000000000000101000101000001000000000000",
      "01010000010000000101000000010001000101000000000100010000000100010101000000000000000001000001010000100",
      "10101111101010111010111111101110101010111111111011101111111011101011101111111111111110111110111011101")
    scala> zs(1).count(_ != '1')
    res: Int = 12
    

    \(z_3\) については23通り, \(z_4\) については19通り, \(z_5\) については22通りある.

  4. 表1のテストパターンを用いた場合,何通りの単一縮退故障を発見できるか. また,どのような単一縮退故障が発見できないか.
    (解答例)

    \(z_i\) のいずれかが正しい値と異なっていれば良い. 以下から,44通りの単一縮退故障を検出できることがわかる.

    scala> (1 to 100).count(j => zs.exists(z => z(0) != z(j)))
    res: Int = 44
    

    また,以下から \(x_1=1\), \(x_1^1=1\), \(x_1^2=0\), \(x_1^2=1\) などが検出できないことがわかる.

    scala>(1 to 100).filter(j => zs.forall(z => z(0) == z(j)))
    res: Int = IndexedSeq[Int] = Vector(2, 4, 5, 6, 8, 10, 12, ..., 97, 100)
    
  5. 表1のBoole連鎖は prog/prod-2-3-wires-bchain.txt のようになっている. 原著の演習問題49に回答せよ.
    (解答例)

    プログラム例は prog/src/main/scala/stuck.scala である. 以下のように実行する.

    $ ./taocpsat stuck list_patterns Y3,Y2,Y1,X2,X1 Z5,Z4,Z3,Z2,Z1 <prod-2-3-wires-bchain.txt
    00000 Z1 00001
    .....
    01111 ~q 00001
    .....
    11111 ~Z5 00101
    

    縮退故障 Z1=1 はパターン \(y_3y_2y_1x_2x_1 = 00000\) で, 縮退故障 q=0 はパターン \(y_3y_2y_1x_2x_1 = 01111\) で検出できることがわかる.

    $ ./taocpsat stuck covering Y3,Y2,Y1,X2,X1 Z5,Z4,Z3,Z2,Z1 <prod-2-3-wires-bchain.txt
    ~ patterns of ~x1
    5 7 9 11 13 15 17 19 21 23 25 27 29 31
    .....
    ~ patterns of b3:2
    15
    .....
    ~ patterns of ~c1:2
    15
    .....
    ~ patterns of ~s:2
    15
    ~ patterns of s:2
    ~ patterns of ~p
    .....
    ~ patterns of ~q
    15
    .....
    

    縮退故障 s:2=1 を検出できるパターンは存在せず, 縮退故障 b3:2=1, c1:2=0, s:2=0, q=0 を検出できるパターンは01111だけだとわかる.

    以下のようにすれば,検出可能なすべての単一縮退故障を検出する5つのパターンを見つけられる.

    $ ./taocpsat stuck min_covering Y3,Y2,Y1,X2,X1 Z5,Z4,Z3,Z2,Z1 5 <prod-2-3-wires-bchain.txt | sat13 | tr ' ' '\n' | egrep '^[0-9]'
    (126 variables, 350 clauses, 1766 literals successfully read)
    !SAT!
    Altogether 8519+121002 mems, 31402 bytes, 145 nodes, 49 clauses learned (ave 7.3->6.6), 2585 memcells.
    (2 learned clauses were discarded.)
    (1 clause was subsumed on-the-fly.)
    (20 restarts.)
    15
    28
    31
    11
    23
    

    01111, 01011, 10111, 11100, 11111 の5つが得られている.

  6. 図34の回路について,原著の段落10で述べられている方法を用い, 与えられた縮退故障を検出せよ.
    (解答例)

    式(23)のBoole連鎖ではなく, prog/prod-2-3-wires-bchain.txt を用いる.

    以下の内容のファイル prog/prod-2-3-wires-bchain-stuck.txt を作成する.

    1. prog/prod-2-3-wires-bchain.txt と同じBoole連鎖
    2. prog/prod-2-3-wires-bchain.txt と同じだが X1, X2, Y1, Y2, Y3以外のBoole変数にプライムを付けたBoole連鎖
    3. 以下のBoole連鎖
      ZZ1 = Z1 xor Z'1
      ZZ2 = Z2 xor Z'2
      ZZ3 = Z3 xor Z'3
      ZZ4 = Z4 xor Z'4
      ZZ5 = Z5 xor Z'5
      
    4. 以下の節 (Scala版プログラムでは,Boole連鎖中で ';' から始まる行は節として扱われる)
      ; ZZ1 ZZ2 ZZ3 ZZ4 ZZ5
      

    このBoole連鎖中で,プライム付き変数 \(x'\) に対する代入を \(x' = 0\) または \(x' = 1\) に置き換えれば良い. 例えば,以下のようにすれば, \(q\) が0縮退した故障を発見するパターンが表示される.

    $ sed -e "s/^q' = .*$/q' = 0/" <prod-2-3-wires-bchain-stuck.txt | ./taocpsat bchain encode | sat13 | ./taocpsat decode log X Y
    (110 variables, 257 clauses, 589 literals successfully read)
    !SAT!
    Altogether 6445+4577 mems, 22682 bytes, 10 nodes, 2 clauses learned (ave 2.5->2.5), 815 memcells.
    (1 restart.)
    X(2..1) = 11_2 = 3
    Y(3..1) = 011_2 = 3
    

    \(y_3y_2y_1x_2x_1 = 01111\) のパターンが見つかる.

  7. knuth/sat-examples/README の "Test patterns for single-stuck-at faults" を参照して, Knuthがどのように16ビットと32ビットの乗算回路のテストパターンを作成したかを調べ,同様のことを行え.

4.6 Boole関数の学習 (Learning a Boolean function)

4.6.1 概要

未知の20変数のBoole関数 \(f\) があり, 表2のように32通りの入力に対する値がわかっている. \(f\) がどのような関数なのか,SATソルバーを用いて推測する方法を学ぶ.

4.6.2 注釈

  • 段落2: ここで述べられている方法は,CNFを発見するためにも利用できる. \(\bar f=\{2,3,10\}\land\{6,10,12\}\land\{\bar 8,13,15\}\land\{8,\bar{10},12\}\) は,表2の左右を入れ替えたデータと矛盾しない.
  • 段落3: 補助変数 \(z_{i,k}\) は,1になる \(k\) 番目の点は \(i\) 番目の項で成り立つことを表している. 求める式はDNFだから,少なくとも1つの項で成りたてば良い.

4.6.4 関連する原著の演習問題

演習問題52–64

  • ► Exercise 53  [ M20 ]  表2の値は絶対にランダムではない.なぜだかわかるか?
  • ► Exercise 54  [ 23 ]  上の演習問題の規則を用いて,表2を拡張せよ. \(M=3\), 4, 5の時, \(f(x)\) がDNFで \(M\)-項の表現を持たなくなるまでには, いくつの行が必要か?
  • ► Exercise 56  [ 22 ]  式(27)は,表2に合致し, 20変数のうち8個だけに依存している関数を表している. SATソルバーを利用すれば, \(x_j\) 中の5個だけに依存した 適切な \(f\) を実際に発見できることを示せ.
  • ► Exercise 57  [ 29 ]  上の演習問題を7.1.2項の方法と組合せ,表2に対する関数 \(f\) で, わずか6個のBoole演算(!)で計算できるものを示せ.
  • ► Exercise 58  [ 20 ]  式(29), (30), (31)に 節 \(\bar p_{i,j}\lor\bar q_{i,j}\) を追加することについて議論せよ.
  • ► Exercise 63  [ 20 ]  \(\alpha= [i_1:j_1][i_2:j_2]\ldots [i_r:j_r]\) は, 5.3.4項の演習問題で定義された通りの \(n\)-ネットワークとする. \(\alpha\) がソート・ネットワークでないことを テストするためにSATソルバーを用いる方法を説明せよ. ヒント: 定理5.3.4Zを利用せよ.

4.6.6 Scala版プログラム

4.6.7 練習問題

  1. prog/table2.txt とKnuth版プログラム sat-synth-trunc-kluj を用いて, 32点のデータに対する4項のDNFを求めよ. Knuth版プログラムの利用方法については knuth/sat-examples/README を参考にせよ.
    (解答例)

    以下のように実行すれば良い. 20, 4, 32は,それぞれ \(N\), \(M\), \(2P\) を表す.

    $ sat-synth-trunc-kluj 20 4 32 <table2.txt | sat13 | tr " " "\n" | grep -v '~' | grep '[-+]' | sort
    (224 variables, 1384 clauses, 7744 literals successfully read)
    !SAT!
    Altogether 29965+105131 mems, 73788 bytes, 483 nodes, 14 clauses learned (ave 20.2->20.2), 8061 memcells.
    (9 restarts.)
    1+14
    1+19
    1-16
    2+7
    2-10
    2-14
    2-6
    3+10
    3-12
    3-4
    4-10
    4-12
    4-19
    4-7
    

    1+14 は,第1項に変数 \(x_{14}\) が正に現れることを意味し, 2-10 は,第2項に変数 \(x_{10}\) が負に現れることを意味する. これからDNFが得られる.

    \(2P=40\) までは4項のDNFが得られる.

  2. (★) 原著の演習問題54に取り組め.
  3. (★) 原著の演習問題56に取り組め.
  4. (★) 原著の演習問題57に取り組め.
  5. (★) 原著の演習問題63に取り組め.
  6. (★) \(x\) が \(0000_2\) から \(1111_2\) の二進列として, Boole関数 \(f(x)\) の値は \(x\) が素数の時は1,合成数の時は0とする. \(f(x)\) を表す4項のDNFを求めよ. \(x\) が5ビットだと何項が必要になるだろうか.

4.7 有界モデル検査 (Bounded model checking)

4.7.1 概要

有名なConwayのライフ・ゲームが題材として取り上げられている. SATソルバーを用いれば,図35のようにライフ・ゲームでの遷移を逆向きに遡ることや, 式(37)のグライダーのパターンを探すことができる.

4.7.2 注釈

  • 段落5: ライフ・ゲームで任意のTuring機械を模倣できることが知られている.
  • 段落6: BDD (Binary Decision Diagram)は,4A巻7.1.4項で詳しく説明されている.
  • 段落9: "mem"は本シリーズ内で用いられている単位で,1memは1回のメモリ・アクセスを表す.

4.7.3 参考資料

4.7.4 関連する原著の演習問題

演習問題65–86

  • ► Exercise 65  [ 28 ]  Lifeの遷移関数(35)を節に符号化する方法を説明せよ.
    • a) 変数 \(x'_{ij}\) と \(x_{ij}\) だけを使用せよ.
    • b) BailleuxとBoufkhadの符号化(20)–(21) と同様に補助変数を用い,本文中で述べたように近傍のセル間で中間結果を共有するようにせよ.
  • ► Exercise 71  [ 22 ]  正方格子上でライフの遷移列を探す場合, この格子には8通りの異なった対称性があるから, 非対称な解が8通りの異なった形で現れる. さらに,周期の長さが \(r\) の時, 非対称な周期的な解が \(8r\) 通りの異なった形で現れる.

    本質的に同一の解が一度だけ生じるようにするには, どのような節をさらに加えれば良いか説明せよ: 「正規形 (canonical forms)」だけが条件を満たす.

  • ► Exercise 73  [ 21 ]  (流動的フリップフロップ) 省略
  • ► Exercise 82  [ 22 ]  (光速) ライフが無限平面上にあり,左下の象限以外では時刻0ですべてのセルが死滅しているとしよう. より正確には, \(X_t=(x_{tij})\) が, すべての \(t\ge0\) およびすべての整数 \(-\infty<i,j<+\infty\) に対して定義され, \(i>0\) あるいは \(j>0\) なら常に \(x_{0ij}=0\) とする.
    • a) \(0\le t<\max(i,j)\) なら常に \(x_{tij}=0\) であることを証明せよ.
    • b) さらに, \(0\le-i\le j\) かつ \(0\le t<i+2j\) なら \(x_{tij}=0\) .
    • c) また, \(i\ge0\) かつ \(j\ge0\) の時, \(0\le t<2i+2j\) に対し \(x_{tij}=0\) .

    ヒント: \(i\ge-j\) なら常に \(x_{tij}=0\) がいえれば, \(i>-j\) なら常に \(x_{tij}=0\) である.

  • ► Exercise 85  [ 39 ]  (エデンの園) 省略

4.7.6 Scala版プログラム

4.7.7 練習問題

  1. インターネットでライフ・ゲーム (Conway's Game of Life)について調べよ.
    (解答例)

    Youtubeなら動画も見つかる.

  2. Golly をインストールし,図35を試して見よ.
    (解答例)

    Gollyで prog/life-fig35.rle をopenする. スペース・キーを押すと,次の状態に移る.

  3. knuth/sat-examples/README を読み,図35のパターンを見つけよ.
    (解答例)

    以下のように実行する.

    $ sat-life-grid 7 15 3 >/tmp/slg3.sat
    $ sat-threshold-bb-life15 105 39 >/tmp/stb39.sat
    $ cat ../knuth/sat-examples/sources/7x15life3.dat /tmp/slg3.sat /tmp/stb39.sat | sat13 h10 | sat-life-filter
    

    図35と同じパターンだろうか?

  4. (★) "LIFE"で終わるパターンでなく,"SAT"で終わるパターンを探せ.
    (解答例)

    prog/src/main/scala/life.scala を利用する.

    $ sat-life-grid 7 15 4 >/tmp/a.sat
    $ ./taocpsat life pattern d <life-sat.txt >/tmp/b.sat
    $ ./taocpsat life threshold_bb 7 15 38 a b c >/tmp/c.sat
    $ cat /tmp/a.sat /tmp/b.sat /tmp/c.sat >/tmp/d.sat
    $ sat13 h11 </tmp/d.sat | sat-life-filter
    
    .................
    .**....*.........
    ...**..*...*.*...
    .**.*.**.*...**..
    ..*.....**..***..
    .**..*.*...*..*..
    .****....*..*....
    ......**.*...*...
    .................
    
  5. (★) 原著の演習問題65に取り組め.
  6. (★) 原著の演習問題73に取り組め.

4.8 TODO 相互排除への応用 (Applications to mutual exclusion)

4.8.1 概要

式(40)のような,2つの並行して動作するプログラムについて, 相互排除が行えているかをSATソルバーを用いて検証する方法を学ぶ.

4.8.3 関連する原著の演習問題

演習問題87–102

  • ► Exercise 94  [ 21 ] 
  • ► Exercise 98  [ M23 ] 
  • ► Exercise 101  [ 31 ] 

4.9 TODO デジタル断層撮影 (Digital tomography)

4.9.1 概要

図36のような白黒画像で,各行,各列,各対角線について黒のピクセルの個数がわかっているとする. SATソルバーを用いて元の画像を復元することは可能だろうか.

4.9.2 関連する原著の演習問題

演習問題103–118

  • ► Exercise 107  [ 22 ] 
  • ► Exercise 109  [ 20 ] 
  • ► Exercise 113  [ 30 ] 

4.9.4 練習問題

  1. (★) 原著の演習問題107に取り組め.
  2. (★) 原著の演習問題118に取り組め.

4.10 TODO SATの例—まとめ (SAT examples—summary)

5 TODO バックトラック法のアルゴリズム (BACKTRACKING ALGORITHMS)

5.1 SATに対するバックトラック法 (Backtracking for SAT)

5.1.1 アルゴリズムA

以下のように実行する.

$ ./taocpsat SolverA <rivest-sat.sat
(4 variables, 7 clauses, 21 literals successfully read)
!SAT!
 ~1 2 ~3 4
Altogether 227+115 mems, 600 bytes, 3 nodes.

Knuth版 sat0 に相当するが,プログラムの記述はテキストに沿っている.

$ sat0 <rivest-sat.sat
(4 variables, 7 clauses, 21 literals successfully read)
!SAT!
 ~1 2 ~3 4
Altogether 337+115 mems, 600 bytes, 3 nodes.
  • 前処理部分のメモリアクセス数 (227および337)は一致しない.
  • 探索処理部分のメモリアクセス数 (115)は一致するようにしている.

5.2 遅延データ構造 (Lazy data structures)

5.2.1 アルゴリズムB

実行方法は SolverA と同様である. Knuth版 sat0w に相当するが,プログラムの記述はテキストに沿っている.

5.3 単位節からの強制動作 (Forced moves from unit clauses)

5.3.1 アルゴリズムD

実行方法は SolverA と同様である. Knuth版 sat10 に相当するが,プログラムの記述はテキストに沿っている.

5.4 アルゴリズムの比較 (Comparison of the algorithms)

5.5 *もっと頑張って速度向上 (Speeding up by working harder)

5.6 *Speeding up by looking ahead

5.7 *Looking even further ahead

6 TODO RANDOM CLAUSES

6.1 Random satisfiability

6.2 Analysis of random 2SAT

7 TODO 節の導出 (RESOLUTION OF CLAUSES)

7.1 導出 (Resolution)

7.2 *一般の導出の下界 (Lower bounds for general resolution)

8 TODO 節学習のアルゴリズム (CLAUSE-LEARNING ALGORITHMS)

8.1 導出によるSAT解法 (SAT solving via resolution)

8.2 衝突駆動の節学習 (Conflict driven clause learning)

8.3 充足不能の証明書 (Certificates of unsatisfiability)

8.4 *不要な節の処分 (Purging unhelpful clauses)

8.5 *リテラルの洗浄とリスタート (Flushing literals and restarting)

9 TODO MONTE CARLO ALGORITHMS

9.1 Monte Carlo methods

10 TODO THE LOCAL LEMMA

10.1 The Local Lemma

10.2 Traces and pieces

10.3 Arithmetic on traces

10.4 *Traces and the Local Lemma

11 TODO MESSAGE-PASSING ALGORITHMS

11.1 *Message passing

12 TODO 節の前処理 (PREPROCESSING OF CLAUSES)

12.1 *節の前処理 (Preprocessing of clauses)

13 TODO 制約の節への符号化 (ENCODING CONSTRAINTS INTO CLAUSES)

13.1 制約の節への符号化 (Encoding constraints into clauses)

13.1.1 注釈

  • 段落4: 演習問題7.1.1–55(b)の符号化方法は, \(p-3\) 個の補助変数 \(t_2\), \(\ldots\), \(t_{p-2}\) を導入し, \(1<j<p\) に対し \(t_{j-1}\lor\bar y_j\), \(t_{j-1}\lor\bar t_j\), \(\bar y_j\lor\bar t_j\) という 合計で \(3p-6\) 個の二項節を用いる. ただし \(t_1 = \bar y_1\), \(t_{p-1} = y_p\) とする.
  • 段落5: Langford対の問題は \(n=4m-1\) か \(n=4m\) の時だけ解を持つ.
  • 段落6: 順序符号化は,訳者らが整数上の線形制約 \(\sum_{i=1}^n a_i x_i \le b\) に 適用できるよう発展させた [N. Tamura, A. Taga, S. Kitagawa, M. Banbara Constraints 14, 254–272, 2009参照].
  • 段落7: 直接符号化,多値符号化,対数符号化,順序符号化については [田村直之,丹生智也,番原睦則: 制約最適化問題とSAT符号化, 人工知能学会誌, 25巻1号, 77–85, 2010] に解説がある.
  • 段落8: \(n\times n\) のチェス盤で,各マスを頂点とし,クイーンが動ける頂点同士が辺で結ばれているグラフを クイーン・グラフ (queen graphs)という. クイーン・グラフを \(n\) 色で彩色できた場合, \(n\) 個ずつの \(n\) 個のグループからなるクイーン(計 \(n^2\) 個)を, \(n\times n\) のチェス盤に同じグループのクイーン同士が互いに取られないように配置できる.\par この問題は, \(n \equiv \pm 1\ (\mod 6)\) の場合に \(n\) 色で彩色できることが知られている. それ以外の場合, \(n \le 11\) なら \(n\) 彩色はできない. \(n \ge 12\) については, 26以下のすべてについて \(n\) 彩色が発見されている (2005年時点).
  • 段落9: 田島宏史は神戸大学大学院自然科学研究科の修士課程学生である. 日本の大学の修士論文がTAOCPに引用されたのは始めてのことだと思う. 田島は,クイーン・グラフ彩色問題と類似した 汎対角ラテン方陣問題について網羅的に調査し,(162)のヒント節が有効なことを発見した.
  • 段落13: 2SAT問題は,多項式時間で解けることがわかっている. したがって,各制約が高々2個の変数を含む関係の集合は,順序符号化を用いれば多項式時間で解ける.
  • 段落14: 前述の訳者らの論文 [N. Tamura, A. Taga, S. Kitagawa, M. Banbara Constraints 14, 254–272, 2009]では, 3変数の制約を \(O(d^2)\) 個の節で表している.

13.1.3 関連する原著の演習問題

演習問題387–419

  • ► Exercise 387  [ 21 ] 
  • ► Exercise 389  [ 22 ] 
  • ► Exercise 390  [ 23 ] 
  • ► Exercise 396  [ 23 ] 
  • ► Exercise 397  [ 22 ] 
  • ► Exercise 399  [ 23 ] 
  • ► Exercise 404  [ 21 ] 
  • ► Exercise 405  [ M23 ] 
  • ► Exercise 407  [ M22 ] 
  • ► Exercise 408  [ 25 ] 
  • ► Exercise 409  [ M26 ] 
  • ► Exercise 411  [ 25 ] 
  • ► Exercise 415  [ M22 ] 

14 TODO 単位伝播と強制 (UNIT PROPAGATION AND FORCING)

14.1 単位伝播と強制 (Unit propagation and forcing)

15 TODO 対称性除去 (SYMMETRY BREAKING)

15.1 対称性除去 (Symmetry breaking)

16 TODO 充足可能性を保つ写像 (SATISFIABILITY-PRESERVING MAPS)

16.1 充足可能性を保つ写像 (Satisfiability-preserving maps)

17 TODO 100個のテスト・ケース (ONE HUNDRED TEST CASES)

17.1 100個のテスト・ケース (One hundred test cases)

18 TODO パラメータの調整 (TUNING THE PARAMETERS)

18.1 パラメータを調整する (Tuning up the parameters)

19 TODO EXPLOITING PARALLELISM

19.1 Exploiting parallelism

20 TODO HISTORY

20.1 A brief history

?????

Date: 2018-07-19 11:12:10 JST

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

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0