CDCLソルバーにおける学習節の深さに基づく節管理戦略

CDCL

ソルバーにおける学習節の深さに基づく節管理戦略

A Clause Management Strategy based on the Depth of Learnt

Clauses for CDCL Solvers

横前菜々子

1∗

鍋島英知

2

Nanako Yokomae

1

Hidetomo Nabeshima

2

1

_{山梨大学工学部コンピュータ・メディア工学科情報メディアコース}

1

_{Information Media Course, Department of Computer Science and Media Engineering,}

Faculty of Engineering, University of Yamanashi

2

_{山梨大学大学院医学工学総合研究部}

2

_{Department of Research Interdisciplinary Graduate School of Medicine and Engineering,}

University of Yamanashi

Abstract: In this paper, we propose a new clause management strategy based on the depth of learnt clauses for CDCL solvers. A CDCL solver derives many learnt clauses from conflicts occurred in the search process. These learnt clauses are useful to prevent similar conflicts, but they are periodically reduced to avoid memory overflow and decreasing the speed of unit propagation. Hence, an evaluation criteria of learnt clauses is important for CDCL solvers. In this study, we propose a new evaluation criteria based on the depth of learnt clauses. Each learnt clause has the depth in the derivation tree. Our approach holds (1) learnt clauses which may become bottleneck, that is, there is no other clauses at the depth, and (2) learnt clauses at deepest part of the tree. The experimental results show that our criteria can help to identify useful learnt clauses compared with existing criteria used in CDCL solvers.

1

はじめに

充足可能性判定問題 (SAT 問題) は，与えられた命題 論理式を満たす変数割り当てが存在するか否かを判定 する問題で，Cook[1] により初めて NP 完全性が証明さ れた問題である．SAT 問題を解くソフトウェアを SAT ソルバーといい，近年，SAT ソルバーは飛躍的に性能 が向上している．高速な SAT ソルバーはハードウェア・ ソフトウェア検証，スケジューリング，プランニング といった様々な分野で利用されている． 近年の高速 SAT ソルバーの多くは，矛盾からの節 学習 (conflict-driven clause learning；CDCL)[3][4] を 導入した SAT ソルバーである．この SAT ソルバーを， CDCLソルバーと呼ぶ．CDCL ソルバーは，SAT 問題 の求解過程で学習節を導出する．その導出過程は有向 非巡回グラフ (DAG) で表される．よって，各学習節に は，その学習節が導出された深さを与えることができ る．学習節の中には，深さに強く関連した重要な節が ∗_{連絡先：山梨大学工学部コンピュータ・メディア工学科情報メ} ディアコース 〒 400 - 8511 山梨県甲府市武田 4 - 3 - 11 E-mail: yokomae@nabelab.org 存在している． 学習節は，SAT 問題の求解過程で数多く導出され， CDCLソルバーはそれらの節を保持する．学習節は必 ず矛盾に至る割り当てを回避することができるため，探 索の効率化を図ることができる．その一方で学習節の 増大が，単位伝搬速度の低下やメモリ圧迫の原因とな るため，CDCL ソルバーでは通常，今後の探索に役に 立つであろう学習節を，その学習節の節長やリテラル ブロック距離 (literal blocks distance；LBD)[10] とい う評価尺度を用いて評価をし，削除と保持を行う．こ れらの評価尺度は，学習節の深さについて全く考慮し ていない節管理戦略である．本稿では，既存の節管理 戦略に加え，学習節の深さを評価尺度として加えた節 管理戦略を提案する． 本稿の構成は以下の通りである．まず，2 節において SAT問題と CDCL ソルバーについて説明する．3 節で は学習節の深さについて解説する．4 節において既存の 節戦略の概説と提案手法について説明し，5 節で提案 手法の評価実験を行う．6 節では調査・考察を述べる． 7節でまとめと今後の課題を述べる． 人工知能学会研究会資料 SIG-FPAI-B404-17

2

SAT

問題と

CDCL

ソルバー

