日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

iSugar : インクリメンタル SAT 解法が利用可能な
SAT 型制約ソルバー
迫 龍哉

宋 剛秀

番原 睦則

田村 直之

鍋島 英知

井上 克巳

近年，命題論理の充足可能性判定 (SAT) 問題を解く SAT ソルバーの飛躍的な性能向上を背景に，制約充足問題をSAT に変換し，SAT ソルバーを用いて求解する SAT 型制約ソルバーが成功を収めている．しかしながら，制約最適化問題，解列挙問題などに対しては，SAT ソルバーを複数回起動する必要があり，求解性能が大きく低下することがある．この問題を解決する方法として，インクリメンタル SAT 解法の利用が挙げられる．SAT Race 2015 で，
このような解法を容易に実現するためのインクリメンタル SAT API が提案された．本稿では，インクリメンタル
SAT API の拡張と，これに対応したインクリメンタル SAT 型制約ソルバーを提案する．提案システムの実現として，iSugar を開発した．iSugar の特長は，上記の求解困難な問題に対して，ただ一度だけ SAT ソルバーを起動し，かつ学習節を再利用することにより，求解性能を大きく向上できる点である．実験の結果，ショップスケジューリン
グ問題，N-クイーン問題，ハミルトン閉路問題に対して，iSugar の有効性を確認した．

Remarkable improvements on SAT solvers over the last decade have led the success of SAT-based constraint
solvers. However, existing SAT-based constraint solvers cannot eﬃciently solve constraint optimization andenumeration problems since those solvers invoke SAT solvers multiple times from scratch and cannot reusesearch information such as learnt clauses. Recently, incremental SAT method has been proposed to eﬃciently solve these problems. In addition, SAT Race 2015 provides its API which enables us to implement
general purpose system using incremental SAT method. In this paper, we extend the incremental SAT API
and develop the incremental SAT-based constraint solver iSugar. By using the incremental SAT method,
iSugar can reduce the invocation overhead and allows us to reuse learnt clauses. To evaluate the eﬃciency
of iSugar, we carried out experiments on shop-scheduling, N-queens, and Hamiltonian cycle problems. In
the result, iSugar succeeded in improving computation time and the number of solved instances comparedwith the existing constraint solver Sugar.

1 はじめに
制約充足問題 (CSP; Constraint Satisfaction Prob-lem) は与えられた制約条件を満たす値の割当てを決定
iSugar : A SAT-based Constraint Solver Utilizing Incremental SAT Method
Tatsuya Sako, 神 戸 大 学 大 学 院 シ ス テ ム 情 報 学 研 究科, Graduate School of System Informatics, Kobe
University.
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.
Hidetomo Nabeshima, 山梨大学大学院医学工学総合研究部, Department of Research Interdisciplinary Graduate School of Medicine and Engineering, University
of Yamanashi.
Katsumi Inoue, 国立情報学研究所情報学プリンシプル
研究系, Principles of Informatics Research Division,
National Institute of Informatics.

する問題である．人工知能の分野における多くの組合せ
問題は CSP として定式化可能であり，CSP を効率よく解くことは重要なテーマとなっている [23] [1] [4] [14]．
近年，命題論理の充足可能性判定 (SAT; Boolean Sat-isfiability Testing) 問題を解く技術が進歩しており，非常に高速に解を求めることのできる SAT ソルバーが実現されている [12] [3]．これによって CSP を一度

SAT 問題に符号化してから高速 SAT ソルバーで解を求め，その解を復号化して元の解を求める SAT 型
制約ソルバーと呼ばれるシステムが注目を集めており [26] [17] [24] [10] [18]，そのひとつである Sugar は多くの問題で高い性能を示している [20]．

能である．

CSP に関連する問題として，制約最適化問題，解iSugar で既存のシステムとの比較実験を行った結果，列挙問題がある．これらは CSP を繰り返し解く必要

オープンショップスケジューリング問題では平均 16があり，一般に CSP よりも求解が困難である．既存倍の高速化に成功した．また N-クイーン問題の解列の SAT 型制約ソルバーは，これらの問題を解く際に挙では解の総数が多いほど性能が向上し，ハミルト

は CSP を解く回数と同じだけ SAT ソルバーを起動

ン閉路問題では求解問題数が 33 問増加した．以上かする．しかしながら，ひとつの問題から生成される各ら，iSugar の有効性が確認できた．

SAT 問題の大部分は共通の制約であるため，SAT ソ

本稿の構成は次の通りである．2 節で SAT と CSP

ルバーは同一の探索空間を何度も調べることになり，について説明し，SAT 型制約ソルバーの問題点を挙求解効率が低下するという問題点がある．

げてその解決案を提示する．3 節でインクリメンタ

上記のように SAT ソルバーを繰り返し起動するこル SAT 解法とこれを利用する API について説明し，となく，制約最適化問題や解列挙問題を効率的に解API の拡張を提案する．4 節で iSugar の設計と実装

くために，インクリメンタル SAT 解法 [6] の利用がについて述べる．5 節で具体的な問題に対する評価実有効であることが知られている．インクリメンタル

験の結果を示して考察を行い，6 節で結論をまとめる．

SAT 解法は有界モデル検査 [2] などに利用されている手法であり，SAT ソルバーが同様の探索失敗を避け

2 SAT 型制約ソルバー

るために獲得した学習節を保持することで，無駄な

本節では，SAT と CSP について簡単に説明し，探索を行うことなく，節を追加した SAT 問題を連続SAT 型制約ソルバーとその問題点について述べたの的に解くことができる [13] [11]．このため，CSP を繰

