成分分割を用いる投射モデル計数ソルバにおける成分単位でのSAT判定を利用した性能改善

成分分割を用いる投射モデル計数ソルバにおける成分単位での

SAT

判定を利用した性能改善

Improvement of Projected Model-Counting Solver with Component

Decomposition Using SAT Solving in Components

鈴木 涼介

1∗

_橋本健二

1

_酒井正彦

1

Ryosuke Suzuki

1

_{Kenji Hashimoto}

1

_{Masahiko Sakai}

1

1

_{名古屋大学大学院情報科学研究科}

1

_{Graduate School of Information Science, Nagoya University}

Abstract: We improve our existing projected model-counting solver with component decompo-sition and caching. We use a CDCL algorithm, including backjumping and restarting, to decide whether components without projection variables are satisfiable or not. Furthermore, we try a limited backjumping technique according to the condition of processed components. We reimple-ment, on glucose, a projected model counter with component decomposition and caching. Then we add the above functions and evaluate by experiments them comparing with the existing projected model counters.

1

はじめに

命題論理式 F と変数集合 S に対して，論理式 F を 充足する真理割り当てを変数集合 S に制限したものを， F の S に関する投射モデルという．投射モデル計数問 題は，命題論理式と変数集合が与えられたときに，異 なる投射モデルの総数を求める問題である．投射モデ ル計数の応用の１つとして，プログラムの量的情報流 解析 [2] が挙げられる．これはプログラムを命題論理式 に変換して入出力等を表す特定の変数に関する投射モ デル計数を行うことで解析を行う．現状では比較的小 さなプログラムしか解析を行うことができず，より大 きなプログラムの解析を行うためには投射モデル計数 問題を解くソルバの高速化が課題となっている． 我々はこれまでに成分分割・キャッシングを利用し たモデル計数ソルバ sharpSAT [5] を投射モデル計数に 対応できるように拡張を行った（以降，sharpSATproj とよぶ）[7]．成分分割を用いるモデル計数ソルバは， CNF 論理式を，変数を共有しない独立した部分式（成 分）に動的に分割して，小さい成分のモデル数を計算 し，それらの結果を掛け合わせて分割前の成分のモデ ル数を求めていくのが特徴である．また，成分の計数 結果をキャッシュしておくことで，同じ成分が出現した ときに重複した計算を避けることが可能である．その ため，sharpSATproj は制約が比較的緩くモデル数が非 ∗_{連絡先：〒 464-8603 愛知県名古屋市千種区不老町 C-31(603)} 名古屋大学大学院情報科学研究科 酒井研究室 E-mail: suzuki [email protected]