命題論理式の充足可能性判定 (Bollean (or proposi-tional) satisfiability (testing) ; SAT)は，与えられた 命題論理式を真にする変数割り当てが存在するか否か を判定する問題であり，通常，連言標準形 (conjunctive normal form ; CNF)で表される．命題変数 a または その否定¬a をリテラルと呼び，前者を正リテラル，後 者を負リテラルという．リテラルを論理和 (∨) で結ん だものを節，節を論理積 (∧) で結んだものを CNF 式 と呼ぶ．ひとつの節中のリテラルの個数を節長といい， 節長が 0，すなわち，節にひとつもリテラルを含まな い節を空節と呼ぶ．節長が 1 の節，または，節中に未 割り当てのリテラルが 1 つで，残りのリテラルには偽 が割り当てられている節を単位節という．与えられた CNF式が充足可能の場合，CNF 式中の全ての節が充 足する変数割り当てが存在し，充足不能の場合は，そ のような変数割り当てが存在しない．SAT 問題を解く ソフトウェアを SAT ソルバーと呼び，与えられた問題 が充足可能か充足不能かを判定する． 近年の高速 SAT ソルバーの多くは，DPLL アルゴリ ズム [2] に，矛盾からの節学習 (conflict-driven clause learning；CDCL) を導入している．このような SAT ソルバーを CDCL ソルバーと呼ぶ．以下に，DPLL ア ルゴリズムと CDCL アルゴリズムを簡単に説明する． DPLLアルゴリズムは，与えられた命題論理式に対 して充足可能 (SAT) または充足不能 (UNSAT) と判定 するまで以下の手順を繰り返し行う． 1. 単位節を探し，単位節が充足するような変数割り 当てを行う (単位伝播)． 2. 単位節が見つからない場合，ある変数決定ヒュー リスティクスに基づいて変数を選択 (決定変数) し，真または偽を割り当てる．決定変数の数を決 定レベルという． 3. ある真偽値割り当てのもとで空節が発生した場合 (矛盾)，矛盾発生時の決定レベルでの値割り当て を取り消し，決定変数の真偽値を反転させる．反 転済みの場合，さらに 1 つ前の決定レベルに戻り 同様の処理を行う (バックトラック)． 以上の手順を繰り返す過程で，与えられた問題のすべ ての節が充足するような変数割り当てを発見した場合， 充足可能となり探索を終了する．決定レベル 0 におい て矛盾が起きた場合，または，決定レベル 0 へのバッ クトラックが生じた場合は，与えられた問題は充足不 能と判定する． CDCLアルゴリズムは矛盾が起きた際 (手順 3) に矛 盾の導出に関わった節を解析し，同様の矛盾の発生を 防ぐための節を学習する．矛盾解析によって獲得され る節を学習節と呼ぶ．以下の例を用いながら説明する． F = C1∧ C2∧ C3∧ C4 C1= (¬c ∨ e ∨ ¬f) C2= (b∨ f) C3= (¬a ∨ c) C4= (¬a ∨ ¬b ∨ ¬d)

ここでは，a∼f はリテラルである．a，d には真，e に 偽が割り当てられているとき，f で矛盾が発生する．す なわち，(a∧ d ∧ ¬e) のとき必ず矛盾が起きることにな る．この原因の否定の節 (¬a ∨ ¬d ∨ e) を獲得し元問題 に追加することで，今後の探索において同様の矛盾を 防ぐことができる．そのため，学習節は探索空間の枝 刈りをし，探索の効率化を図ることが可能である．ま た，学習節は矛盾した節に，その矛盾に関わった節 (矛 盾した節の各リテラルを偽にするような単位伝播を生 んだ節) を順次線形融合することで導出することがで きる．融合法による導出過程を図 1(a) に示す．矛盾し た節 C1とその矛盾に関わった節 C2∼C4とし，C1に 対して C2∼C4を順次線形融合させていくことで学習 節を導出していく．このとき CDCL ソルバーでは，C1 と C2より融合節 C5(¬c ∨ e ∨ b) を求め，C5と C3より 融合節 C6(¬a ∨ e ∨ b) を求め，最後に C6と C4より融 合節 C7(¬a ∨ ¬d ∨ e) を求め，C7を学習節をして獲得 する．学習節を追加した後，ある決定レベルまでバッ クジャンプし探索を進めるていく． 学習節は探索空間の枝刈りを行う有用な節であるが， 学習節は探索過程で爆発的に増える．そのため，単位伝 播の速度低下をもたらす．実際，SAT 問題求解過程に おいて 70%∼90%のコストを占める処理は単位伝播 [7] であるため，単位伝播の速度低下は CDCL ソルバーの 求解性能低下につながる．また，学習節の節長は探索 が進むにつれ長くなる傾向があり，すべての学習節を 保持することはメモリの面から考えて困難である．そ のため，通常 CDCL ソルバーは節管理戦略基づいて学 習節を削減している．また，与えられた問題が充足不 能である場合，空節が導かれ探索を終了する． 近年の CDCL ソルバーには上記で述べた技術以外に も，リスタート戦略や監視リテラル，変数選択ヒュー リスティクスなど様々な技術が実装され，より高速な 求解を追求している．

