DPLL型モデル計数ソルバの投射モデル計数への拡張

DPLL

型モデル計数ソルバの投射モデル計数への拡張

An Extension of a DPLL-Based Model-Counting Solver

for Projected Model

鈴木 涼介

1∗

橋本 健二

2

酒井 正彦

2

Ryosuke Suzuki

1

Kenji Hashimoto

2

Masahiko Sakai

2

1

_{名古屋大学工学部}

1

_{School of Engineering, Nagoya University}

2

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

2

_{Graduate School of Information Science, Nagoya University}

Abstract: We extend a model-counting solver for projected models of a propositional CNF for-mula. A projected model is a projection of a model of a formula on a given set of variables. We give an extension of a DPLL-based model-counting algorithm for projected models, and extend the model-counting solver sharpSAT to count the exact number of projected models. We experimen-tally show that the extended solver achieves better performance than existing solvers for projected models.

1

はじめに

命題論理式を充足する真理値割り当て（モデル）の 数を求めることをモデル計数という．通常のモデル計 数は，命題論理式に現れる変数のうち１つでもその変 数への真理値割り当てが異なるようなモデルは別のモ デルとして数える．一方，命題論理式を充足する真理 値割り当てを特定の変数集合に制限した割り当ての数 を求めることを投射モデル計数という．すなわち，命 題論理式のモデルを，特定の変数集合への割り当ての 違いのみに注目して数えることである．例として，次 の命題論理式を考える． (x∨ ¬y ∨ z) ∧ (¬x ∨ y ∨ z) そのすべてのモデルは以下のように数え上げられるた め，モデル数は 6 である． {x 7→ 1, y 7→ 0, z 7→ 1}, {x 7→ 1, y 7→ 1, z 7→ 0}, {x 7→ 1, y 7→ 1, z 7→ 1}, {x 7→ 0, y 7→ 0, z 7→ 0}, {x 7→ 0, y 7→ 0, z 7→ 1}, {x 7→ 0, y 7→ 1, z 7→ 1} これらのモデルの中で，x と y に割り当てられた値に 注目すると，以下の 4 個なので，{x, y} に制限した投 射モデル数は 4 となる． {x 7→ 1, y 7→ 0}, {x 7→ 1, y 7→ 1}, {x 7→ 0, y 7→ 0}, {x 7→ 0, y 7→ 1} ∗_{連絡先：〒 464-8603 愛知県名古屋市千種区不老町 C3-1(631)} 名古屋大学 大学院情報科学研究科 酒井研究室 E-mail: suzuki [email protected]

投射モデル計数の応用例としてプログラムの量的情 報流解析 [4] が挙げられる．量的情報流解析においては， エントロピーなどの尺度でプログラムの入力から出力 へどの程度の情報が流れるのかを解析する．その手法 の１つとして，プログラムの入出力関係を表す CNF 式 を生成し，プログラムの入力あるいは出力に対応する 命題変数に関する投射モデル計数の結果を利用して解 析を行う方法が提案されている [4]． 既存の投射モデル計数ソルバとして sharpCDCL や

sharp-p-SATが知られている [4]．sharpCDCL は SAT

ソルバ miniSAT をベースとし，モデルを 1 つ見つけ るたびにそのモデルの指定変数部分の否定を表す節を 追加して次のモデルを探すことで計数を行う．そのた め，モデル数が少ない問題は高速で解くことができる が，モデル数が多い問題では実行時間は長くなり，モ デル数が 107_{程度以上になると現実的な時間で解くこ} とができなくなる．一方，sharp-p-SAT はモデル数が 多い場合でも高速で計数可能な DPLL 型モデル計数ソ ルバ sharpSAT [8] を拡張したものである．しかし，投 射モデル数の上界を出力するだけであり，問題によっ ては正確なモデル数と大きな誤差が生じる． 本研究の目的は，モデル数が多い論理式の投射モデ ル数を高速かつ正確に求めるためのソルバを開発する ことである．そのために，sharpSAT が採用する DPLL 型モデル計数アルゴリズムを正確な投射モデル数が求 められるように拡張した．具体的には，指定された変 数集合の変数への真理値割り当てを優先して行い，そ 人工知能学会研究会資料 SIG-FPAI-B404-11

