魔術師見習いのノート

プロフィール

魔術師見習い
Author魔術師見習い-_-.
Twitter魔術師見習い

コンピュータ関係のメモを主に書きます.

MENU

MiniSat

投稿日:
タグ:

目次

SATソルバ

充足可能性問題を解決するためのツールとしてSATソルバというソフトウェアがある.SATソルバは与えられた論理式が充足可能かどうかを判断する.充足可能である場合,SATソルバは論理式が真になる時の論理変数の値を1つ返す.多くのSATソルバーでは,入力可能な論理式は乗法標準形のみである.全ての論理式は論理同値な乗法標準形に変換できる.

MiniSat

ここでは,MiniSatというSATソルバについて簡単に説明する.MiniSatは,SAT問題に関わる活動を始める研究者や開発者を助けるために開発された最小かつオープンソースのSATソルバである.MiniSatの最初のバージョンは,C++でコメント文を除くと600行ほど,バージョン2でさえ1500行ほどで記述されている.また,そのソースコードは,読みやすく,拡張がしやすい設計となっている.MiniSatは,MITライセンスの元で配布されており,多くの環境で動作する.MiniSatは,コマンドライン上で実行されるプログラムである.

実行方法は次のような感じである.

user% minisat2 input.cnf output.cnf
ここで,input.cnfは入力ファイル,output.cnfは出力ファイルである.入力ファイルは,DIMACS CNF形式である.

出力ファイルは,1行目に充足可能であるかどうかが記述されている.

SAT充足可能
UNSAT充足不能
SATの場合,更に2行目に全体の論理式が真になる場合の各命題変数の値が1パターン記述されている.各命題の真偽については,DIMACS CNF形式と同様の記述である.

DIMACS CNF形式

The Center for Discrete Mathematics & Theoretical Science(DIMACS)とは,離散数学と利論的コンピュータサイエンスのためのセンタのこと.ラトガース大学,プリンストン大学,AT&Tベル研究所とBellcore社の研究者らが,全米科学財団の科学技術センターとして運営している研究者の協会である. 彼らの挑戦の1つの提案は,共通のインスタンスと解析ツールのテストベッドを提供することによってアルゴリズムや発見手法の試験や比較に要求される労力を減らすことである.この労力を減らすため,標準フォーマットが必要だった.そのフォーマットの1つが,MiniSatの入力ファイル形式として使用されるDIMACS CNF形式である.研究者たちは論理式を変換するための翻訳プログラムをもっと手軽に,またはもっと簡潔に開発することを望んでいる.UNIXのawkの機能は,この作業に特に適しているとして推奨されている.

MiniSatを含むSATソルバの多くは,このフォーマットを入力対象とする.これは,毎年開催されるSATソルバの性能を競争するSAT competitionにおいて,そのフォーマットが指定されていることに起因する.各SATソルバの性能を競う上で入力インターフェースの統一は必要不可欠である.

DIMACS CNF形式のファイルは,ASCII文字から成る.このファイル形式は,以下で述べる種類のいくつかの行をもつ.そして,それらの行は改行文字で終わる.各行の欄は,最小1つのブランクスペースによって分けられる.このファイル形式の各行は,PreambleとClausesによって分類できる.

Preamble

Preambleでは,行の最初が行の種類を決める1つの文字(次にスペースが続く)から始まる.それらのタイプは,次の2つからなる.

Comments行
c This is a comment line.
Problem行

p FORMAT VARIABLES CLAUSES
FORMAT"cnf"が入る.
VARIABLES命題変数の数.
CLAUSES節数.

Clauses

Clausesは,problem行の次の行から開始される.そこで,使用される命題変数名は,1からVARIABLESの番号がつけられる.もちろん,すべての変数が論理式に登場する必要はない.各節は,空白やタブ,改行で区切られる数字の列で表される.変数をiとした時,論理否定するものを-iと表し,そうでないものをiと表す.各節は,0によって終わる.

(X1∨X2)∧X3∧(X4∨X5)∧¬X2に対応するDIMACS CNF形式の入力ファイルの中身と,それをMiniSatに与えた時の出力結果,出力ファイルの中身を示す.