3

学習節の深さ

学習節は，矛盾した節に対して，その矛盾に関わっ た節を順次線形融合することで導出することができる．

C4 C3 C2   C1 C6 C5 C7 (a)融合法による学習節の導出 過程 C4 C3 C2 C1 C7 (b)節含意グラフ 図 1: 学習節の導出過程 CNF式 学習節 深さ = 0 深さ = 1 深さ = 2 元節 学習節 深さ = 3 図 2: 学習節の導出過程と深さ 本稿では，融合法によって導出された学習節を節含意 グラフ [5] によって表す．節含意グラフでは，学習節を 導く過程で導出された途中の融合節を省略して表記す る．図 1(a) を節含意グラフで示したグラフが，図 1(b) である． 節含意グラフは有向非巡回グラフ (DAG) で表され， 各節には深さを付けることができる．与えられた CNF 式の節 (元節) を深さ 0 とし，元節 (深さ 0) から導出さ れた学習節は深さ 1，深さ 0 と深さ 1 から導出された学 習節を深さ 2 と深さを各節に付ける．このように，導 出した学習節の深さは，親節の深さの最大値に 1 を足 したものとなる．図 2 は，学習節の導出過程と深さを 図で示した例である． 学習節の深さという観点から見たときに現れる SAT 問題求解の特性について 2 つ紹介する．前者は既知の 結果であり，後者は本稿で新たに実証した結果である． 求解のボトルネック [6] Katsirelosらは，SAT 問題の求解過程においてし ばしばボトルネックとなる学習節が現れているこ とを実証している．ボトルネックとは，ある学習 節が導出されなければ，ある学習節から導出され る多くの学習節を導くことができない節のこと である．ボトルネックとなる節の深さでは他の節 がほとんど存在せず，かつ，それ以降の深さには 非常に多数の節が存在するという特徴を持つ．実 際，並列 SAT ソルバーでは，ボトルネックとな る節の存在が並列化の障壁となっている． 空節の深さ 与えられた問題が充足不能の場合，空節が学習 節として最後に導出され，探索を終了する．SAT 2014競技会の Application 部門の問題 300 問に 対して空節の深さを調査したところ，空節は学習 節の深さの中でも最深値に近いところで出現して いることが分かった． ボトルネックとなる節数と空節の深さに関する実証結 果を示す．使用した SAT ソルバーは，glueminisat2.2.6-ucore[8]を改良し各節に深さを付けたもので，使用問題 は SAT 2014 競技会の Application 部門の問題 300 問， 実験は 1 問当たり 5000 秒，CPU Intel(R) Xeon(R) E3-1230 V2 3.30GHz，メモリ 8GB の実験環境で行った． 図 3 は，blocks-blocks-37-1.130-NOTKNOWN.cnf と いう問題の求解過程で導出された学習節について，横 軸を深さ，縦軸をその深さにおける節数としたグラフ である．深さ 0 の節数は原問題に含まれる節（元節）の 数である．実線は元節と求解で導かれた学習節 (全節)， 点線は空節を導くために必要となった節 (反駁) を表す． 点線の線の最も深い節は空節である．図 3 より，深さ における節数が少ない深さの後に，多くの節が導かれ ていることが分かる．さらに，実線と点線の一番深い 点を比べると，空節は全学習節の深さの中でも深いと ころに存在している． 表 1 は，実証実験において 5000 秒以内に求解でき た 187 問 (SAT90 問，UNSAT97 問) における導出木 中のボトルネックとなる節の割合を示した結果である． SATな問題と UNSAT な問題のボトルネックの節は全 学習節の 0.94% ，すなわち，約 1% ほどである．また， SATな問題と UNSAT な問題でボトルネックの割合に 違いがあり，UNSAT な問題のほうがボトルネックの 節が多いことが分かる． 表 2 は，5000 秒以内に求解できた USAT な問題 99 問におけるの空節の深さの平均値と，学習節の最大深 さの平均値である．全学習節における空節の深さの割 合を調べた結果，95.66%であり，空節は深いところに 存在していることが分かった．