れ以外の変数のみが残った場合には充足する真理値割 り当てを 1 つ見つけた時点で探索を終了し，指定変数 の決定段階までバックトラックして計数を続けるよう に変更した． 実際に，モデル計数ソルバ sharpSAT に提案したア ルゴリズムを組み込むことにより，投射モデル計数ソ ルバを開発した．次に，sharpSAT のベンチマークに 使われた SATLIB の問題に変数集合を追加して作成し た問題と sharpCDCL のベンチマークの問題を使用し て評価実験を行い，拡張の有効性を示した．また，本 研究のソルバの処理中に行う充足可能性を調べる部分 について，いくつかのヒューリスティクスの効果を比 較した． 本稿の構成は以下の通りである．2 節では必要な諸 定義を与える．3 節では DPLL 型モデル計数アルゴリ ズムの投射モデル計数アルゴリズムへの拡張について 述べる．4 節では，拡張したアルゴリズムを用いて投 射モデル計数ソルバの実装を行い，本研究のソルバの 性能評価を行った結果を示す．最後に，5 節でまとめと 今後の課題について述べる．

2

準備

命題変数は，その値として 1 または 0 をとり，これ らの値はそれぞれ真または偽に相当する．以降，命題 変数を単に変数とよぶ．変数 x またはその否定¬x を リテラルという．リテラル l に現れる変数を var(l) と書 く．また，リテラル l の補リテラルを¬l と書く．リテ ラルを論理和で結合した論理式を節という．特に，リテ ラルを含まない節を空節，リテラルをただ 1 つ含む節 を単位節とよぶ．節を論理積で結合した論理式を CNF 式という．本稿では，節をリテラルの集合，CNF 式を 節の集合とみなす．命題変数の有限集合 X に対して， CNF式 F 中に出現する変数 x がいずれも X に含まれ るとき，F を X 上の CNF 式とよぶ．CNF 式 F に対 して，リテラル l が真となるように var(l) に値を割り 当てて得られる CNF 式を F|lと表記する． 変数集合 X 上の CNF 式 F に対して，X に対する 真理値割り当て M : X → {0, 1} が F を充足するとき， M を F のモデルという．また，X の部分集合 S につ いて，F のモデル M の定義域を S に制限したものを， F の S に関する投射モデルといい，M|S と表記する． Sのことを投射変数集合とよぶ． 例 1 CNF 式 F = {{x, ¬y, z}, {¬x, y, z}} に対して， M ={x 7→ 1, y 7→ 0, z 7→ 1} は F のモデルの 1 つであ る．投射変数集合 S ={x, y} に対して，M|S ={x 7→ 1, y7→ 0} は F の S に関する投射モデルの 1 つである． モデル計数問題（あるいは#SAT 問題）は，変数集 合 X 上の CNF 式 F が与えられたときに，F のモデル の総数を求める問題である．本稿で扱う投射モデル計 数問題は，X 上の CNF 式 F と投射変数集合 S が与え られたときに，F の S に関する投射モデルの総数を求 める問題である．従来のモデル計数問題は，投射変数 集合が X である場合の投射モデル計数問題である．F のモデルの総数を #(F )，F の S に関する投射モデル の総数を #S(F )と表記する．

3

DPLL

型モデル計数の投射モデル

計数への拡張

本節では，DPLL 型モデル計数アルゴリズムを投射 モデル計数が行えるように拡張する方法について説明 する．我々はモデル計数ソルバ sharpSAT を正確な投 射モデル計数が行えるように拡張する．ここで，拡張 の本質を明快に説明するため，素朴な DPLL 型#SAT アルゴリズム CDP[2] をベースとして投射モデル計数 への拡張について説明する．

3.1

CDP

アルゴリズム