ち，問題点を解決する方法の提案を行う．

り返し解く問題群に対して求解性能の向上が期待される．

2. 1 SAT

また最近では，SAT Race 2015†1 においてインク

充足可能性判定問題 (SAT) とは，与えられた命題

リメンタル SAT を利用する汎用的な API が公開さ論理式が真となる値の割当ての存在を判定する問題れた．しかし，この API には提供されている機能がである．そのような値割当てが存在すれば充足可能

低レベルで記述が冗長になる，Java アプリケーショ(sat)，しなければ充足不能 (unsat) であるという．

ンからの利用を考慮していないという問題点がある．

SAT 問題は通常，連言標準形 (CNF; Conjunctive

そこで，本稿では以下の 2 点を提案する．

Normal Form) で与えられる．CNF は節の連言であ

1. SAT Race 2015 のインクリメンタル SAT API
を高機能化し，また Java アプリケーションからも利用可能にする拡張された API

2. 1. の API に対応し，インクリメンタル SAT 解法が利用可能な SAT 型制約ソルバー

り，各節はリテラルの選言で表される．また，リテラ
ルは命題変数またはその否定である．

SAT 問題を解くプログラムは SAT ソルバーと呼ばれる．SAT ソルバーは CNF を受け取ってそれがsat か unsat かを判定し，sat ならその解となる値

提案システムの実現として，インクリメンタル SAT

割当てをひとつ返す．近年の SAT ソルバーには，求型制約ソルバー iSugar を開発した．iSugar の特長は，解過程で発生する矛盾から獲得した学習節を利用し，次の通りである．

解を探索する CDCL アルゴリズム [9] などの高速化• インクリメンタル SAT 解法が利用可能である．

技術が取り入れられており，その性能は飛躍的に向上• SAT Race 2015 のインクリメンタル SAT API

している [12]．これに伴い，直接求解することが困難

を実装している高速 SAT ソルバーとの結合が可な問題を SAT 問題に変換し，SAT ソルバーを用いて解くという手法が確立されている．

†1 http://baldur.iti.kit.edu/sat-race-2015/

2. 2 CSPを行う．このように既存の SAT 型制約ソルバーのほ

制約充足問題 (CSP) とは，与えられた制約式をす

とんどは，SAT ソルバーが本体とは別のプロセスとべて満たすことができるような変数の値の割当てをして動作する疎な結合となっている．この結合方法で決定する問題である．本稿では，整数の有限領域上のは，前節で挙げたような CSP を複数回解く必要のあ

CSP を単に CSP と呼ぶ．CSP は，整数変数の有限る問題の求解において，以下の問題が生じる．

集合，各変数の取り得る値の集合 (ドメイン)，制約の有限集合によって構成される．

CSP に関連する問題として，与えられた制約を満たしつつ特定の変数の値を最小化または最大化す• 学習節をはじめとする，その後の探索に有益な情報を保持できない．

• 同一の探索空間を繰り返し調べるため，探索に無駄が多い．

る制約最適化問題 (COP; Constraint Optimization• プロセス起動，ファイル I/O などの処理が複数

Problem)，制約を満たす値割当てを列挙する解列挙問

回起こり，求解以外の部分におけるオーバーヘッ

題などがある．また，CSP として定式化・求解する際ドが大きい．

に CEGAR (Counter-Example Guided Abstraction

これらはいずれも，各 SAT 問題を解く度に SAT ソ

Refinement) [5] を用いると効率よく解ける問題もあルバーを起動することが原因である．上記の問題点をる．例として，ハミルトン閉路問題 (HCP; Hamilto-

解決するため，SAT 型制約ソルバーをインクリメン

nian Cycle Problem) においては CEGAR 解法の有タル SAT 解法へ対応させる．

効性が示されている [16]．これらは，いずれも CSPを繰り返し解くことで求解が可能である．

3 インクリメンタル SAT API の提案
本節では，インクリメンタル SAT 解法の概要およ2. 3 SAT 型制約ソルバー

び SAT Race 2015 より公開されたインクリメンタル

CSP の解を探索するプログラムは制約ソルバーとSAT API の説明を行い，API の拡張の提案と設計，呼ばれる．その中でも，CSP を一度 SAT 問題に変実装について述べる．

換 (SAT 符号化) して，SAT ソルバーを用いて元の問題の解を求めるシステムが注目されている．この3. 1 インクリメンタル SAT 解法

ようなシステムを SAT 型制約ソルバーという．代

インクリメンタル SAT 解法とは，複数の SAT 問

表的な SAT 型制約ソルバーである Sugar は，順序

題を連続して効率的に解く手法である．以下で，その符号化法 [21] と呼ばれる SAT 符号化法を用いてお内容を説明する．

り，国際 CSP ソルバー競技会の GLOBAL 部門に最新の SAT ソルバーの多くは，求解終了後も結果

おいて，2008-2009 年の 2 年連続で優勝した [22]．まが sat であれば，その探索で追加された学習節を次た，ショップスケジューリング問題において当時未知回以降の探索で利用できる．また，仮説 (部分的な真であった最適値を決定するなど，多くの問題で成功を偽値の割当て) を与えて探索することも可能である．

収めている [20]．

これらの機能により，節を追加した問題や仮説を変更

しかしながら，既存の SAT 型制約ソルバーには前した問題を複数回解く場合に，前回の探索において述のインクリメンタル SAT 解法に対応していないと獲得した学習節を再利用できる．その結果，探索空間いう問題点がある．このことについて，Sugar を例にの枝刈りが行われ，効率よく解を探索することがで説明する．Sugar は CSP が記述されたファイルを読きる．