4

節管理戦略

CDCLソルバーでは学習節を節管理戦略に基づいて 定期的に削減している．本節では，既存の節管理戦略 について説明した後，本研究で提案する節管理戦略に ついて述べる．

1 10 100 1000 10000 100000 1e+06 1e+07 0 500 1000 1500 2000 2500 •–ª fl ¤ fl ا 深さ 深 節 数 全節 反駁 図 3: 深さにおける節数 表 1: ボトルネックの割合 SATな問題 + UNSAT な問題 0.94% SATな問題 0.41% UNSATな問題 1.39% 表 2: 空節の深さ 空節の深さ (平均) 71442 学習節の最大深さ (平均) 74685 空節の深さ (平均) 学習節の最大深さ (平均)× 100 95.66%

4.1

既存の節管理戦略

学習節を削減する際，今後の求解に役に立つ学習節 は保持し，役に立たない節は削除することによって探 索の効率を高めたい．そこで，学習節を評価し，学習 節の保持や削除を行う．学習節の著名な評価尺度とし て，活性度 (activity) や節長，リテラルブロック距離 (literal blocks distance；LBD)[10] などがある．

代表的な CDCL ソルバーである MiniSat[9] では，学 習節の評価尺度として活性度を使用している．活性度 は，学習節が導出された時，または，矛盾の原因とし て使用された時に活性度を上げる．活性度が高ければ 高いほど，矛盾発生に関係した節となる．また，ある 活性度が閾値を越えると，すべての活性度を定数で割 ることにより，矛盾に関与する節の活性度が高くなる． 学習節の削減の際は，活性度の低い学習節を削除し，高 い学習節は保持する． 節長による学習節の評価は，最も基本的な学習節の 評価尺度である．探索過程で学習節は，学習節中に含 まれる全てのリテラルに偽が割り当てることを防ぐが， 節長は短ければ短いほど制約が強い節となる．節長が 2 以下の節は特に強い制約であるため，CDCL ソルバー では今後の探索に重要な節と評価し保持する． LBDによる学習節の評価は，Audemard らによって 提案された学習節の評価尺度のひとつで，学習節中の リテラルをブロックごとに分ける．ブロックとは，決 定レベルごとに割り当てられたリテラル群である．変 数 a∼h で構成された節を用いて例を示す． ( a∨ ¬ b ∨ c ∨ d ∨ ¬ e ∨ f ∨ ¬ g ∨ h ) 四角で囲ったリテラル群は，ブロックで分けられている ことを示している．この例の場合，3 つのブロックに分 かれており，3 つの決定レベルでそれぞれ値が割り当て られたということを示している．同一のブロック内のリ テラルは，今後の探索においてもある決定レベルで同時 に割り当てられることが期待できるため，LBD の評価 尺度ではブロックをあたかも 1 つのリテラルとして見な す．よって，節長が大きい学習節でも LBD が小さい節 ならば，制約が強い節と考え保持する．この例の場合， 節長は 8 であるが，LBD は 3 となる．Audemard らは， LBDの小さな節を保持する節管理戦略が，CDCL ソル バーの性能を大きく向上させることを示した．

4.2

提案手法

既存の節管理戦略では，学習節の深さについて考慮 していない．学習節の深さは，ボトルネックとなる節 や空節と強く関連しており，節の管理において有益な 情報になりうる．そこで，既存の節管理戦略に加えて 学習節の深さを節の評価尺度を取り入れた節管理戦略 を 2 つ提案する． 4.2.1 ボトルネックとなる節候補の保持戦略 学習節の深さに関連する特性のひとつとして，求解 のボトルネックとなる節の存在を挙げた．ボトルネッ クの節は，その節から多くの学習節を導出するため重 要な節であると考えられる．もしボトルネックの節を 削除すると，その節から導出される学習節を導くこと ができなくなり，さらに，削除したボトルネックの節 以降に導かれる学習節を導くためには，ボトルネック の節の再構築が必要となるため探索効率の低下をもた らす可能性がある．そこで，学習節を削除する際，ボト ルネックの学習節は削除せず保持する．しかし，探索 過程である節がボトルネックかどうかを判断し保持す ることは困難である．なぜなら，学習節削減の際，深 さにおける節数が少ない節を保持しても，今後の探索 において，ボトルネックとはならない可能性があるた めである．そこで本提案手法では，学習節の削減の際， ある深さにおける節数が k 以下の場合，その深さの学 習節はボトルネックとなる節候補として削除せず保持 する．ここでは，k はパラメータ値である．