モデル計数アルゴリズムである CDP[2, 11] は SAT ソルバの基礎となる DPLL [3] にもとづいたアルゴリ ズムである． 図 1 に示すアルゴリズム CDP は変数集合 X と X 上 の CNF 式 F を入力とし，以下のように動作する．F が空集合であるならば，X へのどの真理値割り当てに ついても F は充足されるので，2|X|を返す．また，F が空節を含むとき，モデルは存在しないので 0 を返す． 上述以外の場合，F が単位節を含めばそれを真にする 割り当てを行う（単位伝播）．単位伝播した式を F′と し，F′に CDP を適用して得られる F1のモデル数を返 す．単位節がなければ，割り当て未定の変数 x を選び， F を (x∧ F |x)∨ (¬x ∧ F |¬x)にシャノン展開する．F のモデル集合は x∧ F |xと¬x ∧ F |¬xのモデル集合の 和であり，それらの 2 つの集合は互いに素である．よっ て，F1 = F|xと F2 = F|¬xを X− {x} 上の CNF 式 と考えると，#(F ) = #(F1) + #(F2)が成り立つ．こ のようにして再帰的に CDP を適用することで F のモ デル数を計算することができる． なお，文献 [2, 11] では CDP の入力として変数集合 Xではなく X の大きさが与えられているが，ここでは 後に説明する投射モデル計数アルゴリズムとの対応を わかりやすくするため変数集合そのものを入力として いる．

  入力: 変数集合 X，X 上の CNF 式 F 出力: F のモデルの数 #(F ) if F が空集合 then return 2|X|; if F が空節を含む then return 0; if F が単位節 l を含む then F′={C − {¬l} | C ∈ F, l ̸∈ C}; return CDP(F′, X− {var(l)}); end if F に出現する変数 x を選択; F1={C − {¬x} | C ∈ F, x ̸∈ C}; F2={C − {x} | C ∈ F, ¬x ̸∈ C}; return CDP(F1, X−{x})+CDP(F2, X−{x});   図 1: アルゴリズム CDP(F, X)

3.2

投射モデル計数のための拡張

3.1節で述べた CDP を投射モデル計数に対応させる 拡張のアイディアを説明する．CDP からの変更点は以 下の 2 つである． • 値を割り当てる未定変数の決定の際に投射変数集 合中の変数を優先して選択する. • 投射変数が現れない CNF 式 F に対しては，充足 可能であれば 2n（n は未定な投射変数の数）を， 充足不能であれば 0 を返す． 投射モデル計数に対応した具体的なアルゴリズム PCDP（図 2 参照）を説明する．PCDP は CNF 式 F と投射変数集合 S を入力とし，以下のように動作す る．PCDP では，対象とする変数集合 X 全体ではな く投射変数集合 S になっている点を除けば，F が空集 合であるときと，空節を含むとき，そして単位節を含 むときの処理は 3.1 節の CDP と同様である．それら 以外の場合では，S 中の変数が F に少なくとも 1 つ 出現するならば，そのような変数の 1 つを選択して， CDPと同様に，その変数にそれぞれ 0 と 1 を割り当て た場合の投射モデルの数の和を返す．一方，S 中の変 数が F に一切出現しない場合は，通常の DPLL のよ うに充足可能性をチェックする．ただし，充足可能な 場合は 2|S|を返し，そうでなければ 0 を返す．具体的 には，F に出現する（S に含まれない）未割り当ての 変数 x を選び，F = (x∧ F |x)∨ (¬x ∧ F |_¬x)と展開 し，F1 = F|x, F2= F|¬xとする．次に PCDP(F1, S) を呼び出しその返り値が 0 より大きければ，F1は充 足可能かつ #S(F1) = 2|S|であるので，#S(F1)をそ のまま返す．そうでなければ，PCDP(F2, S)を呼び出 しその返り値をそのまま返す．F2が充足可能であれば PCDP(F2, S)の返り値は #S(F2) = 2|S|であり，そう   入力: CNF 式 F ，投射変数集合 S 出力: F の S に関する投射モデルの数 #S(F ) if Fが空集合 then return 2|S|; if Fが空節を含む then return 0; if Fが単位節 l を含む then F′ ={C − {¬l} | C ∈ F, l ̸∈ C}; return PCDP(F′, S− {var(l)}); end if if S中の少なくとも 1 つの変数が F に出現する then F に出現する S 中の変数 x を選択; F1={C − {¬x} | C ∈ F, x ̸∈ C}; F2={C − {x} | C ∈ F, ¬x ̸∈ C}; return PCDP(F1, S− {x}) +PCDP(F2, S− {x}); else F に出現する変数 x を選択; F1={C − {¬x} | C ∈ F, x ̸∈ C}; F2={C − {x} | C ∈ F, ¬x ̸∈ C}; if PCDP(F1, S) > 0 then return PCDP(F1, S); else return PCDP(F2, S); end if   図 2: アルゴリズム PCDP(F, S) でなければ 0 が返る．したがって，F が充足可能な場 合は 2|S|が返り，そうでなければ 0 が返る． 例 2 CNF 式 F ={{x, z}, {x, y, ¬z, w}} の投射変数集 合 S ={x, y} に関する投射モデルの総数 #S(F )を求 めよう．このとき，PCDP(F, S) は以下に示すように 実行される（図 3 参照）． まず，F に投射変数 x, y が出現するので，ここでは xを選択するとする． F1=∅, F2={{z}, {y, ¬z, w}} として，PCDP(F1,{y}) と PCDP(F2,{y}) が呼び出 される．PCDP(F1,{y}) については，F1が空集合で あることと投射変数が 1 つであることから 21_が返る． PCDP(F2,{y}) については，単位節 {z} を含むので， F₂′ ={{y, w}} として PCDP(F2′,{y}) が呼び出される．PCDP(F2′,{y}) については，投射変数 y が F2′に出現するので y が選 択される． F21=∅, F22={{w}}