み込んで SAT 符号化した節をファイルに書き出し，

2.2 節で挙げた問題は，SAT 問題を繰り返し解く

SAT ソルバーを起動する．SAT ソルバーはファイル問題群である．したがって，インクリメンタル SATから CNF を読み込んで解の探索を行い，標準出力に解法の利点を引き出し，求解時間を大幅に短縮するこ

その結果を出力する．これをもとに，Sugar が復号化とが期待できる．

表1

既存 API IPASIR (C/C++)

関数名

動作

const char * ipasir signiture()

インクリメンタル SAT を用いるライブラリの名前とバージョンを返すvoid * ipasir init()

新しいソルバーのオブジェクトを作成し，そのポインタを返す

void ipasir release(void * solver)
void ipasir add(void * solver, int lit or zero)

ソルバーのリソースと確保した領域を解放する与えられたリテラルを現在の節に追加する．0 を与えるとその節を閉じる

void ipasir assume(void * solver, int lit)

仮説となるリテラルをソルバーに与える

int ipasir solve(void * solver)与えられた仮説の下で SAT 問題の求解を行い，sat なら

10，unsat なら 20，探索が中断されたら 0 を返す
int ipasir val(void * solver, int lit)

求解結果が sat である場合に，指定したリテラルの真偽値を返す

int ipasir failed(void * solver, int lit)

求解結果が unsat であった場合に，与えた仮説がその証明に用いられていれば 1，そうでなければ 0 を返す

void ipasir set terminate(void * solver, void * state,
int(* terminate)(void * state))

ソルバーに探索の終了要求を行うためのコールバック関数
をセットする3. 2 既存 API

前提として設計されており，Java からの利用は考慮

インクリメンタル SAT は注目度の高い技術であされていない．また，提供されている機能が少ないたり，多くのソルバーが独自のインターフェースによっ

めに，SAT ソルバーが持つ他の様々な機能を利用でてその機能を提供している．しかしながら，インターきない．加えて，処理がリテラル単位でしか行えない

フェースの仕様がそれぞれ異なるため，アプリケーなど機能そのものも低レベルである．

ションから利用する際の SAT ソルバーの切り替えやそこで，API の利便性を高めるため，既存 API の

各 SAT ソルバーのインクリメンタル SAT の性能比拡張を行うことを提案する．本稿では，この拡張した

較が難しかった．

API を提案 API と呼ぶ．提案 API の機能を提供す

国際的な SAT 競技会である SAT Race 2015 では新しい競技部門として Incremental Library Trackが導入された †2 ．Incremental Library Track の目的
は，多くの異なる SAT ソルバーに共通のインクリ
メンタル SAT インターフェースを構築し，性能を比る iSAT Library の設計方針は，以下の通りである．

• 既存 API の拡張
既存 API で提供される関数は，そのまま利用可
能である．

• 機能の高レベル化

較することである．これを実現するため，表 1 に示

既存 API より高度なレベルでの記述を可能にすす汎用的なインクリメンタル SAT API (IPASIR) がる．例えば，リテラル単位でなく節単位での処理

提案，公開された．以下，本稿ではこの API を既存を実現する．これにより，ユーザーはより忠実に

API と呼ぶ．

意図する処理の記述を行うことができ，コードの可読性，記述力が向上する．

3. 3 提案 API• Java および C/C++ 両方の API の提供

表 1 に示した既存 API は，インクリメンタル SAT

Java からの利用も対象とする．Java 用にはより解法を利用するための最低限の機能を提供している．

高度なクラスを用意し，API をラップして動作

しかしながら，この API は C/C++ からの利用をするようにする．

†2 http://baldur.iti.kit.edu/sat-race-2015/index.
php?cat=rules\#api

表2

提案 API (C/C++)

関数名

動作

int isat vars(void * solver)

ソルバーが保持する変数の個数を返す

void isat add clause(void * solver, int[] clause,

節をまとめてソルバーに追加する

int length)
結果が sat であった場合に，全ての変数に対する真偽値

int * isat model(void * solver)

割り当てを返す得られた解の構成を禁止する否定節をソルバーに追加すvoid isat add blocking clause(void * solver,る

int[] literals, int length)

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:

void isat freeze(void * solver, int literal)

指定したリテラルを簡単化の対象から除外する

int isat is eliminated(void * solver, int literal)

指定したリテラルが簡単化されているかをチェックする

int [][] cnf = ...
com . sun . jna . Pointer solver = ...
int maxLit = 0;
for ( int [] clause : cnf ) {for ( int lit : clause ) {ipasir_add ( solver , lit );maxLit = Math . max ( maxLit , Math . abs ( lit ));}ipasir_add ( solver ,0);}while ( ipasir_solve ( solver ) == 10) {/* output sol u tio n */for ( int i =1; i <= maxLit ; i ++) {int lit = ipasir_val ( solver , i );ipasir_add ( solver , - lit );}ipasir_add ( solver ,0);}

図1

既存 API を用いた解の列挙

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

int [][] cnf = ...
ISatSolver solver = ...
for ( int [] clause : cnf )solver . add_clause ( clause );while ( solver . solve ()) {solver . model ();/* output s o l u t i o n */solver . a d d _ b l o c k i n g _ c l a u s e ();}図2

提案 API を用いた解の列挙; Input Example
p cnf 3 4
1 2 3 0-1 -2 0
-1 -3 0-2 -3 0
図3

; Output Example
1 -2 -3-1 -2 3
-1 2 -3問題と出力の例