input.cnf
p cnf 5 4
1 2 0 3
4 5 0
-2 0
実行結果
user% minisat input.cnf output.cnf
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics
]=============================
|
|
WARNING! DIMACS header mismatch: wrong number of clauses.
|  Number of variables:             5
|
|  Number of clauses:               2
|
|  Parse time:                   0.00 s
|
|  Eliminated clauses:           0.00 Mb
|
|  Simplification time:          0.00 s
|
|
|
============================[ Search Statistics
]==============================
| Conflicts |          ORIGINAL         |          LEARNT          |
Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |
|
===============================================================================
===============================================================================
restarts              : 1
conflicts             : 0              (-nan /sec)
decisions             : 1              (0.00 % random) (inf /sec)
propagations          : 2              (inf /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 8.00 MB
CPU time              : 0 s

SATISFIABLE
output.cnf
SAT
1 -2 -3 -4 5 0

SATソルバによる数独の解法

投稿日:
修正日:
タグ:

注意:この記事はWEBブラウザがCSSに対応していることを前提に書かれています.

数独はSATソルバにより解法できる.とはいえ,充足可能性判定問題はNP完全なので,数独の規模やコンピュータの性能によっては解けない問題もある.

数独

数独は「数字は独身に限る」という名前に由来するペンシルパズルの1つである.

数独のルールはラテン方陣の応用である.ラテン方陣とは,各行と各列にそれぞれ1からnの整数が1回だけ出てくるn×nの行列である.数独はさらに小行列を持つ(必ずしも小行列とは限らないが).小行列はn個の要素を持ち,1からnの整数を1つずつ含む.

数独のルールは次の4種類から成る.この記事では,nの値を4として説明する.

数独の解は,これらの全てを満たす.

各マス(要素)のルール
  • 1つのマスに1から4の整数が入る.
  • 各行の各列の各マスには値が1つだけ入る.
各行のルール
各行各のマスには,各値は1度だけ現れる.
各列のルール
各列の各マスには,各値は1度だけ現れる.
小行列のルール
各小行列の各マスには,各値は1度だけ現れる.
実際の数独の問題は,このような共通ルールに加え,いくつかのマスの値が予め確定しているなどの非共通ルールを持つ.非共通ルールについては,後で言及する.

結論からいうと,各行と列,小行列のルールと,各マスのルールの後者は,皆似たような記述で表現できる.そこで,各マス(要素)のルールの2つを代表として説明し,残りのルールについては各マスのルールの後者との差異だけを紹介する.まずこのルールを命題を用いていくつかの言語で示す.

  • 日本語(自然言語)
  • 述語論理
  • 命題論理
  • 命題論理(CNF)
  • 命題論理(DIMACS CNF形式)
それぞれの表現方法については,ここでは説明しない.これらを用いた表現方法を説明した後,数独のルールの一部を出力するCNF式を出力するRubyプログラムを説明し,最終的に他のルールへの適応方法を紹介する.

日本語(自然言語)の場合

命題には,次のようなものを使用する.

命題: i行目のj列目の値がkである

1行目の1列目のマスを考えた時,それを表す命題は次のように表現できる.

  1. 1行目の1列目のマスの値は1である.
  2. 1行目の1列目のマスの値は2である.
  3. 1行目の1列目のマスの値は3である.
  4. 1行目の1列目のマスの値は4である.
これを参考にして,前述のルールを記述すると,次のように表現できる.
  • "1行目の1列目のマスの値は1"または"1行目の1列目のマスの値は2"または"1行目の1列目のマスの値は3"または"1行目の1列目のマスの値は4"である.
ここで,あえて冗長な表現で記述している理由は,他の言語に対応付ける際に都合が良いからである.

次に,もう1つの各マスのルール「各行の各列の各マスには値が1つだけ入る.」について説明する.そして「各行の各列の各マスには値が1つだけ入る.」というルールは,前述の各命題を参考にすると,次のように記述できる.

  • "1行目の1列目のマスの値は1"または"1行目の1列目のマスの値は2"または"1行目の1列目のマスの値は3"または"1行目の1列目のマスの値は4"である.
  • "1行目の1列目のマスの値が1"ならば,"1行目の1列目のマスの値は2"か"1行目の1列目のマスの値は3"か"1行目の1列目のマスの値は4"でない.
  • "1行目の1列目のマスの値が2"ならば,"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は3"か"1行目の1列目のマスの値は4"でない.
  • "1行目の1列目のマスの値が3"ならば,"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は2"か"1行目の1列目のマスの値は4"でない.
  • "1行目の1列目のマスの値が4"ならば,"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は2"か"1行目の1列目のマスの値は3"でない.
この表現は元のルールと対応する表現とは言い難いが,先に示したルールを満たす.元のルールは述語記号や量化記号,存在記号を用いることで表現できる.

述語論理の場合 Part.1

前述の日本語で示した表現を今度は述語論理で表現する. ここでは,次のような記号を使用する.

補助記号: ( ) ,
論理記号: ∨ ∧ ¬ ⇒
対象変数: i j k

Cell(i,j,k): i行目のj列目の値がkである.
これらの記号を用いた時,先ほどの表現はそれぞれ次のように記述できる.
「1つのマスに1から4の整数が入る.」
Cell(1,1,1)∨Cell(1,1,2)∨Cell(1,1,3)∨Cell(1,1,4)∧
「各マスには整数が1つだけ入る.」
(Cell(1,1,1)⇒¬(Cell(1,1,2)∨Cell(1,1,3)∨Cell(1,1,4)))∧
(Cell(1,1,2)⇒¬(Cell(1,1,1)∨Cell(1,1,3)∨Cell(1,1,4)))∧
(Cell(1,1,3)⇒¬(Cell(1,1,1)∨Cell(1,1,2)∨Cell(1,1,4)))∧
(Cell(1,1,4)⇒¬(Cell(1,1,1)∨Cell(1,1,2)∨Cell(1,1,3)))

命題論理の場合

Cell(1,1,1),Cell(1,1,2),Cell(1,1,3),Cell(1,1,4)をそれぞれa,b,c,dという命題変数とした時,前述の式は次のように記述できる.

「1つのマスに1から4の整数が入る.」
a∨b∨c∨d∧
「各マスには整数が1つだけ入る.」
(a⇒¬(b∨c∨d))∧
(b⇒¬(a∨c∨d))∧
(c⇒¬(a∨b∨d))∧
(d⇒¬(a∨b∨c))
同様に「"1行目の1列目のマスの値が2"ならば,"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は3"か"1行目の1列目のマスの値は4"でない」と表現できる.

命題論理(CNF)の場合

SATソルバは,CNF式のみを受け付ける.そのため,前述の式をCNF式に変換例を示す.ただし,ここでは「a⇒¬(b∨c∨d)」をCNF式に変換する例だけを紹介する.これは,いくつかのCNF式を論理積で繋いだ式がCNF式であることに起因する.この例に限らず,論理積で結合される各式がそれぞれCNF式に変換できれば,同様のやり方でCNF式に変換できる.

a⇒¬(b∨c∨d)⇔
¬a∨¬(b∨c∨d)⇔
¬a∨(¬b∧¬c∧¬d)⇔
(¬a∨¬b)∧(¬a∨¬c)∧(¬a∨¬d)
同じような変換を他の節にも行うことで,全てCNF式に変換できる.なお,「¬a∨¬b」と「¬b∨¬a」などは意味が重複しているため冗長であるが,これについてここでは考慮しない.

命題論理(DIMACS CNF形式)の場合

前述のCNF式をSATソルバが読み取り可能な形式(DIMACS CNF形式)に書き換えると,このようになる.DIMACS CNF形式では,命題変数を絶対値が1以上の整数,論理否定を"-",論理和をスペースや改行などの区切り,論理積を"0"で表す.DIMACS CNF形式の詳細については,ここでは言及しない.ここで命題変数はaを1,bを2,cを3,dを4で表す.

1 2 3 4 0
-1 -2 0
-1 -3 0
-1 -4 0
-2 -1 0
-2 -3 0
-2 -4 0
-3 -1 0
-3 -2 0
-3 -4 0
-4 -1 0
-4 -2 0
-4 -3 0

述語論理の場合 Part.2

ユーザがルール全てをタイプするのは困難である.そこで,SATソルバに与える入力ファイルを生成するプログラムを作成する.ここでは代表してマスのルールを述語論理で表す.その後,それに対応した入力データを作成するためのRubyプログラムを紹介する.

ここでは,述語記号Cellや主語を表すiとj,kは,前述と同じである.次の式は各マスのルールを表している.

補助記号: , ( ) { }
対象定数: 1 2 3 4
対象変数: i j k k'
述語記号: ∈ Cell = ≠

i∈{1,2,3,4}
j∈{1,2,3,4}
k∈{1,2,3,4}
k'∈{1,2,3,4}

∀i(∀j(∃k(Cell(i,j,k)∧∀k'((k≠k')⇒¬Cell(i,j,k')))))

命題論理(DIMACS CNF形式)式を出力するRubyプログラム

以下に前述で示した述語論理の式を出力するRubyプログラムを紹介する.ちなみにRubyである必要性はない.

s = [1, 2, 3, 4]

for i in s
  for j in s 
    for k in s
      print "#{Cell(i,j,k)} "
    end
  end
end
puts "0"

for i in s
  for j in s
    for k1 in s
      for k2 in s   
        if i != j then
          puts "#{-Cell(i,j,k1)} #{-Cell(i,j,k2)} 0"
        end
      end
    end
  end
end

その他のルール

行や列,小行列の場合も同じような考え方である.以下に,数独の全てのルールを述語論理で示す.なお,述語記号の意味は前述と同じである.ここで,「∃k(Cell(i,j,k)∧∀k'((k≠k')⇒¬Cell(i,j,k'))」を∃!と省略する.

補助記号: , ( ) { } |
対象定数: 1 2 3 4
対象変数: a b i j k l 
関数記号: ∃! + -
述語記号: ∈ Cell ≦ 


i,j,k∈{1,2,3,4}
a,b∈{1,2}
l∈{x∈Z|2a-1≦x≦2a}
c∈{x∈Z|2b-1≦x≦2b}

∀i∀j∃!k Cell(i,j,k)
∀i∀k∃!j Cell(i,j,k)
∀j∀k∃!i Cell(i,j,k)
∀a∀b∀l∀c∃!k Cell(l,c,k)

このように他のルールに関しても同じように記述できる.それゆえ,入力ファイルを生成するためのプログラムも要領は同じである.

非共通ルール

一般的な数独の問題では,いくつかのマスの値が始めから決まっている.これらを命題論理の式で示すのは難しくない.

1
1
例えば,前述の述語記号を使って"1行目の1列目が1"で"4行目の4列目が1"であることを表す場合,次のように書けば良い.
... ∧
Cell(1,1,1)∧
Cell(4,4,1)

この論理式はCNF式である.それゆえ共通ルールと非共通ルールの両方を満たす論理式もまたCNF式である.

命題変数と命題の相互変換

SATソルバで解法を行うためには,命題と命題変数を対応付ける必要がある.数独の場合,行番号と列番号,マスの値から命題変数へ命題変数から行番号と列番号,マスの値への変換ができれば,それが可能となる.

例えば,Cell(1,1,1)が命題変数1に,Cell(4,4,1)が命題変数61に対応する時(解があれば),次のようなファイルが出力される.

SAT
1 -2 -3 -4 ... 61 -62 -63 -64 0
この時,真である命題変数が各マスの値を指す.このような変換と逆変換は,ユーザが行うよりも,入力ファイルを作成したようにプログラムを使った方が効率が良い.そのためには,行と列,値に応じて命題変数を返す関数やその逆変換を行う関数を定義する必要がある.

その他のパズル

最後に特殊な数独と数独以外のパズルを紹介しているサイトを示す.

一覧