として，PCDP(F21,∅) と PCDP(F22,∅) が呼び出され る．PCDP(F21,∅) は 20を返す．PCDP(F22,∅) につい ては，単位節{w} を含むので，さらに PCDP(∅, ∅) が 呼び出され最終的に 20が返る．よって，PCDP(F2′,{y}) お よ び PCDP(F2,{y}) は ，PCDP(F21,∅) と PCDP(F22,∅) の 返 り 値 の 和 2 を 返 す．最 後 に ， PCDP(F,{x, y}) の 返 り 値 は ，PCDP(F1,{y}) と PCDP(F2,{y}) の返り値の和をとって，4 となる． ({{x,z},{x,y,¬z,w}},{x,y}) 4 (∅,{y }) 2 ({{z},{y,¬z,w}},{y }) 2 ({{y,w}},{y }) 2 (∅,∅) 1 ({{w }},∅) 1 (∅,∅) 1 x= 1 x= 0 z= 1 y= 1 y= 0 w= 1 図 3: PCDP による投射モデル計数の例

4

ソルバの拡張と評価実験

4.1

sharpSAT

の拡張

3節で説明した投射モデル計数への拡張アルゴリズ ム PCDP に則って，DPLL 型モデル計数ソルバ sharp-SAT [8]を投射モデル計数に対応させた．sharpSAT では成分分割・成分キャッシング [1, 6] や節学習，Im-plicit BCP [8]などの技術が利用されている．また，値 を割り当てる変数を決定するヒューリスティクスとし て VSADS [7] が採用され，lastUIP を用いた矛盾から の節学習 [9] が利用されている．今回の sharpSAT の 拡張ではこれらの技術は基本的にはそのまま利用した． 入力形式には DIMACS 形式の CNF ファイルを利用し， 投射変数集合はヘッダ部分に変数の番号を列挙する形 で指定することとした．

4.2

評価実験

この節では次に説明する２つの評価実験を行った結 果を示す． まず，本研究のソルバの評価のため，sharpCDCL と sharp-p-SATという既存の投射モデル計数ソルバ [4] と

の比較を行った．sharpCDCL は SAT ソルバ miniSAT

をベースとし，モデルを 1 つ見つけるたびにそのモデ ルの投射変数への割り当てを否定した節をもとの論理 式に追加して次のモデルを探すということを繰り返す ことによって，全ての投射モデルを列挙する．sharp-p-SATは，本研究でのソルバと同様な sharpSAT の投 射モデル計数への拡張である．しかし，sharp-p-SAT は投射モデル数の上界を出力するだけであり，問題に よっては正確なモデル数と大きな誤差が生まれること がある．以上の 2 つのソルバと本研究のソルバとの間 で，実行時間と解けた問題数の比較を行った． 次に，PCDP では充足可能性のみを判定する部分が あるので，本研究のソルバにおけるその充足可能性判 定の部分で現代の SAT ソルバにおいて有効とされる技 術を採用した場合とで，実行時間と解けた問題数の比 較を行った． 今回ベンチマークとして利用した問題数は 331 問で ある．内訳は，文献 [4] で用いられていたベンチマー ク 7 問と，sharpSAT のベンチマークとして使用され た SATLIB の問題から 27 問選んで投射変数集合を追 加して作成した 324 問である．SATLIB の各問題につ き 12 通りの投射変数集合を指定した．投射変数の数を CNF式の変数の数の 1/2, 1/4, 1/10, 1/100 の 4 通り， 投射変数の選び方を CNF 式に出現する回数が多い順に 選択，少ない順に選択，その両方から半分づつ選択の