3. 4 iSAT Library の設計

れる解は，図 3 のようになる．以下で，既存 API に

提案 API で新たに提供する関数の一部を，表 2 によるプログラムの流れを説明する．1 行目，2 行目で示す．以下で，iSAT Library の設計方針を述べる．

それぞれ CNF と SAT ソルバーを与える．3 行目のAPI は C/C++ で記述し，Java から利用する際

変数 maxLit は，リテラルの番号のうち最大のもの，には，JNA (Java Native Access) を用いて API を

すなわち SAT ソルバーに追加された変数の数を表呼び出す．これにより，C/C++ と Java の両方か

す．4 行目から 10 行目が節の追加処理である．節中ら API を利用することが可能になる．Java 側には，の各リテラルに対して追加処理を行い (6 行目)，リテ

JNA で API を利用するためのインターフェースと，

ラル番号の更新を行う (7 行目)．全てのリテラルを追より高レベルなラッパークラスを作成する．

加し終えたら，0 を追加してその節が終了したことをAPI の使用例として，Java から既存 API，提案

SAT ソルバーに知らせる (9 行目)．これを全ての節

API のそれぞれを用いて解の列挙を行うプログラムに対して繰り返す．次に 11 行目から 18 行目で解のを図 1，2 に示す．なお図 2 では，提案 API のラッ列挙を行う．求解結果が SAT なら (11 行目)，解のパークラスのメソッドを利用している．入力と得ら表示を行った後に (12 行目)，得られた解の構成を禁

(2)

Sugar

提案

提案 API

API
既存

(C++)

(Java)API(1)

SAT Solver
Wrapper

JNA

iSAT Library

Class

Interface(C++ 用)iSugarSAT Solver

iSAT Library (Java 用)

図4

(3)

↑ API用モジュール

システム全体の構成

止する否定節を追加する (13〜16 行目)．このときも• 様々な高速 SAT ソルバーと密に結合できる．

否定節の最後に 0 を加える必要がある (17 行目)．

• COP，解列挙問題，CEGAR 解法による問題を

このように，既存 API を利用する場合には補助的

高速に求解可能である．

な変数の導入や，同じ記述の繰り返しなどが生じ，冗

本節では，提案システムの実現である iSugar の設計

長なコードになる．提案 API では，新たな変数などと実装について述べる．

を用いることなく同じ処理を 9 行で行える．また，各処理の内容も分かりやすくなっており，既存 API の

4. 1 設計

問題点を解決している．

iSugar では符号化した節を，ファイルを経由することなく iSAT Library の関数を通して直接 SAT ソル

3. 5 実装上の工夫

バーに与え，解も関数の戻り値として直接受け取る．

JNA による関数呼び出しにはマーシャリング (型SAT ソルバーは iSugar と同一のプロセスで動作し，変換) などの前処理があり，通常に比べて大きなオー

求解後も終了せずに情報を保持する．両者の間でファバーヘッドが存在する．そのため，関数の呼び出し

イルアクセスは行わず，節や解などの情報はすべて回数が多くなるとその処理時間が無視できなくなる．

整数や配列のデータとして受け渡しを行う．CSP のこのオーバーヘッドを調べるため，簡単な予備実験

読み込みや SAT 符号化・復号化などの処理は iSugarを行った．リテラル数が 10 の節 10,000,000 個に対しのメインプログラムから Sugar のメソッドを呼び出て，既存 API で節の追加処理を行ったところ，全て

すことで行う．

の節を追加するのに 260.53 秒かかった．そこで，複iSugar と SAT ソルバーの結合には，iSAT Library

数の節をまとめて SAT ソルバーに追加する関数をを利用する．C/C++ 側では各 SAT ソルバーに対作成した．一度に追加する節数を変えたところ，10

応する API 用のモジュールを設計する．これによっ個の場合で 1.65 秒，1000 個の場合で 0.25 秒となり，て，API を介していろいろな SAT ソルバーをプラオーバーヘッドが削減できた．この結果から，Javaから利用する場合には節をバッファリングして，一度グインできる．API 用モジュールのプログラムは短く，MiniSat 2.2†3 の場合で 100 行程度である．なお，に複数個を SAT ソルバーに追加するようにした．こ

SAT Race 2015 に提出されたソルバーなど，既存れらの工夫は，ラッパークラスで実装している．

API に対応しているものであれば，特別な作業を行うことなく iSugar との結合が可能である．

4 iSugar の設計と実装

以上から，システム全体の構成は図 4 のようになる．

2 節および 3 節を踏まえて，本稿では以下の 2 点を目的とし，インクリメンタル SAT 解法の利用によりこれを実現したインクリメンタル SAT 型制約ソルバーを提案する．

†3 http://minisat.se/MiniSat.html

4. 2 実装
ベースには Sugar 2.2.1，結合する高速 SAT ソル
バーには GlueMiniSat 2.2.5 [25](以下 GlueMiniSat) を選択した．実装内容は主として SAT ソルバーを利用するためのプログラムの実装と，各問題の求解を行うためのプログラムの実装に分けられる．以下でそれぞれについて具体的に述べる．

4. 2. 1 SAT ソルバーとの結合• Sugar のクラスやメソッドを利用し，与えた問
題ファイルを処理するためのメイン部分のプログ
ラムを作成した (図 4-(1))．

• Sugar において節をファイルに書き出す部分の処理を SAT ソルバーに直接追加する処理に変更するため，関連する Sugar のメソッドをオーバーライドした (図 4-(2))．

• GlueMiniSat の仕様に合わせて，API 用のモ
ジュール部分を実装した．(図 4-(3))．
これには，SAT Race 2015 が提供している，Min-