常に多い問題を得意とする．一方で，阻止節を利用す る sharpclasp [1] などのソルバと比較して，複雑な制 約をもちモデル数が比較的少ない問題はあまり得意で はない． 現状の sharpSATproj の問題点として，投射変数で ない変数のみからなる成分に対しても成分分割が行わ れる点が挙げられる．そのような成分については充足 可能か否かを判定すれば十分であるが，現状ではその 他の成分と同様に分割処理を行いながら，すべての分 割成分について 1 つ以上のモデルが存在することが確 定した時点でバックトラックを行うようにしている．ま た，sharpSATproj ではバックジャンプやリスタートな どは行われないため，近年の CDCL ソルバと比べて矛 盾解消に時間がかかっている場合があると考えられる． そこで，投射変数を含まない成分に対しては，その 成分に限定してバックジャンプやリスタートを利用し た CDCL による SAT 判定を行う．また，それ以外の成 分を処理している際も，制限的なバックジャンプ [6] を 導入する．成分分割・キャッシングを利用した投射モデ ル計数処理を glucose 3.01_{をベースに再実装し，その} 上で以上で述べた手法を実装し評価実験を行った．そ の結果から，特に投射変数を含まない成分での SAT 判 定により性能が向上することを示す． 1_{http://www.labri.fr/perso/lsimon/glucose/} 人工知能学会研究会資料 SIG-FPAI-B506-07

2

準備

本節では，命題論理に関する諸定義と投射モデル計 数問題の定義を与える．また，文献 [7] で与えた DPLL 型投射モデル計数の手法に基づいた基本アルゴリズム を紹介する． 命題論理式と投射モデル計数問題 命題変数は，その 値として 1 または 0 をとり，これらの値はそれぞれ真 または偽に相当する．以降，命題変数を単に変数とよ ぶ．変数 x またはその否定¬x をリテラルという．リ テラルを論理和で結合した論理式を節という．節を論 理積で結合した論理式を CNF 式という．命題変数の有 限集合 X に対して，CNF 式 F 中に出現する変数 x が いずれも X に含まれるとき，F を X 上の CNF 式と よぶ． 変数集合 X 上の CNF 式 F に対して，X に対する 真理値割り当て ν : X → {0, 1} が F を充足するとき， ν を F のモデルという．また，X の部分集合 S につい て，F のモデル ν の定義域を S に制限したものを，F の S に関する投射モデルといい，ν|Sと表記する．S の ことを投射変数集合とよぶ． モデル計数問題（あるいは#SAT 問題）は，変数集 合 X 上の CNF 式 F が与えられたときに，F のモデ ルの総数を求める問題である．本稿で扱う投射モデル 計数問題は，X 上の CNF 式 F と投射変数集合 S が与 えられたときに，F の S に関する投射モデルの総数を 求める問題である．従来のモデル計数問題は，投射変 数集合が X である場合の投射モデル計数問題である． F のモデルの総数を #(F )，F の S に関する投射モデ ルの総数を #S(F ) と表記する．なお，S =∅ の場合， F が充足可能であるとき #S(F ) = 1，そうでなければ #S(F ) = 0 である． 例として，命題論理式 F = (x∨¬y∨z)∧(¬x∨y∨z) の 投射モデル数について考える．この論理式のモデル数は 3 変数への 8 通りの割り当てから充足しない 2 通りの割 り当て_{{x 7→ 0, y 7→ 1, z 7→ 0}, {x 7→ 1, y 7→ 0, z 7→ 0}} を除いた 6 である．これらの割り当ての中で，変数 x と y への値の割り当て方は_{{x 7→ 1, y 7→ 0}, {x 7→ 1, y 7→} 1}, {x 7→ 0, y 7→ 0}, {x 7→ 0, y 7→ 1} の 4 通りである． よって，変数集合_{{x, y} に関する F の投射モデル数は} 4 となる． 成分分割を用いる投射モデル計数 sharpSATproj およ び本稿で扱う投射モデル計数ソルバが基礎としている アルゴリズム PMC を説明する．Algorithm 1 に PMC を簡単のため再帰関数として示す．PMC は DPLL 方式 に基づく素朴な投射モデル計数アルゴリズム PCDP[7] をベースとし，節学習 [8] と成分分割及び成分キャッシ ング [3] を利用している． CNF 式 F を 共 通 の 変 数 が 現 れ な い 節 集 合 F1, F2,· · · , Fnに分割すると，F = F1∧F2∧· · ·∧Fnと 表すことができる．F1, F2,· · · , Fnを F の成分という． 異なるどの 2 つの成分も共通の変数をもたないため， F のモデル数は #(F ) = #(F1)× #(F2)× · · · × #(Fn) となる．F の投射変数集合 S に関する投射モデル数に ついては，各 Fiに現れる S 中の変数の集合を Siとお くと，#S(F ) = #S1(F1)× #S2(F2)× · · · × #Sn(Fn) となる．一度投射モデル数を求めた成分については， その数をキャッシュしておく．これによって後の探索 において同じ成分が出現したときに再計算を回避する ことができる．この手法を成分キャッシングという [3]． PMC では成分の投射モデル計数を始める段階でその 成分の投射モデル数がキャッシュに登録されているか チェックし，登録されていればその投射モデル数を利 用する．登録されていなければその成分用の格納領域 をキャッシュに確保し，投射モデル数を求めた後でそ の計数結果を登録する． 変数決定（Algorithm 1 の 1 行目）では，S に属する 投射変数が CNF 式 F に現れる場合はそれらを優先し て選択する．投射変数が 1 つも現れない場合のみ投射変 数以外を選択する．Algorithm 1 の 9 行目の SplitComp は成分分割を行う関数であり，分割成分の集合_{C と C} 中のどの成分にも属さず値が未割当である投射変数の 数 #ipvs を返す．21 行目において，成分が投射変数を もたない場合（S =∅）には充足可能性が判定できれば 十分であるため，投射モデル数が 1 以上であればその 成分の探索を終了する．

3

成分単位での

SAT

判定処理

PMC（Algorithm 1）の 14 行目において成分 C に 対する計数を行う際，成分 C に投射変数が含まれない 場合には実質 C が充足可能かどうかを判定すればよい． sharpSATproj では，そのような成分に対しても成分分 割を行い，各分割成分で 1 つ以上のモデルが存在する ことが確定した時点でバックトラックするようにして いる．しかしながら，成分分割のオーバーヘッドや，処 理中の成分を一時的に記憶するためのメモリ消費が無 視できない．また，sharpSATproj では矛盾発生時に節 学習を行ってはいるが，近年の SAT ソルバでよく利用 されるバックジャンプやリスタート [8] を利用していな い．そこで，成分分割時に投射変数が含まれない成分 が現れた場合には，その成分についてはバックジャン プおよびリスタートを含めた CDCL による SAT 判定 を行うようにする． 成分単位での CDCL による SAT 判定を用いるよ うに変更した点を説明するため，成分分割を行う関数 CompDivide（Algorithm 2）を導入し，それを利用し

Algorithm 1 投射モデル計数（sharpSATproj） PMC(CNF 式 F ，変数割当 ν, 投射変数集合 S) 1: F に現れる未割当の変数 x を選択（投射変数を優先） 2: #F [0] := #F [1] := 0; 3: for all v∈ {0, 1} do 4: ν′:= propagate(F, ν∪ {(x, v)}); 5: if 矛盾発生 then 6: 節学習; 7: #F [v] := 0; 8: else 9: (C, #ipvs) := SplitComp(F, ν′); 10: #F [v] := 2#ipvs_; 11: for all C ∈ C do 12: #C := Cache[c];

13: if #C = NOT FOUND then

14: #C := PMC(C, ν′, S∩ var(C)); 15: end if 16: #F [v] := #F [v]× #c; 17: if #F [v] = 0 then break; 18: end for 19: if #F [v] = 0 then CleanCache(); 20: end if

21: if S =∅ and #F [v] > 0 then break;

22: end for 23: Cache[F ] := #F [0] + #F [1]; 24: return #F [0] + #F [1] た PMC のより詳細なアルゴリズム gPMC（非再帰関 数）を Algorithm 3 に与える．CP [dl] は決定レベル dl で処理対象となっている成分，br[dl] はレベル dl の決 定変数に真偽のどちらが割り当てられているかを表す 状態（PMC での変数 v に相当），#(F, b) は F の分岐 b での投射モデル数（PMC での #F [v] に相当）を表す． CompStack は計数対象の成分を格納しているスタック であり，CompStack[dl] はレベル dl で生成された成分 集合を表す． CompDivide（Algorithm 2）では，成分分割を行っ た後，分割成分 C が投射変数をもたない場合に C に対 して SAT 判定（9 行目 solveSAT 関数）を行う．C が SAT であれば次の成分を調べ，そうでなければ分割前 の成分が充足不能であったということなので分割成分 をすべて削除し，false を返す．投射変数を含まない成 分がすべて SAT であれば true を返す． gPMC（Algorithm 3）では，PMC 同様に単位伝播 によって矛盾が発生しなかった場合に，成分分割を行 う（9 行目 CompDivide 関数）．返り値 res が false の 場合と現レベルでの分割において新たな成分が得られ なかった場合はバックトラックを行う．そうでなけれ ば CompStack に積まれた残りの成分の探索を続ける． Algorithm 2 成分分割 CompDivide(CNF 式 F , 変数割当 ν, 投射変数集合 S) 1: b := br[dl]; 2: (C, #ipvars) := SplitComp(F, ν); 3: #(CP [dl], b) := 2#ipvs_; 4: for all C∈ C do

5: if Cache[C] = NOT FOUND then

6: #(CP [dl], b) := #(CP [dl], b)× Cache[C]; 7: else

8: if C が S 中の変数をもたない then

9: if solveSAT(C) = SAT then continue;

10: CompStack[dl].clear(); 11: #(CP [dl], b) := 0; 12: return false; 13: else 14: CompStack[dl].push(C); 15: end if 16: end if 17: end for 18: return true; Algorithm 3 投射モデル計数 (本稿) gPMC(CNF 式 F ，変数割当 ν, 投射変数集合 S) 1: CP [0] = F ; dl = 0; 2: while true do 3: ν := propagate(CP [dl], ν) 4: if 矛盾発生 then 5: dl = 0 のとき return 0; 6: #(CP [dl], br[dl]) := 0; 7: (bl, x, v) := conflict analysis(); 8: (state, ν) := backjump(bl, x, v, ν); 9: else 10: res := CompDivide(F, ν, S);

11: if !res or CompStack[dl].empty() then

12: (state, ν) := backtrack(ν); 13: else

14: state := NEXTCOMP;

15: end if

16: end if

17: if state = EXIT then break;

18: else if state = NEXTCOMP then

19: CP [dl + 1] := CompStack[dl].pop(); 20: dl := dl + 1; 21: dvar[dl] := CP [dl] の変数 (投射変数を優先); 22: ν := ν∪ {(dvar[dl], 0)}; 23: br[dl] := 0; 24: end if 25: end while 26: return #(F, br[0])

gPMC 中の bakjump 関数と bactrack 関数について は 4 節で説明するが，返り値として EXIT，RESOLVE， NEXTCOMP のいずれかの状態を返す．EXIT は全体 の処理が終了したことを表す．RESOLVE はバックト ラック後に伴って現在のレベルでの決定変数の割り当 てが変更されている状態を表す．NEXTCOMP はある 成分の計数が終了したので同レベルで分割された別の 成分の処理に移ることを意味する．

4

バックジャンプの制限的利用

sharpSATproj は sharpSAT 12.08.1 を投射モデル計 数に対応させたソルバであるが，sharpSAT 12.08.1 で は矛盾発生時にバックジャンプを行う機能が搭載され ていない．このことが，sharpSATproj が，複雑な制約 をもちモデル数が少ない問題を得意としていない理由 の 1 つと考えられる．しかしながら，3 節での成分単 位での SAT 判定と異なり，成分分割を用いた投射モデ ル計数において一般にバックジャンプを行う場合，複 数の決定レベルの変数への割り当てを一度にキャンセ ルすることにより，既にモデル数を計算し終わってい る領域や，成分のキャッシュまで破棄する必要がある． これは誤って重複して計数を行わないためやキャッシュ 汚染 [3] を避けるためである．投射モデル計数の場合は すべての投射モデルを計数する必要があるため，破棄 された領域あるいはそれと重なりのある領域を後に再 探索しなければならない可能性がある．また，成分分 割・キャッシュを利用しているので，それらの再実行に よるオーバヘッドも無視できない [4]． そこで，文献 [6] で示されているバックジャンプ法を 参考に，成分の計数状況に応じてバックジャンプをす るかバックトラックをするかを切り替えるようにする． 決定レベル l での分割で得られたある成分が 1 つ以上 のモデルをもつ場合は，l より浅いレベルにはバック ジャンプさせないように制限する．制限を越えてバッ クジャンプしようとした場合は代わりに通常のバック トラックを行う．これにより，モデルを発見し数え終 わっている領域は変数への割り当てがキャンセルされ ないため，モデル数や成分のキャッシュの情報を破棄す ることなく探索を続けることができる． Algorithm 4 に制限を加えたバックジャンプ関数 buckjump を示す．バックジャンプするレベルの上限 は lim で与えられている．矛盾解析の結果バックジャ ンプするレベルが bl となったとき，bl < lim であれば バックジャンプせずにバックトラックする．そうでな ければバックジャンプを行う． バックトラック (Algorithm 5) では，#(CP [dl], 0) が 計数し終われば #(CP [dl], 1) の計数に切り替え（2∼9 行目），#(CP [dl], 1) が計数し終わっていれば 1 レベ Algorithm 4 制限付きバックジャンプ backjump(レベル bl, 変数 x, 真偽値 v, 変数割当 ν) 1: if bl < lim then 2: return backtrack(); 3: end if 4: while bl < dl do 5: ν := cancel(ν, dl); {dl での割当をキャンセル } 6: CompStack[dl].clear(); 7: CleanCache(); 8: dl := dl− 1; 9: end while 10: ν := ν∪ {(x, v)} 11: return (RESOLVE, ν) Algorithm 5 バックトラック backtrack(変数割当 ν) 1: while true do 2: if br[dl] = 0 then 3: ν := cancel(ν, dl); 4: ν := ν∪ {(dvar[dl], 1)}; 5: br[dl] := 1; 6: if lim > dl or #(CP [dl], 0) > 0 then 7: lim := dl; 8: end if 9: return (RESOLVE, ν) 10: else 11: total := #(CP [dl], 0) + #(CP [dl], 1); 12: Cache[CP [dl]] := total; 13: ν := cancel(ν, dl); 14: dl := dl− 1; 15: #(CP [dl], br[dl]) := #(CP [dl], br[dl])×total; 16: if total = 0 then 17: CompStack[dl].clear(); 18: CleanCache();

19: else if !CompStack[dl].empty() then

20: lim := dl + 1;

21: return (NEXTCOMP, ν);

22: end if

23: if dl = 0 then return (EXIT, ν);

24: end if 25: end while ル戻る（10∼23 行目）．バックトラック時に lim > dl あるいは成分 CP [dl] の投射モデル数がすでに 0 より大 きいならば lim を dl に設定する（7 行目）．また，同 じレベルの分割で得られた成分のうち投射モデル数が 0 でないことが確定した成分が存在する場合，lim をそ の成分の決定レベルより 1 深くする（20 行目）．

5

実装と評価実験

5.1

実装

MiniSat ベースの SAT ソルバである glucose 3.0 の ソースコードをもとにして，その中で利用されている データ構造を活用しつつ，成分分割・キャッシングを 用いた計数処理を実装した．そのソルバに 3 節と 4 節 で挙げた成分単位での SAT 判定やバックジャンプ機能 を追加した．以降，実装した投射モデル計数ソルバを gPMc とよぶ．Algorithm 2 の 9 行目の solveSAT(C) では，成分 C に現れる未割当変数集合のみを決定変数 の候補に限定した上で，それらのみから変数決定のた めのヒープを構成した後，glucose の solve メソッドを ほぼそのまま利用している．ただし，SAT 判定を始め る時点での決定レベル dl を 1 つ増やして，そのレベル を開始レベル sl とする．SAT 判定の処理中にバック ジャンプが発生した際に sl より浅いレベルに戻ろうと する場合には戻り先を sl に変更している．リスタート についても決定レベル 0 ではなく sl から再開させるよ うにしている．SAT 判定が終了した時点で決定レベル を dl に戻して判定結果を返す．

5.2

評価実験

gPMc と 3 節及び 4 節で挙げた手法の評価のため，既 存の投射モデル計数ソルバである sharpSATproj と同 等の計数処理のみを実装した gPMc-nocsat，成分単位 での SAT 判定を行う gPMc-nolbj，さらにバックジャ ンプを行う gPMc，の 3 つのバージョンの比較を行っ た．加えて，sharpSATproj や異なる計数手法を実装し た sharpclasp [1] との比較も行った．sharpclasp は阻 止節を利用して SAT ソルバを複数回実行することで投 射モデルを数え上げる手法をとっている．阻止節は投 射モデルを見つける度に増えていくが，探索の過程で 必ず充足する阻止節を消去することで増加を抑えてい る．また，投射モデルの割り当てのうち，式を充足す る極小な部分割り当てを求めることで，一度に複数の 投射モデルをまとめて数え上げることで高速化してい る．sharpclasp では CNF 式から LP を経由して ASP 問題に変換する必要があるが，今回の実験ではその変 換にかかる時間は省いてソルバによる求解時間のみで 比較を行った． 実行環境については，OS は FreeBSD 9.3，プロセッ サは Core-i7 i7-4790K(4.0GHz/4core cache 8MB)，メ モリは 32GB を搭載した PC を 10 台使用し，1 台につき 1 プロセスで 1 問ずつ実行した．実験で使用したベンチ マーク問題は，Pseudo-Boolean Competition 20162_の OPB-SMALLINT カテゴリの OPB 問題から CNF 式を 2_{http://www.cril.univ-artois.fr/PB16/} 0 500 1000 1500 2000 2500 3000 3500 300 350 400 450 500 550 600 時間 [秒 ] 求解数 sharpclasp sharpSATproj gPMc-nocsat gPMc-nolbj gPMc 図 1: 実験結果のカクタスプロット 生成した．そのカテゴリの問題 1600 問のうち，NaPS 1.02b3 _{で 1800 秒以内に CNF 式に変換でき，さらに} 節を 1 つ以上含みかつ MiniSat 2.2.0 で 3600 秒以内に SAT と判定された 1267 問を利用した．対象のカテゴ リの問題は最適化問題となっており，目的関数に現れ る変数に対応する命題変数を投射変数として指定した． 図 1 は各ソルバの実験結果のカクタスプロットである． 曲線が右下にあるほど短い実行時間でより多くの問題を 解けていることを表している．sharpSATproj と gPMc-nocsat は実装上での違いしかないが，gPMc-gPMc-nocsat の 方が 10 問程度求解数が多くなっている．gPMc-nocsat と gPMc-nolbj については，gPMc-nocsat は求解数が 453 問，gPMc-nolbj は 565 問となっており，投射変数 を含まない成分に対する SAT 判定処理の効果が大きく でていることが確認できる．また，gPMc-nolbj で新た に解けるようになった問題 112 問の中で gPMc-nocsat では実行中にメモリ不足で途中終了していた問題が 5 問あった．gPMc-nolbj では投射変数を含まない成分の 分割を行わないため，決定レベルごとに一時的に成分 を保持するために使っているメモリ消費が抑えられて いると考えられる．gPMc-nolbj とそれにバックジャン プの機能を追加した gPMc を比較するとほとんど差は なく，今回のベンチマークではバックジャンプによる 性能改善はあまり見られなかった． sharpSATproj と sharpclasp については，図 1 を見る と 1000 秒を超えたあたりから sharpclasp の方が求解数 が多くなっている．これらの２つのソルバで解ける問題 セットはかなり異なっている．表 1 に，sharpSATproj と sharpclasp, gPMc の投射モデル数ごとの求解数を示す． sharpSATproj と sharpclasp を比較すると，投射モデル 数が 105_{以下の比較的少ない問題に対しては sharpclasp} の方が求解数が多い．反対に，投射モデル数が 105_を超 えると sharpSATproj の方が求解数が多くなっている． gPMc は sharpSATproj と比較するとすべての投射モ 3_{https://www.trs.cm.is.nagoya-u.ac.jp/NaPS/}

表 1: 投射モデル数別の求解数 投射モデル数 sharpclasp sharpSATproj gPMc [1− 10) 275 270 273 [10− 102_{) 29 16 29} [102− 103) 21 20 21 [103− 104) 18 11 18 [104_{− 10}5_{) 99 7 95} [105_{− 10}6_{) 12 12 13} [106_{− 10}7_{) 8 9 9} [107− 108) 5 14 14 [108_{− ∞) 26 84 95} 合計 493 443 567 デル数帯において求解数が増加している．加えて，投 射モデル数が 104_{以下の問題に対しては sharpclasp と} ほぼ同数，104_{− 10}5_{に関しても sharpclasp の 96%程} 度解けており，投射モデル数が比較的少ない問題に対 しても性能が向上したことが確認できた．

6

おわりに

本研究では，成分分割・キャッシングを用いた投射モ デル計数法を glucose ベースで再実装し，成分単位で の SAT 判定やバックジャンプ法を利用するように拡張 した．評価実験を行い，これらの手法を実装すること により求解数が増加したことから，提案手法が成分分 割を用いる投射モデル計数ソルバの性能改善に有効で あることを確認した． 今後の課題として，プログラムの情報流解析などの 応用における評価が挙げられる．比較的小さい単純な プログラムから生成される CNF でも gPMc で解けな い場合が存在するため，CNF に変換する前段階での解 析との連携も必要であると考えられる．また，規模の 大きい問題に対応するため，投射モデル計数の並列化 や近似計算なども課題として挙げられる．

参考文献

[1] R. A. Aziz, G. Chu, C. Muise, and P. Stuckey. #∃SAT: projected model counting. In Proc. of the 18th SAT, LNCS 9340, pp. 121–137, 2015. [2] V. Klebanov, N. Manthey, and C. Muise.

SAT-based analysis and quantification of information flow in programs. In Proc. of the 10th QEST, LNCS 8054, pp. 177–192, 2013.

[3] T. Sang, F. Bacchus, P. Beame, H. Kautz, and T. Pitassi. Combining component caching and clause learning for effective model. In Online Proc. of the 7th SAT, 2004.

[4] T. Sang, P. Beame, and H. Kautz. Heuristics for fast exact model counting. In Proc. of the 8th SAT, LNCS 3569, pp. 226–240, 2005.

[5] M. Thurley. sharpSAT - counting models with advanced component caching and implicit BCP. In Proc. of the 9th SAT, LNCS 4121, pp. 424– 429, 2006.

[6] T. Toda. and T. Soh. Implementing efficient all solutions SAT solvers. Journal of Experimental Algorithmics, Vol. 21, No. 1.12, pp. 1–44, 2016. [7] 鈴木涼介, 橋本健二, 酒井正彦. DPLL 型モデル計 数ソルバの投射モデル計数への拡張. 人工知能学 会 人工知能基本問題研究会, SIG-FPAI-B404-11, pp. 59–64, 2015. [8] 鍋島英知, 宋剛秀. 高速 SAT ソルバーの原理. 人工 知能学会誌, Vol. 25, No. 1, pp. 68–76, 2010.