3通りとした．実験環境は Ubuntu 14.04, CPU Intel

Core i7-2600 3.40GHz,メモリ 8GB である． 4.2.1 既存の投射モデル計数ソルバとの比較 本研究のソルバと sharpCDCL，sharp-p-SAT の 3 つ のソルバでそれぞれ問題を解き，実行時間とタイムア ウト前に解けた問題数を比較した．タイムアウトは 600 秒に設定した．各ソルバでタイムアウト前に解けた問 題数と実行結果のカクタスプロットを表 1 と図 4 に示 す．表 1 の sharp-p-SAT の欄の () 内の数字は，解け た問題の中で正確に投射モデル数が数えられた問題数 である．ここで，カクタスプロットはある時間内に解 けた問題数を表すグラフであり，グラフの線が下にあ るほど，また，右にあるほど良い結果であるといえる． sharpCDCLと本研究のソルバを比較する．表 1 に示 す通り，タイムアウトせずに解けた問題数は sharpCDCL が 104 問であるのに対して，本研究のソルバは 207 問 であり本研究のソルバの方が多い．sharpCDCL で解け た問題は，本研究のソルバでも実行時間が長くなるもの が多いもののタイムアウト前にはすべて解けた．本研究 のソルバで解けた問題のうち投射モデルの数が 600000 以下である問題は sharpCDCL で解けたが，それ以上 の数の投射モデルをもつ問題はタイムアウトまでに解 けなかった．よって，本研究のソルバは sharpCDCL よ

表 1: タイムアウト前に解けた問題数 sharpCDCL sharp-p-SAT 本研究のソルバ 104 205 (129) 207 Ϭ ϭϬϬ ϮϬϬ ϯϬϬ ϰϬϬ ϱϬϬ ϲϬϬ Ϭ ϱϬ ϭϬϬ ϭϱϬ ϮϬϬ ϮϱϬ ᐇ⾜ ᫬㛫 䠄 ⛊ 䠅 ゎ䛡䛯ၥ㢟ᩘ ƐŚĂƌƉ> ƐŚĂƌƉͲƉͲ^d ƐŚĂƌƉͲƉͲ^d㸦ṇゎ䛾䜏䠅 ᮏ◊✲䛻䜘䜛ᣑᙇ 図 4: 既存のソルバとの比較結果 りも解ける問題数が多く，投射モデル数が多い問題で は特に有効であるといえる． 次に，sharp-p-SAT と比較すると，解けた問題数だ けならば，表 1 より，本研究のソルバが 207 問であるの に対し，sharp-p-SAT は 205 問とあまり差はみられな かった．図 4 より時間内に解けた問題数の変化にも大 きな差はなかった．しかし，sharp-p-SAT が出力した モデル数が正確である問題数は 205 問中 129 問であっ た．したがって，本研究のソルバは今回のベンチマー クにおいて正確なモデル数を sharp-p-SAT と同程度の 速度で求めることができた．なお，sharp-p-SAT のモ デル数が正確であるかは，本研究のソルバの結果によ り確認した．ここで，sharp-p-SAT では解けたが本研 究のソルバではタイムアウトした問題 3 問については， 本研究のソルバを最大 6 時間程度動作させることで確 認した． 4.2.2 SATソルバの高速化手法の利用の効果 本研究のソルバでは処理の途中で充足可能性のみを 調べる部分が存在する．そのため，その部分では現代 の SAT ソルバで利用されている手法に切り替えること を試みた．sharpSAT では変数選択ヒューリスティクス に VSADS が利用されているが，miniSAT などの主流 の SAT ソルバでは VSIDS [5, 10] が利用されている． また，sharpSAT では Implicit BCP とよばれる単位伝 播ヒューリスティクスに基づく手法が利用されている． モデル計数では効果的であることは報告されているが， Ϭ ϭϬϬ ϮϬϬ ϯϬϬ ϰϬϬ ϱϬϬ ϲϬϬ Ϭ ϱϬ ϭϬϬ ϭϱϬ ϮϬϬ ϮϱϬ ᐇ⾜ ᫬㛫䠄⛊䠅 ゎ䛡䛯ၥ㢟ᩘ ኚ᭦䛺䛧 /W䛺䛧 s^/^ s^/^ͬ/W䛺䛧 ĨŝƌƐƚh/W ĨŝƌƐƚh/Wͬ/W䛺䛧 ĨŝƌƐƚh/Wͬs^/^ ĨŝƌƐƚh/Wͬs^/^ͬ/W䛺䛧 図 5: SAT ソルバでの手法への切り替えによる効果 充足可能性判定においてはオーバーヘッドの方が大き い可能性もある．また，矛盾からの節学習には lastUIP が利用されているが，SAT ソルバでは firstUIP [9, 10] を利用した方が効果があるとされている．そこで，本 研究のソルバにおける充足可能性の判定部分を以下の 3 項目について変化させた 8 通りの実行時間を比較した． • Implicit BCP: 行う/行わない • 変数選択ヒューリスティクス: VSADS/VSIDS • 矛盾からの節学習: firstUIP/lastUIP タイムアウトは 600 秒に設定した． 実験結果のカクタスプロットを図 5 に示す．図に示 す通り，いずれの場合でも解けた問題数はほとんど変 わらなかった．Implicit BCP を利用しない方が倍近く 速く解けた問題も存在したが，逆にタイムアウトまで に解けなくなった問題も数問存在した．