iSat 2.2 に対応する API 実装のプログラムを参考とした．

4. 2. 2 種々の問題への対応
2.2 節で取り上げた COP，解列挙問題，CEGARを用いた問題について，iSugar に実装した求解アル
ゴリズムを以下に示す．COP については，Sugar お
よび iSugar それぞれの求解手順を図を用いて説明する．解列挙問題，CEGAR を用いた問題については，

iSugar での手順のみを簡単に記す．
(COP)
ここでは，目的変数 v (l ≤ v ≤ u) を最小化する

COP を扱う．
目的変数の値の絞り込みの方法には，二分探索や線形探索などがある．インクリメンタル SAT では，sat の判定に比べて時間を要する unsat の判定回数

begin
1: 制約を SAT 符号化し SAT 問題 Ψ を生成
2: Ψ を ファイルに出力3: while Dom(v) が空でない do
4:
if Dom(v) のサイズが k 以上 then5:d := ⌊(l + u)/2⌋
6:
else
7:
d := u − 1
8:
end if9:v ≤ d を表す節をファイルに追加
10:
SAT ソルバーを起動して解く
11:
if sat then12:s := 求まった v の値
13:Dom(v) から s 以上の値を削除
14:
else
15:
Dom(v) から d 以下の値を削除
16:
end if
17: end while
18: s を最適値として出力
end
図5

Sugar による COP の求解アルゴリズム

begin
1: (iSugar の起動とともに SAT ソルバーが起動)
2: 制約を SAT 符号化し SAT 問題 Ψ を生成
3: Ψ を SAT ソルバーに追加
4: while Dom(v) が空でない do
5:
if Dom(v) のサイズが k 以上 then6:d := ⌊(l + u)/2⌋
7:
else
8:
d := u − 1
9:end if10:
ipasir assume(solver, (v ≤ d を表すリテラル))
11:
ipasir solve(solver)
12:
if sat then13:s := 求まった v の値
14:Dom(v) から s 以上の値を削除
15:
ipasir add(solver, (v ≤ s を表すリテラル))
16:
else
17:
Dom(v) から d 以下の値を削除
18:
ipasir add(solver, (v > d を表すリテラル))
19:
end if
20: end while
21: s を最適値として出力
end
図6

iSugar による COP の求解アルゴリズム

は極力少ないほうがよい．二分探索では多くの場合に少ない探索回数で解が求まるが，最適値未満の範

そこで iSugar では，はじめは二分探索を行い，ド囲での探索を 2 回以上行うことがあり，その場合にメインの幅があるしきい値 k 以下となるところから

は unsat を同じ回数判定しなければならない．一方

線形探索に切り替える混合探索を採用した．

で，線形探索では最適値未満の範囲での探索が最後の混合探索による Sugar と iSugar の COP 求解ア

1 回だけなので unsat の判定は 1 回でよいが，探索

ルゴリズムを図 5，6 に示す．iSugar ではループ内で回数が多くなってしまう．

SAT ソルバーの起動がなく，学習節を保持したまま

表3

問題

Sugar

iSugar問題

j6-per0-0

283.3388.81

j6-per0-1

111.56

1.57

j6-per0-2

19.86

j6-per10-0
j6-per10-1

OSS の実験結果 (単位：秒)Sugar

iSugarj7-per0-0

69041.28

29946.84

j7-per0-1

228.09

43.20

4.95

j7-per0-2

156.18

24.64

94.91

3.25

j7-per10-0

359.69

94.63

1.87

j7-per10-1

287.05j6-per10-2

115.012.37

j7-per10-2

j6-per20-0

106.401.97

j7-per20-0

j6-per20-1

124.13

2.12

j6-per20-2

170.83

2.39

問題

Sugar

iSugarj8-per0-1

43397.22

18574.38

j8-per0-2

204.76126.5140.98

j8-per10-0

1011.20296.533.67

j8-per10-1

5852.87386.66976.82367.81j8-per10-2

5432.232859.95

173.051.28

j8-per20-0

409.46

5.19

j7-per20-1

348.0110.85

j8-per20-1

442.773.45

j7-per20-2

287.4921.62

j8-per20-2

431.00

4.94

2 回目以降の探索を行う．

表4

N-クイーン問題の実験結果 (単位：秒)(解列挙問題)N

1. 問題を読み込み，SAT 符号化した節を SAT ソ

4

2

0.50

0.30

5

10

0.49

0.49

2. SAT 問題を解き．unsat なら終了する．

6

4

0.51

0.52

3. 得られた解を禁止する否定節を SAT ソルバー

7

40

1.12

0.50

8

92

1.66

0.49

9

352

7.14

0.90

10

724

52.70

2.42
13.31

ルバーに追加する．

に追加して 2. ヘ戻る．

(CEGAR を用いた問題)
1. 元の問題から緩和問題を生成し，SAT 符号化した節を SAT ソルバーに追加する．

2. SAT 問題を解き．unsat なら終了する．

解の総数

Sugar

iSugar11

2680(T.O.)

1214200(T.O.)

62.90

13

73712

(T.O.)(T.O.)

3. 得られた解が元の問題の制約を満たしているかどうかを確認する．満たしている場合，それを解として終了する．

4. その解を禁止する否定節を追加して 2. へ戻る．

法を切り替える k の値は 100 とした．
実験の結果，26 問全てにおいて求解時間の短縮に成功した．26 問の速度比の幾何平均は 16.41 となり，

iSugar は Sugar の 16 倍程度高速であることが分かっ