0 500 1000 1500 2000 2500 3000 3500 4000 4500 5000 0 20 40 60 80 100 120 140 160 180 200 glueminisat2.2.6-ucore k = 1 n = 0.95 (k = 1) + (n = 0.95) 求解数 CP U 時 間_〔sec 〕 ボトルネックとなる節候補の保持戦略 深い節の保持戦略 併用手法 図 4: 各手法における求解時間の比較 4.2.2 深い節の保持戦略 与えられた問題が充足不能である場合，空節をより 速く見つけ出すことは求解性能の向上につながる．空 節は学習節の中でも最も深いところに存在しているた め，深いところへの探索を促すことでより速く充足不 能を判定できると期待できる．もし深いところに存在 する節を削除すると，より深いところへの探索が進み 難くなると考えられる．そこで，学習節を削減する際， 現在の学習節の最深値×n より深いところに存在する 学習節を削除せず保持する手法を提案する．ここでは， n(0.0≤ n ≤ 1.0) はパラメータ値である．これにより， より深い位置にある学習節の導出が促されることが期 待される．

5

評価実験

4節で述べた学習節の深さに基づく 2 つの節管理戦 略の提案手法の評価実験を行い性能を評価する．提案 手法とそれらの併用手法を glueminisat2.2.6-ucore に実 装し，評価実験を行った．実験環境は前述の条件と同 じである． 表 3 は各手法における求解数を示している．全ての 提案手法で SAT な問題，UNSAT な問題の求解数が伸 びていることが分かる．深い節を保持する手法では， UNSATな問題に対して求解数の向上を期待していた が，実際には，UNSAT な問題において大きな向上が見 られなかった．どの提案手法も UNSAT な問題より SAT な問題のほうが求解数の向上がみられる結果となった． 各ソルバーの求解時間を，図 4 に示す．縦軸が求解 時間〔sec〕で，横軸が求解数を示している．図 4 より， 2000秒あたりまで大きな差は見られないが，それ以降 は提案手法のほうが求解性能の向上が見られる．

6

考察

評価実験の結果に関する詳細な調査を行った．まず， 実際のボトルネックの節をどの程度保持できたのかに ついて調べた． はじめに，既存の手法でのボトルネック保持割合を 調べた結果が表 4 である．表 4 より，既存のソルバー では約 50%であり，ボトルネックとなる節の半分は削 除されていることになる．SAT な問題と UNSAT な問 題では保持の割合に差があり，SAT な問題では約 65%， UNSATな問題では約 40%のボトルネックの節を削除 していた． 次に，提案手法であるボトルネックとなる節候補の 保持戦略において，実際のボトルネック数における提 案手法によって保持された節数の割合を調べた結果が 表 5 である．SAT な問題と UNSAT な問題の保持節は， 実際のボトルネック数に対して約 3.3 倍ほど保持して おり，ボトルネック以外の節を多く保持していること が分かった．SAT な問題に関してみてみると，実際の ボトルネックに対して約 5.6 倍ほど保持している．提 案手法によって保持された節は，既存の戦略では削除 されていた節であり，SAT な問題は求解数が伸びてい ることにより，既存の戦略では削除していた節の中に 今後の探索に役に立つ節が含まれていた可能性がある． UNSATな問題に関しては，実際のボトルネックに対 して約 1.3 倍ほどであり，無駄なくボトルネックとな る節群を保持できているといえる．UNSAT な問題は SATな問題ほど求解数が伸びてはいないが，既存のソ ルバーよりも求解数が伸びていることにより，ボトル ネックとなる節候補の保持戦略を用いることによりボ トルネックとなる節群を保持でき，保持した節が求解 に役に立つ節であったということが考えられる． 深い節の保持戦略と両戦略の併用手法も同様に，最 深部にある節集合を保持することで今後の探索に有用 な節を保持することができ，求解数が伸びたと考えら れる．学習節の深さを評価尺度のひとつとして使用す ることで，今後の探索に役に立つ節を保持することが 期待できる． 学習節の深さにおける評価尺度の妥当性を示すため に，LBD の評価尺度で保持した節に加えて，ランダム に節を保持する戦略との求解性能を比較した．ランダ ムで保持する節数は，各提案手法の保持節数と同等で ある．調査実験結果は表 6 で，差はわずかであるが，学 習節の深さを用いた戦略のほうが良い結果となった．す なわち，学習節の深さに基づく評価尺度は，良い学習節 を保持することができる可能性が高いこと示した．ま た，既存のソルバーよりも求解数が伸びていることに より，既存のソルバーでは学習節を削除し過ぎている 可能性があることをさらに示している．

