SAT
ソルバーの動的対称性除去における候補節削減手法
Candidate Clauses Reduction for Dynamic Symmetry Breaking in
SAT Solving
市澤 拓美
1∗原田 翔規
1鍋島 英知
2Takumi Ichizawa
1Syoki Harada
1Hidetomo Nabeshima
21
山梨大学工学部コンピュータ理工学科
1
Department of Computer Science and Engineering, Faculty of Enginnering, University of
Yamanashi
2
山梨大学大学院医学工学総合研究部
2
Department of Research Interdisciplinary Graduate School of Medicine and Engineering,
University of Yamanashi
Abstract: SAT solvers are now widely used to solve a large variety of problems, especially in field of hardware/software verification. SAT problem often contains symmetries that can be used to shrink the symmetrical search space. Symmetric explanation learning is one of the efficient dynamic symmetry breaking techniques, but it may generate many candidate clauses to reduce symmetric search space, and it requires much memory and computational cost. In this paper, we propose evaluation criteria to measure the usefulness of the candidate clauses and reduction techniques which remove useless candidates. The experimental results show our approach can identify useless candidate clauses and improve the solving speed of solvers.
1
はじめに
SAT 問題では，特に困難な組み合わせ問題において しばしば対称性を示す問題が存在する．対称性は求解 において対称的な探索を促すこととなるため問題中の 対称性を除去することができれば，不必要な対称的な 探索を防ぐことになるため，SAT ソルバーの性能向上 に繋がる．動的対称性除去を行う手法の１つに対称学 習 [1] がある．対称学習は有効な対称性除去手法だが， 対称学習節を生成するために多くの対称学習候補節を 生成するため，多大な候補節によるメモリ消費量の肥 大化や，処理速度の低下が対称学習の課題となってい る．そこで，本論文では，対称性にいくつかの評価尺 度を定義し，それに基づいて対称性の質を決め，対称 性学習候補節の追加を抑制する手法を示す．本手法に よって候補節を大幅に抑制すること可能になり，求解 数は従来手法を維持しつつ，求解速度が向上されるこ とを評価実験によって示す． ∗連絡先： 山梨大学コンピュータ理工学科 〒 400-8511 山梨県甲府市武田 4-3-11 E-mail:[email protected]2
SAT
問題
SAT 問題とは，命題論理式の充足可能性判定問題 のことである．命題論理式とは式のような連言標準形 (Conjunctive Normal Form; CNF) で与えられるもの をいう． (x1∨ x2)∧ (x3∨ x4)∧ ¬x5 (1) それぞれの命題変数もしくはその否定をリテラルと呼 ぶ．リテラルを選言 (∨) で繋げたものを節，節を連言 (∧) で繋げたものを CNF 式と呼ぶ．この CNF 式を 充足させるような論理変数の真偽値割り当てがある場 合，その問題は充足可能 (SAT) と呼び，どのような真 偽値割り当てでも CNF 式が充足しない場合充足不能 (UNSAT) と呼ぶ．2.1
SAT ソルバー
SAT ソルバーは SAT 問題を解くソフトウェアのこ とである．現在の SAT ソルバーでは CDCL ソルバー [2] が主流である．CDCL ではまず単位伝播を行う．単 位伝播とは長さが 1 の節 (単位節) を充足させる戦略で あり，単位節中のリテラルに真を割り当てる．単位伝 人工知能学会研究会資料 SIG-FPAI-B803-05播は SAT ソルバーの処理時間の 7∼9 割を占める重要 な処理である．また，リテラルを割り当てたことによっ て未割り当てのリテラルが 1 つでかつ充足されてない 節にも単位伝播が発生する．この単位伝播を単位節が なくなるまで繰り返す．単位節が存在しなければ，変 数選択を行う．変数選択とは単位伝播が行われなくなっ た際，ヒューリスティックスに基づき変数を選択し割 り当てる行為である．また，単位伝播の最中に，単位 節で x と¬x のように同じ変数に真と偽を両方割り当 てをしなければいけない状況が発生する．これを矛盾 と呼ぶ．その際，同じ矛盾の発生を防ぐために，矛盾 の原因となる変数割り当てを行わないような節を導入 する．この節を学習節という．例えば，矛盾の原因が x1が真，x2が偽という変数割り当てによって起きた場 合，この変数割り当てを行わないすなわち，この変数 割り当ての連言の否定である式 (2) を学習節として追 加する. (¬x1∨ x2) (2) 式 (2) の式によって x1に真が割り当てられたとき，x2 に偽が割り当てられることがなくなる．学習節を原問 題に追加することで同様の矛盾を防ぐことができ探索 空間を削減できる．
2.2
リテラルブロック距離
SAT ソルバー Glucose で導入されたリテラルブロッ ク距離 (Literal Blocks Distance; LBD) と呼ばれ る尺度がある [3]．LBD とは，その学習節を非充足す るために必要となる変数選択の最小回数を表す尺度で ある．LBD の値が小さい節ほど．少ない変数選択で値 が割り当てられるため実質的に制約が強いつまり質の 良い節と言える．たとえ学習節の長さが大きくなって しまっても，LBD が低ければ，質の良い学習節であり， 短い長さの学習節も，LBD が高ければ，質の悪い学習 節となりうる．3
対称性
SAT 問題にはしばしば対称性を示す問題がある．対 称性を持つ問題の 1 つとして，鳩ノ巣問題がある．鳩 ノ巣問題とは n+1 匹の鳩に対して n 個の箱に鳩が入る かという問題である．ただし，一つの箱に鳩は一羽し か入ることが出来ない．図 1 は n=2 とした時の鳩ノ巣 問題である．図 2 は図 1 の問題での全パターンの通り である．この時この問題は箱と鳩それぞれに対して交 換可能すなわち対称性を持つことが言える．この問題 では n 個の箱に n+1 匹の鳩が入るのは論理的に不可能 である. しかし SAT ソルバーでは全ての組み合わせを 試して初めて充足不可能と判断する．対称性を除去す ることができれば対称的な組み合わせを省略すること が可能となり探索空間を削減できる． 図 1: 鳩の巣問題 図 2: 図 1 の巣と鳩の全パターンの組み合わせ3.1
SAT 問題における対称性
SAT 問題における対称性は変数を置換しても論理的 に等価ということを意味する．これを式 (3) で説明する. (x1∨ ¬x3)∧ (x2∨ ¬x3) (3) 式 (3) で x1と x2の変数に着目すると x1と x2を置換し ても問題構造は変わらない. このとき，x1と x2いう対 称性が存在する．この対称性は循環表記を用いて，(x1 x2) と表現する．これは，x1を x2 に，x2を x1に置 換することを表す，また，(x1x2) (x3x4) と記された 場合は，x1を x2に，x2を x1に，なおかつ x3を x4に x4 を x3に 置換することを示す．対称性を用いた節を対称 節と呼ぶ．4
対称性除去
対称性除去というものは対称性の情報から対称的な 探索を見つけ，対称的な探索を防ぐための処理を行う 手法である．除去対称性除去は SAUCY[4] などの対称 性検出ツールを用いて，対称性を検出する．このよう に対称節を選別するのにも手法があり，大きく分けて， 静的対称性除去と動的対称性除去の 2 つの手法がある．4.1
静的対称性除去
静的対称性除去は，SAT 問題を求解する前に，対称 性除去を行う手法である．基本的には対称性除去式と呼ばれる節を元問題に追加する手法が利用される．こ の除去手法は後述の動的対称性除去に比べて，処理自 体は軽いが，検出された対称性に対する対称性除去式 を追加するため，対称性除去式のサイズが大きくなって しまうことが欠点である．静的対称性除去を行うツー ルとして SHATTER[5] や BREAKID[6] がある．
4.2
動的対称性除去
動的対称性除去は，SAT 問題を求解中に．対称性除 去式を構築する手法である．これは SAT 問題求解中に 対称性除去式を構築し元問題に追加したり，単位伝播 を促進するような式を元問題に追加したりと様々な方 法がある．そのため静的対称性除去ではすべての対称 性に対して除去式を追加するのに対し，動的対称性除 去では，探索中に生じた対称的な探索空間を除去する ために，必要に応じて対称性除去を行うため冗長な除 去式を生成せず，またいくつかの動的対称性除去を組み 合わせやすい．しかし，求解処理中に随時，対称性除去 の処理を行うため対称性除去のコストは高い．動的対 称性除去を行う SAT ソルバーとして，SP[7]，SEL[1]， MiniSym[8] などがある．4.3
対称学習
「対称学習 (Symmetric Explanation Learning; SEL)」 は動的対称性除去手法の 1 つのアプローチである [1]． 対称学習の流れを説明する．単位伝播が起きる際に単 位節に対して対称性を適用して対称節を生成する．こ の生成された節を対称学習候補節と呼ぶ．単位伝播す る節にだけ対称性を適用するのは１つのリテラル以外 が全部偽になっているため置換を行なっても偽になっ ているリテラルが多く存在し，単位伝播や矛盾を起こ す可能性が高いからである．このような対称学習候補 節はこのまま学習節として追加しない．この対称学習 候補節は学習節とは別に格納しておき，別の単位伝播 や変数選択によってその対称学習候補節が単位伝播や 矛盾を起こしたとき，対称学習節として学習節集合に 追加される．また，対称学習候補節はバックトラック すると，バックトラックによって割り当てられていた リテラルが未割り当てになったリテラルによって生成 された対称学習候補節は削除される．これによって探 索中に関連する対称節だけを適宜取り出し使用するか 判定している．この手法によって探索に役立つ対称学 習節のみを追加可能かつ対称的な探索を防ぐことがで き，単位伝播が促進される.
4.4
対称学習の欠点
対称学習では対称学習候補節を大量に生成する．特 に矛盾が起きずに単位伝播が促進していくと対称学習 候補節が削減されないため対称学習候補節集合の大き さが多大になってしまう．問題によっては数十億個も 重複を含めて対称学習候補節を生成している．また候 補節は別の探索空間に移動すると削除されるため，何 度も同じ候補節を生成し，それを削除することを繰り 返すことがある．候補節が多ければ多いほどメモリを 消費し，候補節が対称学習節に格納されるか単位伝播 が起きるごとにチェックするので計算コストもかかって しまう．4.5
LBD 値を用いた対称学習
対称学習では対称学習候補節ほどではないが対称学 習節も多く生成してしまう．対称学習節によってもメ モリを消費してしまい，処理が遅くなってしまう．原 田は，対称学習節を LBD 尺度に基づき選別する手法 を示している [8]．この手法では，LBD 値の小さな節 から生成される対称学習節がよく使われる傾向にある ことを実証し，あまり使用されない対称学習節を除去 することを可能にしている．しかし対称学習候補節は 選別しないため，メモリ消費量を大きく削減すること はできていない．5
提案手法
対称学習における対称性学習節削減手法について解 説する．本手法は，対称学習手法を利用する SEL と原 田の LBD 値を用いた対称学習 mySEL を改良し，求解 途中で評価尺度に基づいて対称性の価値を比較し，コ ストが高いが求解に深く関わってない対称性から対称 学習候補節の生成を抑制する手法を実装した．各評価 尺度を占める対称性の割合の小さい順に並べその累積 割合を指定された割合を超えない対称性から対称学習 候補節を生成しないようにした．ここで使用した評価 尺度は以下の 3 つである． 採用率 対称性の採用率とは，その対称性から生成され た対称学習候補節から対称学習節に格上げされ た節の割合をいう．対称学習節をよく生み出す対 称性を重視する尺度であり，計算コストが軽量で ある． LBD を考慮した採用率 採用率では，対称学習節の質 を考慮していない．そのため，原田の LBD によ る対称学習節の削減を利用し，削減されるすなわち質の低い対称学習節を対称学習節の数に含めず に採用率の計算を行う． 使用率 対称性の使用率とは，その対称性から生成され た対称学習節の使用頻度をすべての節の使用頻 度で割ったものである．この尺度はよく使われる 対称学習節を生み出す対称性を重視する尺度で ある． 以上の尺度を用いて，提案手法は問題求解中に以下 の手順を行う． 1. 対称性対称学習候補節数，対称学習節数，節に対 称性情報を保持 2. 対称性候補節が生まれる毎にその対称性の対称学 習候補節数を数え上げ，その対称学習候補節が格 上げされる毎に対称学習節数を数え上げ 3. 対称学習節が 50 万回使用される毎に対称性毎に 以下の処理を行う (a) 対称性毎に評価尺度を計算 (b) 評価尺度を元に昇順に対称性をソート (c) 各尺度における累積相対割合が一定値に満 たない対称性の対称性候補節の生成だけ（対 称性伝播の処理は抑制しない）を抑制 (d) 一度対称性候補節を抑制していた対称性が 累積相対割合が一定値を超えていた場合，対 称性候補節の抑制を解除 4. 1000 秒経過した時に対称学習候補数，対称学習 節数，対称伝播数が 0 回の対称性を削除し，対称 性を再構築 対称性の対称性候補節の抑制を解除する必要性とし ては，時間推移によって対称性の尺度の割合が変化す ることがあるためと，の使用率に至っては，対称性の 使用率の精度が安定するまでに少し時間を要するため， 抑制したあとに精度が安定することによって抑制解除 する対称性がある可能性が高いからである．また，1000 秒経過した後に使用されない対称性を削除することに よって対称性のチェックにかかる処理を削減する．これ は対称性を多数含むものの，そのほとんどが使われな い問題もあるためである．また SAT ソルバーに対称性 情報の入力の段階でメモリを消費し，オーバーフロー してしまうという問題もあった．そのためオーバーフ ローしないように制限を設けた．また求解途中で全く 使用されない対称性は削除するようにした．全く使わ れない対称性を保持していることがメモリ消費すると 考えたからである． 表 1: 問題群における求解数，単位伝播速度，候補節削 減割合 使用ソルバー SEL 採用率 採用率 (LBD) 使用率 求解数 146 147 147 147 PAR2-time 2190058 2192588 2186012 2184728 単位伝播速度 全体 1854139 1958014 2193804 2094437 対称性無 1781101 1738610 1744509 1728388 対称性有 2067745 2205939 2159072 2486663 対称性候補節削減割合 76.5 74.5 74.0
6
実験
本章では，提案手法である対称学習候補節削減手法 を Glucose4.0 をベースとした対称学習 SAT ソルバーで ある SEL に導入し, 比較実験を行なった．実験環境は， Intel Core i5-6600(3.30GHz)，メモリ制限を 8GB, 対称 性検出ツールの制限時間を 1000 秒, 対称性検出ツール を含む制限時間を 5000 秒とした．対称性検出ツールは 逐次的に対称性が出力がされるよう改良した SAUCY と BREAKID の行可換検出手法を使用し，使用した問 題群は SAT competition 2017 である．また，提案手法 において累積相対割合が 10%に満たない対称性から候 補節を生成しないようにし，4GB までの対称性情報を 受け入れた． 本手法は既存の対称学習ソルバー SEL の改良である ため，SEL との性能比較を行った．性能比較する対象 として，求解数，PAR2-time，単位伝播速度，対称性候 補節削減割合，メモリ消費量で比較した．PAR2-time は制限時間内に解けなかった問題にペナルティを設け た際の総求解時間である．単位伝播速度は平均単位伝 播速度を示しており単位伝播速度が早いほど性能がよ い．ままた，対称性候補節削減割合は SEL で生成され た対称学習候補節をどのぐらい削減したかを示してい る．対称性のない問題や対称性が少ないなどで提案手 法を用いて対称学習候補節を削減していない問題は考 慮していない．6.1
実験結果
表 1 は各評価尺度における求解数，PAR2-time，単 位伝播速度，対称性候補節削減割合である． 表 1 が各評価尺度に基づく求解性能と候補節削除割 合と平均単位伝播速度を示す. 単位伝播速度については 全体が今回使用した問題全てにおける値であり，対称 性有が対称性が 1 つ以上検出できた問題，対称性無が 対称性が 1 つも検出できなかった問題である. また図 1 は対称性のある問題でのメモリ使用量であり，メモリ 使用量は問題中で一番メモリを消費した値を昇順に並 べたもので，増加量が少ない方がメモリを消費してい ないということとなる．これらを比較すると使用率，採図 3: 問題群におけるメモリ使用量の比較 用率，LBD を考慮した採用率で見ても候補節を大幅に 削減しているものの求解数は低下していない．また候 補節を削減したことで候補節の参照が少なくなったこ とより単位伝播速度が対称性がある問題だけで約 17%， 全体で見ても約 11.5%速度が向上している．しかしメ モリ消費量は候補節削減手法では抑えることができず， 入力に制限をかけたため制限より大きい対称性を含む 問題だけがメモリ消費を抑えることができている．ま た，節の質を考慮していない採用率よりも節の質を考 慮した LBD を考慮した採用率，使用率の方が単位伝播 速度は早くなっている．
6.2
考察
提案手法はいずれも単位伝搬速度の向上ができてい る．理由としては提案手法により対称性候補節を大幅 に削減したことによって対称性処理が少なくなったた めだと考えられる．しかし，単位伝播速度は向上した のも関わらず求解数が向上しなかった．原因は，時間経 過による評価尺度の変化が挙げられる. 図 2，3 は対称 性毎の経過時間による使用率の変化である．図 2 は時 間経過によって対称性の使用率が変化していない．こ のような問題では提案手法による性能向上が期待でき る．しかし，図 3 のような時間経過によって対称性の使 用率が変化しているともし使用率が低くある時間で急 に使用率が上がる対称性がある場合，使用率が上がる 前にその対称性による対称性候補節を削減してしまう と使用率をあげるような対称性候補節を消してしまい 対称性の使用率が上がらなくなってしまう．そのため 再度この対称性から対称性候補節がまた生成されるよ うな機会があっても結果的に使用率が低いままになっ てしまうので，その対称性から対称学習候補節が生成 されなくなってしまう．そのため質が良い節も削減し 図 4: 対称性の時間経過で使用率が変化しない使用率 の推移 図 5: 対称性の時間経過で使用率が変化する使用率の 推移 てしまっているため，SAT ソルバーの探索速度が落ち， 求解数は向上しなかった． また，メモリ消費量についてだが，メモリを消費し すぎる問題には制限をつけたため，その制限によって メモリ消費量が削減したが，提案手法ではほぼメモリ 消費を削減出来ていない．これは，質の良い節を削減 してしまっているため，探索の削減が減少し，探索時 間が増え，探索時間が増えると結果的にメモリを消費 してしまう．そのため，評価尺度が時間経過で変化し ない問題ではメモリ消費量が落ちたが，評価尺度が時 間経過で変化する問題では質の良い節を多く削減して いる可能性があるため，問題によってはメモリ消費量 が上昇している．7
今後の課題
提案手法により，時間経過による評価尺度の変化が ない問題には有効だが変化があるような問題では有用 とは言えないことがわかった．そのため今後の課題と して，時間経過による評価尺度の変化に対応可能にす ることである．しかし純粋なアルゴリズムでは計算コ ストがかかってしまう．そのため，１つの案として質 の悪い対称性から対称性候補節を全て削減するのでは なく，ランダムでいくつか取り出し，ランダムで取り 出した節が多く使用された際に，その対称性から一定 期間候補節を全て生成させ，あるタイミングでその対 称性の評価尺度を再計算する．これによって使用率が 大きく変化するような対称性は復帰させることが期待 できる．8
まとめと今後の課題
対称学習は対称性除去において有効な手法だが，対 称学習候補節が多く生成されるため，メモリ消費や対 称性候補節のチェックにより，求解性能が落ちている問 題もある. そこで，追加される対称学習候補節をいくつ かの評価尺度を基に抑制する手法を提案したが，単位 伝搬速度の向上は達成できたものの，求解数の向上ま でには至らなかった．提案手法では，時間経過による 使用率の変化をあまり考慮してないため，質が良くな るような対称性から対称学習候補節が生成されないこ とがある. 今後の課題として，時間経過による評価尺度 の変化に対応可能にすることである．しかし単純に使 用率の変化を参照しようとすると計算コストがかかっ てしまう．そのため，１つの案として質の悪い対称性 から対称性候補節を全て削減するのではなく，ランダ ムでいくつか取り出し，ランダムで取り出した節が多 く使用された際に，その対称性から一定期間候補節を 全て生成させ，あるタイミングでその対称性の評価尺 度を再計算する．これによって使用率が大きく変化す るような対称性は復帰させることが期待できる．参考文献
[1] Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Symmetric explanation learn-ing: Effective dynamic symmetry handling for SAT.Theory and Applications of Satisfiability Testing - SAT 2017. pp 83-100 (2017).
[2] Silva, J. P. M. and Sakallah, K. A.: GRASP : A Search Algorithm for Propositional Satisfia-bility,IEEE Transactions on Computers, Vol. 48, pp.506-521 (1999)
[3] G.Audemard, L.Simon.:Predicting Learnt Clauses Quality in Modern SAT Solvers. IJCAI’09 Pro-ceedings of the 21st international jont conference on Artifical intelligence . pp. 399-404 (2009). [4] McKay, B.D., Piperno, A.: Practical graph
iso-morphism, II. Journal of Sym- bolic Computation 60(0), pp. 94 - 112 (2014).
[5] Aloul, F.A., Sakallah, K.A., Markov, I.L.: Effi-cient symmetry breaking for Boolean satisfiabil-ity. IEEE Transactions on Computers 55(5), pp. 549-558 (2006).
[6] Devriendt, J., Bogaerts, B., Bruynooghe, M., De-necker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016. pp. 104-122 (2016) .
[7] Devriendt, J., Bogaerts, B., De Cat, B., Denecker, M., Mears, C.: Symmetry pr opagation: Improved dynamic symmetry breaking in SAT. In: IEEE 24th International Conference on Tools with Ar-tificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9. pp. 49-56(2012).
[8] CDCLSym:Introducing Effective Symmetry Breaking in SAT Solving. Haken Metin,Souheib Baarir,Maximilien Colange,Fabrice Kor-don:TACAS(1) 2018: 99-114
[9] 原田 翔規 (2017)，SAT ソルバーにおける対称性学 習節の削減手法の提案.:山梨大学工学部コンピュー タ 理工学科卒業論文 (2017)