5 性能評価た．これより，OSS ではインクリメンタル SAT 解

実装した iSugar を用いて性能評価の実験を行った．

法が有効であることが示された．

CPU 時間は Linux Ubuntu 14.04(Xeon 3.00GHz,
メモリ 16GB) 上で計測した．

5. 2 解列挙に対する評価
解列挙問題として N-クイーン問題を扱う．Sugar

5. 1 COP に対する評価

は解列挙に対応していないため，インクリメンタル

COP としてオープンショップスケジューリング問

SAT 解法を用いずに解く機能を iSugar に実装した．

題 (OSS; Open Shop Scheduling Problem) を扱う．

具体的には SAT ソルバーを別プロセスとして呼び出

OSS のベンチマーク問題の中でも，j* 問題は Sugar

して問題を解き，解を得るたびに CNF ファイルにそが解くまで未解決であった問題を含んでおり，求解困の解を除去する制約を追加して再度問題を解く手続き

難な問題として知られている．その中から特に難解なを繰り返すことで解列挙を行う．本稿では，このシス

j6，j7，j8 の 26 問について，Sugar と iSugar でそれテムを Sugar と表記する．両システムにおける CPU

ぞれ求解した結果の CPU 時間を表 3 に示す．探索手

時間を比較したものを表 4 に示す．問題のサイズは

4 ≤ N ≤ 13，制限時間は 3600 秒とした．(T.O.) は

表5

HCP の実験結果

制限時間内に求解できなかったことを表す．
表 4 の通り，解の総数が大きくなるにつれて iSugar

頂点数

問題数

Sugar

iSugar

1〜100

26

26

26

101〜500

60

41

52

501〜

33

4

26

合計

119

71

104

の解を発見した (iSugar は他に解がないことを判定で平均反復回数

114.00

23.00

きず終了した)．この結果から，解が多いほどインク

単位求解時間平均 (秒)

0.28

0.27

の求解時間が Sugar に比べて小さくなっていくことがわかり，N = 10 で 21 倍，N = 11 で 270 倍以上の高速化に成功した．また，N = 13 に関しては，3600
秒以内に Sugar が 6303 個，iSugar が 73712 個全て

リメンタル SAT 解法の利点が引き出されていることが確認できた．
100

CEGAR を用いる問題としてハミルトン閉路問題(HCP) を扱う．CEGAR による HCP の定式化および符号化には論文 [16] の方法を用いた．iSugar で解く際には得られた解に部分閉路が存在するかどうかを調べる必要があるため，頂点や辺などのグラフの情

iSugar (sec)

5. 3 CEGAR に対する評価

10

1

0.1

報を保持し，閉路の抽出などを行うクラスを新たに作成した．また Sugar はこの解法にも対応していない

0.01
0.01

ため，解列挙と同様に SAT ソルバーと疎に結合して動作する機能を iSugar に実装した．
ベンチマーク問題には COLOR04†4 の 119 問を用

図7

0.1

1

10

Sugar (sec)100

両方が解けた問題の求解時間比較

いた．問題をグラフの頂点数により分類し，それぞれな原因については調査を行う必要がある．また，両方の問題数および Sugar，iSugar が解けた問題数を表 5で解けた 71 問について，両ソルバーでの求解時間のに示す．制限時間は 500 秒とした．反復回数は SAT

スキャッタープロットを図 7 に示す．図 7 より，規模ソルバーが解を探索した回数，単位求解時間は求解が大きい問題ほど速度比の改善がみられ，iSugar がに要した CPU 時間を反復回数で割ったものであり，大幅に求解性能を向上していることが分かる．なお，

平均は各ソルバーが解けた問題に対する値である．な

71 問での iSugar の平均反復回数は 14.00，単位求解

お，各問題についての詳細な結果は付録にまとめる．

時間平均は 0.01 秒であった．

表 5 の通り，全 119 問のうち Sugar が解けたのは

これより，インクリメンタル SAT 解法の利用によ

71 問であったのに対し，iSugar では 104 問の求解にり各探索回の求解時間を平均的に短縮でき，大規模な成功した．差分の 33 問は全て，Sugar で解けず iSugar

問題に対する性能が向上できたことが示された．

で解けた問題である．Sugar と比べて，iSugar は頂点数が多い問題でもよく解けていることが分かる．ま6 まとめと今後の課題

た反復回数では iSugar が Sugar の約 1/5 になってお

本稿では，SAT Race 2015 で公開されたインクリ

り，より早く解を発見できた．反復回数の減少は学習

メンタル SAT API をより高機能化し，Java アプリ

節を保持することによるものだと考えられるが，正確ケーションからの利用に対応するよう拡張した API
として，iSAT Library の提案を行った．また，SAT†4 http://mat.gsia.cmu.edu/COLOR04/

ソルバーを繰り返し起動することなく，制約最適化

問題や解列挙問題を効率的に解くことを目的として，
インクリメンタル SAT 解法が利用可能な SAT 型
制約ソルバーを提案した．提案システムとして iSAT

Library に対応した iSugar を設計・実装し，インク
リメンタル SAT 解法が有効であると考えられる問題
群に対して既存のシステムとの性能比較を行い，以下の結果を得た．

• OSS
26 問全てで求解時間を短縮し，Sugar と比べ平均で 16 倍高速に求解できた．

• N-クイーンの解列挙
N = 10 で 21 倍，N = 11 で 270 倍以上の高速化に成功した．

