SAT
ソルバーを用いた
MCS
列挙の実装とその評価
An Implementation of MCSes Enumeration with a SAT Solver and
its Evaluations
越村 三幸
1∗佐藤 健
2Miyuki Koshimura
1Ken Satoh
21
九州大学大学院システム情報科学研究院
1
Faculty of Information and Electrical Engineering, Kyushu University
2
国立情報学研究所
2
National Institute of Informatics
Abstract: Enumerating all Maximal Satisfiable Subsets (MSSes) or all Minimal Correction Sub-sets (MCSes) of an unsatisfiable CNF Boolean formula is a cornerstone task in various AI domains. This paper considers MCSes enumeration with a SAT solver. The paper presents a basic enumer-ation procedure and compares it with a state-of-the-art enumerator Enum-ELS-RMR-Cache. The experimental results show that the proposed procedure is more efficient than Enum-ELS-RMR-Cache to solve Partial-MaxSAT instances but it is inefficient than Enum-ELS-RMR-Cache to solve plain MaxSAT instances.
1
はじめに
解を一つも持たない制約集合のことを過制約（over-constrained）という．過制約な制約集合の MSS（Maxi-mal Satisfiable Subset）あるいは MCS（MiniMSS（Maxi-mal Cor-rection Subset）を求めることは，人工知能の様々な分野 で重要とされている [Gr´egoire 18]．本稿では，SAT ソル バーを利用した MCS の列挙を論ずる．同様の研究は多 くあるが，我々は，効率性の点でそれらを上回る列挙手 続きの提案と実装を目的としている．本稿ではその基本 手続きを示し，その実装の性能を現時点で最高性能を示 していると思われる Enum-ELS-RMR-Cache[Gr´egoire 18] と比較する．
2
準備
本稿では，問題は節集合で与えられるものとする． 節（clause）はリテラル（literal）の選言（論理和∨） でリテラルはブール変数あるいはその否定（¬）であ る．ブール変数の集合を V ar とする．変数の値割当て µ は，V ar から{0, 1} の写像である．節集合 Σ に現れ る変数の値割当て µ で Σ の全ての節を 1 にするものが ある時，Σ は充足可能（satisfiable），そのような µ が ない時，充足不能（unsatisfiable）であるという． ∗連絡先：九州大学大学院システム情報科学研究院 〒 819-0395 福岡市西区元岡７４４番地 E-mail: [email protected] 本稿では二種類の節，ハード節とソフト節を扱う． ハード節の集合 Σ1とソフト節の集合 Σ2からなる節集 合 Σ (= Σ1∪ Σ2) に対して，MSS と MCS は次のよう に定義される．定義 1 (MSS) Σ の MSS（maximal satisfiable
sub-set）Φ は，Σ1を含む Σ の部分集合（Σ1 ⊆ Φ ⊆ Σ）
で，充足可能，かつ，∀α ∈ Σ \ Φ, Φ ∪ {α} は充足不能， を満たすものである．
MSS は充足可能性を保ちつつ，Σ1を Σ2のソフト節
でぎりぎりまで拡大した節集合である．
定義 2 (MCS) Σ の MCS（minimal correction
sub-set）Ψ は，Σ の部分集合（Ψ ⊆ Σ）で，その補集合， つまり Σ\ Ψ が Σ の MSS であるものである． MSS は Σ1を含むので，MCS は Σ2の部分集合であ る．MCS は Σ2の部分集合で，それを取り除くと Σ が 充足可能になる，ぎりぎりまで小さい節集合である． SAT ソルバーを利用した MCS 列挙プログラムでは しばしば，ソフト節に対し節選択変数（clause selector） と呼ばれる変数が次のように導入される．それぞれの ソフト節 α ∈ Σ2に対し，新変数 sαを導入し，その 否定を元のソフト節に加えた α∨ ¬sαを作る．これに より，新しい節集合 ΣS 2 = {α ∨ ¬sα | α ∈ Σ2} が得 られる．そして，SAT ソルバーを，Σ そのものでなく， Σ1∪ ΣS2 の充足可能性判定に利用する． 人工知能学会研究会資料 SIG-FPAI-B803-01 － 2 －
sα= 1 の仮定の下では，α∨ ¬sαと元の節 α は充足 可能性が一致するので，sα= 1 とすることを α∨ ¬sα を活性化（activate）する，という．逆に sα= 0 とす ることを非活性化（deactivate）する，という． なお，SAT ソルバーに関する最近の動向については， [宋 18] を参照されたい．
3
MCS
列挙アルゴリズム
Algorithm 1 に提案アルゴリズムの概観を示す．6 行 目の SAT (Σ1∪ΣS2, A) が SAT オラクルを示し，A に含まれるリテラルの値が全て 1 と仮定した時の Σ1∪ΣS2の 充足可能性を判定する．充足可能であれば st が T RU E となり，見つけた変数の値割当て µ が得られる．充足 不能であれば，st が F ALSE となる． Algorithm 1 Enum-MCS (Σ の全ての MCS を列挙 する) 入力： Σ (= Σ1∪ Σ2)（充足不可能な節集合，Σ1は ハード節の集合，Σ2はソフト節の集合） 出力： Σ の全ての MCS 1: ΣS2 ← {α ∨ ¬sα| α ∈ Σ2}; // sαは α の選択変数 2: S ← {sα| α ∈ Σ2}; // 選択変数の集合 3: A← ∅; // MSS 候補に対応する選択変数の集合 4: B ← ∅; // MCS 候補に対応する選択変数の集合 5: while true do
6: (st, µ) = SAT (Σ1∪ ΣS2, A); // SAT オラクル
7: if st = T RU E then 8: A← {s | µ(s) = 1, s ∈ S}; 9: B ← {s | µ(s) = 0, s ∈ S}; 10: Σ1⇐ Σ1∪ ( ∨ s∈Bs); // 阻止節 11: else if A =∅ then 12: return 13: else 14: output(B); // BM CSが MCS 15: A← ∅; 16: end if 17: end while 本アルゴリズムは，SAT オラクルが見つけた変数の 値割当てを出発点として MCS を探していく．アルゴ リズム中の A と B は選択変数の集合であり，A に対 応するソフト節の集合{α | µ(sα) = 1}（以降 AM SS） が MSS の候補であり，B に対応するソフト節の集合 {α | µ(sα) = 0}（以降 BM CS）が MCS の候補である． このアルゴリズムでは，SAT オラクルが充足可能を返 す限り，6∼10 行目が繰り返され，B は段々と小さく なり BM CSは MCS に近づいていく．逆に A は段々と 大きくなり AM SSは MSS に近づいていく．10 行目の ∨ sα∈Bsαは，BM CSより大きな集合を以降の MCS の 探索から除外するための節である． SAT オラクルの答えが充足不能なら，その時の BM CS より小さな MCS 候補はない，ことになり，この BM CS が MCS であることわかる（14 行目）．15 行目の A← ∅ は，MSS 候補がない状態から再び探索を始めることを 表す．SAT オラクルの答えが充足不能で A が空なら， もうこれ以上 MCS はないことが分かり，手続きを終 了する（11，12 行目）． ソフト節が単位節である，つまりソフト節の長さが １であるとき，そのソフト節自身で選択変数の代用を することができる．選択変数の数が減るので，処理の 効率化が期待できる．これは，アルゴリズムの 1，2 行 目を次のように変更すればよい． 1: ΣS 2 ← {α ∨ ¬sα| α ∈ Σ2,|α| > 1} ∪ {α | α ∈ Σ2,|α| = 1}; 2: S← {sα| α ∈ Σ2,|α| > 1} ∪ {α | α ∈ Σ2,|α| = 1};
4
計算機実験
Algorithm 1 を SAT ソルバー Glucose3.0 [Audemard 09, E´en 03] を用いて実装した．評価には，[Gr´egoire 18] と 同じ 1090 個のインスタンスを用いた．その内訳は，ソ フト節のみからなるインスタンス（以降 MS）が 493 個，ソフト節とハード節からなるインスタンス（以降 PMS）が 597 個である．
実験には，メモリ 32Gb を有する Intel Xeon E3-1246v6(3.70GHz) プロセッサ上の Ubuntu 18.04 を用 いた．１インスタンス当たりの制限時間と制限メモリ は，[Gr´egoire 18] と同じく，それぞれ，30 分，8Gb と した． 表 1 は，MS，PMS，それぞれのインスタンス当たり の変数の数と節の数の平均を示している．ソフト節に ついては，単位ソフト節の数を内数としてカッコ内に 示した．MS の方が，変数の数，節の数のいずれも平均 的には多いことが分かる．また，PMS のソフト節のほ とんどは単位節であることも分かる． 表 2 に，上記の制限時間及び制限メモリで列挙した MCS の総和，SAT オラクル総数，及びその比を MS， PMS 毎に示した．比較のため [Gr´egoire 18] で提案さ れた MCS 列挙プログラム Enum-ELS-RMR-Cache1の列 挙数も示した．これは，現段階で最も高速に MCS を 列挙するプログラムの一つである．表 3 に，上記の制 限時間及び制限メモリで MCS 列挙が完了したインス タンス数とメモリ不足により計算を打ち切ったインス タンス数を示す． 1http://www.cril.fr/enumcs から入手した．なお，実験で用い た 1090 個のインスタンスも同サイトから入手した． － 3 －
表 1: 変数と節の個数の平均 変数 節の数 の数 ハード節 ソフト節（内，単位節） MS 156,844 0 496,827 (3,030) PMS 16,032 100,134 10,759 (10,758) 表 2: MCS 総列挙数と SAT オラクル総数（単位：千個），及びその比 Enum-ELS- 提案手法
RMR-Cache Basic Basic+Inc USoft USoft+Inc
MS 349,156 59,711 85,297 60,173 80,735 401,598 568,399 865,993 567,967 818,751 (1.15) (9.52) (10.15) (9.44) (10.14) PMS 494,309 295,870 280,603 637,801 627,593 1,023,506 1,187,627 935,170 1,536,802 1,507,640 (2.07) (4.01) (3.33) (2.41) (2.40) 上段：MCS 総列挙数 中段：SAT オラクル総数 下段：中段/上段 提案手法については，４通りの方法で実験を行った． Basic は Algorithm 1 そのもの，USoft は単位ソフト節 については選択変数を導入せずにその単位ソフト節で 選択変数を代用したものを表す．Inc は Glucose のイ ンクリメンタル SAT 解法機能 [Audemard 13] を利用 したことを表す．この機能の働きの第一は，Glucose の 節評価指標 LBD（Literal Block Distance）の計算に選 択変数を使わないようにすることである． 本アルゴリズムでは，ソフト節（Inc では単位節でな いソフト節）の数分だけ選択変数が導入される．そし て SAT オラクルに選択変数の集合が渡され，Glucose ではこれを仮定（assumption）として処理する．この ような処理を行うと，推論中に選択変数を多く含む学 習節が作られ易くなり，そして，そのような節の LBD は大きくなり（評価が下がり）推論に用いられにくく なる．インクリメンタル SAT 解法機能は，このような 状況を回避するために編み出されたものである．上記 の第一の働き以外に，選択変数を多く含む節に関わる BCP（Boolean Constraint Propagation）や仮定に選 択変数を多く含む際のリスタート（restart）の効率化 などを行う． 表 2 より，ほとんどのソフト節が単位節である PMS で，USoft により MCS 総列挙数が倍増しており，この 効果が大きいことが分かる．一方，多くのソフト節が非 単位節である MS では，Inc の効果が現れている．Basic， USoft 共に３∼４割ほど総列挙数が増えている．結果と して，提案手法については，MS に対しては Basic+Inc が，PMS に対して USoft の性能が最も高かった． Enum-ELS-RMR-Cache と MCS の総列挙数を比べる と，MS については Basic+Inc で４分の１，PMS につ いては USoft で 1.3 倍となっており，PMS では優位で あるものの MS での性能差が顕著である．この性能差 の主要因は，MCS を１個得るのに必要な SAT オラク ルの回数の差にあると思われる．この回数が，MS に対 しては提案手法はいずれも 10 回前後であるのに対し， Enum-ELS-RMR-Cache は僅かに 1.15 回であり，桁違い と言っていいほどの差がある．差がこれほど顕著では ない PMS では提案手法が優位であるので，この差を いかに縮めるかが今後の課題である． 表 3 より，メモリ効率の点では Enum-ELS-RMR-Cache に比べ提案手法の方がより明らかに優れていることが 分かる．また，Inc はメモリ消費量を増やす傾向がある ことも分かる．Glucose は，LBD が大きい学習節を適 宜削除しながら推論を進めるが，Inc により選択変数を 多く含む比較的長い学習節も保持されるようになった ためだと推察される．
5
むすび
SAT オラクルを利用して MCS を列挙する手続き を提案し，SAT ソルバー Glucose を用いて実装した． Enum-ELS-RMR-Cache との比較実験では，提案手法は PMS に対しては優位であったが，MS に対しては劣っ ていた．本提案手法は，Enum-ELS-RMR-Cache の手続 きと比べると簡潔である．それにも関わらず，PMS に 対して優位性を示せたことは本手続きの将来性の高さ － 4 －表 3: 列挙完了のインスタンス数とメモリ不足のインスタンス数
Enum-ELS- 提案手法
RMR-Cache Basic Basic+Inc USoft USoft+Inc
MS 52 57 58 56 58 93 2 16 2 13 PMS 191 182 186 193 193 72 0 19 22 28 上段：列挙完了のインスタンス数 下段：メモリ不足のインスタンス数 を示していると思われる．MS に対する性能を向上さ せるには，MCS １個を見つけるのに要する SAT オラ クル回数を減らす必要があり，今後、実験結果を詳細 に分析し，改良手法を考えていきたい．
謝辞
本研究は JSPS 科研費 JP16K00304，JP17K00307 の 助成を受けたものです．参考文献
[Audemard 09] G. Audemard, L. Simon: Predicting Learnt Clauses Quality in Modern SAT Solver, IJCAI-09, pp.399-404, 2009.
[Audemard 13] G. Audemard, J.-M. Lagniez, L. Si-mon: Improving Glucose for Incremental SAT Solving with Assumption: Application to MUS Extraction, SAT 2013, pp.309-317, 2013. [E´en 03] N. E´en, N. S¨orensson: An Extensible
SAT-solver, SAT-03, pp.502-518, 2003.
[Gr´egoire 18] ´E. Gr´egoire, Y. Izza, J.-M. Lagniez: Boosting MCSes Enumeration, IJCAI-18, pp.1309-1315, 2018.
[Koshimura 09] M. Koshimura, H. Nabeshima, H. Fu-jita, R. Hasegawa: Minimal Model Generation with Respect to an Atom Set, FTP 2009, pp.49-59, 2009.
[宋 18] 宋剛秀，番原睦則，田村直之，鍋島英知：SAT ソルバーの最新動向と利用状況，コンピュータソ フトウェア，Vol.35，No.4，pp.72-92，2018．