表 3: 各手法における求解数の比較 ソルバー  求解数 (SAT + UNSAT) glueminisat2.2.6-ucore 188 (90 + 98) ボトルネックとなる節候補の保持戦略 (k = 1) 196 (95 + 101) 深い節の保持戦略 (n = 0.95) 197 (97 + 100) 併用手法 197 (94 + 103) 表 6: ランダムに節を保持した場合の求解数の比較 ソルバー  求解数 (SAT + UNSAT) ランダムに節を保持 glueminisat2.2.6-ucore 188 (90 + 98) -ボトルネックとなる節候補の保持戦略 (k = 1) 196 (95 + 101) 193 (94 + 99)  深い節の保持戦略 (n = 0.95) 197 (97 + 100) 192 (93 + 99) 併用手法 197 (94 + 103) 195 (95 + 100) 表 4: 既存の戦略でのボトルネック節の保持割合 SATな問題 + UNSAT な問題 46.81% SATな問題 34.27% UNSATな問題 58.44% 表 5: 提案手法でのボトルネック節の保持割合 SATな問題 + UNSAT な問題 332.66% SATな問題 557.12% UNSATな問題 125.41%

7

まとめと今後の課題

SAT問題の求解性能の向上を目指す手法として学習 節の深さに基づく節管理戦略を提案し評価を行った．既 存のソルバ―では有用な節を削除し過ぎている可能性 があることを示した．また，そのような節を保持する 評価尺度として学習節の深さを用いることが有効であ る可能性を示した． 今後の課題として，保持した節の詳細な検証や学習 節の深さにおける新しい評価尺度の考案が挙げられる．

謝辞

本研究の一部は，MEXT 科研費 (No.14467048, 13055676) ならびに H25 栢森情報科学振興財団研究助成 (K25 研 XVII第 426 号) による．

参考文献

[1] Cook, S.A.: The complexity of theorem-proving

pro-cedures, STOC ’71 Proceedings of the third annual

ACM symposium on Theory of computing, pp. 151-158 (1971).

[2] Davis, M., Logemann, G. and Loveland, D. W.: A Machine Program for Theorem-Proving, Commun. ACM, Vol. 5, No. 7, pp. 393-397 (1962).

[3] Bayardo, R. J. and Schrag, R. C.: Using CSP Look-Back Techniques to Solve Real-World SAT Instances, Proceedings of AAAI-97, pp. 203-208 (1997).

[4] Silva, J. P. M. and Sakallah, K. A.: GRASP:

A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, Vol. 48, pp. 506-521 (1999).

[5] Gershman, R., Koifman, M. and Strichman, O.: An Approach for Extracting a Small Unsatisfiable Core, Formal Methods in System Design, Vol. 1-3, No, 1-3, pp. 1-27 (2008).

[6] Katsirelos，G., Sabharwal, A., Samulowitz, H. and

Simon, L.: Resolution and Parallelizability : Barriers to the Efficient Parallelization of SAT Solvers, Pro-ceedings of the Twenty-Seventh Conference on Arti-ficial Intelligence (AAAI-13), (2013).

[7] Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L. and Malik, S.: Chaff: Engineering an Efficient SAT Solver, DAC, ACM, pp. 530-535 (2001).

[8] 渡辺 大樹， 鍋島 英知：最新SATソルバーへの充足不能

コア抽出手法の実装，The 27th Annual Conference of the Japanese Society for Artificial Intelligence, No.

2E4-OS-09a-3 (2013)．

[9] Een, N. and Sorensson, N.: An Extensible

SAT-solver, SAT, Proceedings of the 6th International Conference on Theory and Applications of Satisfi-ability Testing (SAT), pp. 502-518 (2003).

[10] Audemard, G. and Simon, L.: Predicting Learnt

Clauses Quality in Modern SAT Solver, Proc. IJCAI-09, pp. 399-404, (2009).