• HCP の CEGAR 解法
119 問中 104 問を解き，Sugar より 33 問多く求解できた．
以上から，インクリメンタル SAT 解法を利用することにより全体的な性能改善が達成でき，提案したシス
テムの有用性が示された．
今後の研究課題には，求解方法の見直しによる性能の向上， API のさらなる拡張による機能の充実などが挙げられる．提案 API で追加する機能の案としては，極小の充足不能な節集合の抽出 [8] [15] や，擬似
ブール制約の取り扱い [7] [19]，ソルバーの並列化などが考えられる．

参 考 文 献[ 1 ] Barták, R.: On-line Guide to Constraint Programming, http://kti.ms.mff.cuni.cz/~bartak/
constraints/, 1998.
[ 2 ] Biere, A., Cimatti, A., Clarke, E. M., and Zhu,
Y.: Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on
Tools and Algorithms for Construction and Analysis of Systems (TACAS 1999), LNCS 1579, 1999,
pp. 193–207.
[ 3 ] Biere, A., Heule, M., van Maaren, H., andWalsh, T.(eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications(FAIA), Vol. 185, IOS Press, 2009.
[ 4 ] Bordeaux, L., Hamadi, Y., and Zhang, L.:
Propositional Satisfiability and Constraint Programming: A Comparative Survey, ACM Computing Surveys, Vol. 38, No. 4(2006).
[ 5 ] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y.,

and Veith, H.: Counterexample-Guided Abstraction
Refinement, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL,
USA, July 15-19, 2000, Proceedings, Emerson,
E. A. and Sistla, A. P.(eds.), Lecture Notes in Computer Science, Vol. 1855, Springer, 2000, pp. 154–
169.
[ 6 ] Eén, N. and Sörensson, N.: Temporal Induction
by Incremental SAT Solving, Electronic Notes in
Theoretical Computer Science, Vol. 89, No. 4(2003).
[ 7 ] Eén, N. and Sörensson, N.: Translating PseudoBoolean Constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation, Vol. 2,
No. 1-4(2006), pp. 1–26.
[ 8 ] Liﬃton, M. H. and Sakallah, K. A.: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints, J. Autom. Reasoning, Vol. 40,
No. 1(2008), pp. 1–33.
[ 9 ] Marques-Silva, J. P. and Sakallah, K. A.:
GRASP: A Search Algorithm for Propositional
Satisfiability, IEEE Transactions on Computers,Vol. 48, No. 5(1999), pp. 506–521.
[10] Metodi, A. and Codish, M.: Compiling finite domain constraints to SAT with BEE, TPLP, Vol. 12,
No. 4-5(2012), pp. 465–483.
[11] 鍋島英知: SAT によるプランニングとスケジューリ
ング, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 114–
121.
[12] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 68–76.
[13] Nabeshima, H., Soh, T., Inoue, K., andIwanuma, K.: Lemma Reusing for SAT based
Planning and Scheduling, Proceedings of the International Conference on Automated Planning and
Scheduling 2006 (ICAPS 2006), 2006, pp. 103–112.
[14] Rossi, F., Beek, P. v., and Walsh, T.: Handbookof Constraint Programming (Foundations of Artificial Intelligence), Elsevier Science Inc., New York,NY, USA, 2006.
[15] Ryvchin, V. and Strichman, O.: Faster Extraction of High-Level Minimal Unsatisfiable Cores,
Theory and Applications of Satisfiability Testing SAT 2011 - 14th International Conference, SAT
2011, Ann Arbor, MI, USA, June 19-22, 2011.
Proceedings, Sakallah, K. A. and Simon, L.(eds.),
Lecture Notes in Computer Science, Vol. 6695,
Springer, 2011, pp. 174–187.
[16] Soh, T., Le Berre, D., Roussel, S., Banbara, M.,
and Tamura, N.: Incremental SAT-Based Methodwith Native Boolean Cardinality Handling for the
Hamiltonian Cycle Problem, Logics in Artificial Intelligence, Springer International Publishing, 2014,
pp. 684–693.
[17] Soh, T., Tamura, N., and Banbara, M.: Scarab:
A Rapid Prototyping Tool for SAT-Based Constraint Programming Systems, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th
International Conference, Helsinki, Finland, July

8-12, 2013. Proceedings, Järvisalo, M. and Gelder,
A. V.(eds.), Lecture Notes in Computer Science,Vol. 7962, Springer, 2013, pp. 429–436.
[18] Stojadinovic, M. and Maric, F.: meSAT: multiple encodings of CSP to SAT, Constraints, Vol. 19,
No. 4(2014), pp. 380–403.
[19] Tamura, N., Banbara, M., and Soh, T.: Compiling Pseudo-Boolean Constraints to SAT with Order
Encoding, 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, Herndon,
VA, USA, November 4-6, 2013, IEEE Computer
Society, 2013, pp. 1020–1027.
[20] 田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知, 井上克巳: ショップ・スケジューリング問題の SAT 変換
による解法, スケジューリング・シンポジウム 2007 講
演論文集, 2007, pp. 97–102.
[21] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[22] Tamura, N., Tanjo, T., and Banbara, M.: System Description of a SAT-based CSP Solver Sugar,
Proceedings of the 3rd International CSP Solver

Competition, 2008, pp. 71–75.
[23] 田村直之, 丹生智也, 番原睦則: 制約最適化問題とSAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010),
pp. 77–85.
[24] Tanjo, T., Tamura, N., and Banbara, M.: Azucar: A SAT-Based CSP Solver Using Compact Order Encoding, Theory and Applications of Satisfiability Testing – SAT 2012, Cimatti, A. and Sebastiani, R.(eds.), Lecture Notes in Computer Science, Vol. 7317, Springer Berlin Heidelberg, 2012,
pp. 456–462.
[25] 鍋島英知, 岩沼宏治, 井上克巳: GlueMiniSat 2.2.5:
単位伝搬を促す学習節の積極的獲得戦略に基づく高速
SAT ソルバー, コンピュータ ソフトウェア, Vol. 29,
No. 4(2012), pp. 4 146–4 160.
[26] 田村直之, 丹生智也, 番原睦則: SAT 変換に基づく
制約ソルバーとその性能評価, コンピュータ ソフトウェ
ア, Vol. 27, No. 4(2010), pp. 183–196.

