魔術師見習いのノート

プロフィール

魔術師見習い
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

一覧