5

おわりに

本研究では，DPLL 型モデル計数アルゴリズムを拡 張した投射モデル計数アルゴリズムを与えた．そして， 既存のモデル計数ソルバ sharpSAT のモデル計数アル ゴリズムを拡張したアルゴリズムに置き換えることに より投射モデル数を正確に求めるソルバを実現した．評 価実験により，一定時間内で解ける問題数あるいは解 の正確さにおいて，既存の投射モデル計数ソルバであ る sharpCDCL や sharp-p-SAT と比較して優れた結果 が得られた． 本研究の投射モデル計数の拡張は直観的で素朴な方法 であるため，実行効率について改善の余地はあると考え られる．また，PCDP の実行中に，充足可能性を判定す れば十分な場合においても，我々の実現では sharpSAT のモデル計数用のコードを利用しており，効率を低下 させる原因になっている．そこで，最新の SAT ソルバ

の技術をうまく組み込むことで高速化が可能ではない かと考えている．さらに，今回は正確な投射モデルの 総数を求めるソルバの実現を目指したが，実用的には モデルの総数の近似値を高速に求めることも重要であ る．近似モデル計数ソルバの投射モデル計数への拡張 も今後の課題である．

参考文献

[1] Bayardo, R. J. and Pehoushek, J. D.: Count-ing models usCount-ing connected components, Proc. AAAI-00, pp. 157–162, 2000.

[2] Birnbaum, E. and Lozinskii, E. L.: The good old Davis-Putnam procedure helps counting models, J. Artif. Intell. Res., Vol. 10, pp. 457–477, 1999. [3] Davis, M., Logemann, G. and Loveland, D., A machine program for theorem proving, Commun. ACM, Vol. 5, No. 7, pp. 394–397, 1962.

[4] Klebanov, V., Manthey, N. and Muise, C., SAT-based analysis and quantification of information flow in programs, Proc. QEST-13, pp. 177–192, 2013.

[5] Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L. and Malik, S., Chaff: Engineering an efficient SAT solver, Proc. DAC-01, pp. 530–535, 2001.

[6] Sang T., Bacchus F., Beame P., Kautz H. and Pitassi T., Combining component caching and clause learning for effective model counting, Proc. SAT-04, pp. 20–28, 2004.

[7] Sang T., Beame P. and Kautz H., Heuristics for fast exact model counting, Proc. SAT-05, pp. 226–240, 2005.

[8] Thurley, M., sharpSAT - Counting models with advanced component caching and implicit BCP, Proc. SAT-06, pp. 424–429, 2006.

[9] Zhang, L., Madigan, C. F., Moskewicz, M. H. and Malik, S., Efficient conflict driven learning in a boolean satisfiability solver, Proc. ICCAD-01, pp. 279–285, 2001. [10] 鍋島英知，宋剛秀，高速 SAT ソルバーの原理，人 工知能学会誌，25 巻 1 号，pp. 68–76，2010． [11] 長谷川 隆三，藤田 博，越村 三幸，モデル列挙と モデル計数，人工知能学会誌，25 巻 1 号，pp. 96– 104，2010．