A HCP の実験結果
HCP の実験結果詳細を表 6 に示す．

表6

HCP の実験結果 (単位：秒)Instance

Sugar

iSugar

Instance

Sugar

iSugar

Instance

Sugar

iSugar

1-FullIns 3

0.93

0.75

DSJC500.1

268.939.15

mulsol.i.3(T.O.)(T.O.)

1-FullIns 4

10.74

1.52

DSJC500.5(T.O.)

24.79

mulsol.i.4(T.O.)(T.O.)

1-FullIns 5(T.O.)

6.23

DSJC500.9(T.O.)

46.48

mulsol.i.5(T.O.)(T.O.)

1-Insertions 4

1.44

1.02

DSJR500.1(T.O.)

4.29

myciel3

0.45

0.28

1-Insertions 5

155.88

3.01

DSJR500.1c(T.O.)

48.85

myciel4

0.74

0.48

1-Insertions 6(T.O.)

74.89

DSJR500.5(T.O.)

24.99

myciel5

2.32

1.02

2-FullIns 3

0.03

0.79

fpsol2.i.1(T.O.)

8.33

myciel6

8.31

2.36

2-FullIns 4

142.51

3.81

fpsol2.i.2(T.O.)(T.O.)

myciel7120.52

3.79

2-FullIns 5(T.O.)

135.47fpsol2.i.3(T.O.)(T.O.)

qg.order100(T.O.)(T.O.)

2-Insertions 3

0.66

0.47

games120

15.22

1.56

qg.order30(T.O.)

13.55

2-Insertions 4

10.74

1.81

homer

0.60

0.71

qg.order40(T.O.)

30.28

2-Insertions 5(T.O.)

24.67

huck

0.26

0.28

qg.order60(T.O.)

122.553-FullIns 3

4.95

1.16

inithx.i.1(T.O.)(T.O.)

queen10 10

10.62

3.76

3-FullIns 4(T.O.)

4.25

inithx.i.2(T.O.)(T.O.)

queen11 11

7.12

3.67

3-FullIns 5(T.O.)(T.O.)

inithx.i.3(T.O.)(T.O.)

queen12 12

12.70

3.80

3-Insertions 3

0.66

0.67

jean

0.25

0.27

queen13 13

58.44

4.46

3-Insertions 4

47.59

3.32

latin square 10(T.O.)

136.05queen14 14

48.78

4.13

3-Insertions 5(T.O.)(T.O.)

le450 15a

36.43

7.08

queen15 15

83.54

5.62

4-FullIns 3

3.49

1.60

le450 15b

1.02

0.96

queen16 16

45.96

6.57

4-FullIns 4(T.O.)

16.00

le450 15c

397.81

10.18

queen5 5

0.76

0.77

4-FullIns 5(T.O.)(T.O.)

le450 15d

(T.O.)

9.93

queen6 6

1.45

1.15

4-Insertions 3

1.03

0.78

le450 25a

231.74

7.09

queen7 7

3.44

1.52

4-Insertions 4(T.O.)

15.20

le450 25b153.24

7.29

queen8 12

6.35

3.36

5-FullIns 3

20.21

2.50

le450 25c

358.7910.05

queen8 8

4.11

2.51

5-FullIns 4(T.O.)

124.32le450 25d192.61

10.42

queen9 9

3.98

2.97

abb313GPIA(T.O.)

22.66

le450 5a

18.68

5.73

school1

0.85

0.84

anna

0.25

0.29

le450 5b

24.66

5.97

school1 nsh

0.89

0.88

ash331GPIA

0.63

0.70

le450 5c133.36

7.59

wap01a(T.O.)

54.86

ash608GPIA

1.19

1.17

le450 5d

32.94

7.72

wap02a(T.O.)

58.37

ash958GPIA

1.57

2.97

miles1000

24.25

4.19

wap03a(T.O.)

167.95

david

0.25

0.30

miles1500

66.24

5.27

wap04a(T.O.)

179.07DSJC1000.1(T.O.)

20.91

miles250

0.26

0.27

wap05a(T.O.)

19.12

DSJC1000.5(T.O.)

104.70miles500

24.90

3.78

wap06a(T.O.)

20.26

DSJC1000.9(T.O.)

360.99miles750

376.393.73

wap07a(T.O.)

42.26

DSJC125.1

3.23

2.11

mug100 1

1.06

0.75

wap08a(T.O.)

46.10

DSJC125.5

16.62

3.93

mug100 25

1.05

0.78

will199GPIA(T.O.)

7.05

DSJC125.9

140.486.55

mug88 1

1.32

0.79

zeroin.i.1

57.97

4.68

DSJC250.1

52.47

4.28

mug88 25

0.97

0.76

zeroin.i.2(T.O.)(T.O.)

zeroin.i.3(T.O.)(T.O.)DSJC250.5

201.999.58

mulsol.i.1

42.20

3.90

DSJC250.9(T.O.)

13.66

mulsol.i.2(T.O.)(T.O.)