ブール基数制約を経由した擬似ブール制約のSAT符号化法

ブール基数制約を経由した擬似ブール制約の

SAT

符号化法

A SAT Encoding of Pseudo-Boolean Constraints via Boolean

Cardinality Constraints

南 雄之

1∗

宋 剛秀

2

番原 睦則

2

田村 直之

2

Yushi Minami

1

Takehide Soh

2

Mutsunori Banbara

2

Naoyuki Tamura

2

1

_{神戸大学大学院システム情報学研究科}

1

_{Graduate School of System informatics, Kobe University}

2

_{神戸大学情報基盤センター}

2

_{Information Science and Technology Center, Kobe University}

Abstract: SAT (Satisfiability) is a problem of deciding the satisfiability of a given propositional

formula, and several extensions of SAT problems are also proposed. PB (Pseudo-Boolean) problem is a problem of deciding the satisfiability of a set of PB constraints, which are linear constraints over propositional variables. PB problem is thus an extention of the SAT problem. Since the enormous progress of SAT solvers which are programs solving SAT problems, encoding of PB constraints into SAT problems is actively studied and many methods have been proposed. In this paper, we propose a new SAT encoding method of PB constraints. The main feature is that it uses Boolean Cardinality (BC) constraints as an intermediate form while encoding PB into SAT. BC constraints are PB constraints whose coefficients are all 1, and some effective SAT encoding are known. Using BC constraints, it is thus expected that the realization of an effective SAT encoding methods of PB constraints. In experiments, we compared the proposed encoding methods with existing methods using benchmark instances of PB.

1

はじめに

SAT (Satisfiability)とは，与えられた命題論理の式 の充足可能性を判定する問題である [6]．SAT 問題を拡 張した問題も様々提案されている．本論文で対象とす る擬似ブール (Pseudo-Boolean; PB) 制約は命題変数 上の線形制約であり，PB 制約集合の充足可能性を判定 する問題は SAT 問題の拡張になっている． SAT問題を解くプログラムである SAT ソルバー [8] の性能が飛躍的に向上していることを背景として PB 問題を SAT 問題に符号化する研究が活発に行われてお り，数多くの手法が提案されている [10, 5, 13, 9, 11]． 本論文では，PB 制約集合を SAT 問題に符号化する 新しい手法を提案する．提案手法の特徴は，ブール基 数 (Boolean Cardinality; BC) 制約を経由した変換を 行う点である．BC 制約は係数が 1 の PB 制約であり， 効果的な SAT 符号化手法が知られている [12, 2]．BC 制約を介することで，より優れた PB 制約の SAT 符号 化の実現が期待できる． ∗_{連絡先：神戸大学情報基盤センター} 〒 657-8501 兵庫県神戸市灘区六甲台町 1-1 E-mail：[email protected] 図 1: 提案手法の概要 提案手法の流れは以下の通りである (図 1 参照)． 1. PB制約を接頭和表現という PB 制約中の同一係 数の項をまとめた表現に変換する (3.1 節)． 2. 接頭和表現を順序符号化を用いて BC 制約の連言 標準形式（BC-CNF 式）へ符号化する (3.2 節)． 3. BC-CNF式から，BC リテラル間の関係を利用し て，不要な BC リテラルと BC 節の除去を行う (3.3節)． 人工知能学会研究会資料 SIG-FPAI-B506-04

4. BC-CNF式を，BC 制約の SAT 符号化の 1 つであ るシーケンシャルカウンタ法 [12] を用いて SAT 問題に符号化する (3.4 節)． 以下，SAT，PB 制約，BC 制約について説明した後， 提案手法について上記に示した流れに沿って説明する． その後，PB のベンチマーク問題を用いて既存手法との 比較評価を行う．

2

SAT, PB

制約

, BC

制約

命題変数 p およびその否定 p をリテラル (literal) と 呼ぶ．複数のリテラルの選言 (OR) を節 (clause) と呼 び，複数の節の連言 (AND) を CNF式 (Conjunctive Normal Form formula)と呼ぶ．

与えられた CNF 式を真にする命題変数への値割当

てが存在するか否かを判定する問題を SAT問題と呼

ぶ [6]．値割当てが存在する場合，CNF 式は充足可能 (satisfiable; sat) であると言い，存在しない場合，充 足不能 (unsatisfiable; unsat) であると言う．SAT ソ ルバーは，与えられた CNF 式が sat か unsat かを判 定し，sat ならその解となる値割当てを返すプログラ ムである [8, 4, 1, 7]． 命題変数上の線形制約である擬似ブール制約 (PB 制 約) は，以下のように定義される． 定義 1 (PB 制約). xiがリテラル，aiおよび c が整数 定数， が関係演算子 (=, ≤, ≥) の時，以下の式を PB 制約と呼ぶ． n ∑ i=1 aixi c 項 aixi で係数 aiが負の場合，その項を−aixi+ ai に置き換えることで，係数を正にできる．また，項の 順序を入れ換えることで，PB 制約の左辺は係数の降順 に項が並んでいるとしても一般性を失わない．すなわ ち，以下では a1≥ a2≥ · · · ≥ an > 0を仮定する．さ らに，特に必要がない限り関係演算子 が ≥ の場合に ついて議論し，≤ や = の場合の説明は省略する． 係数が全て 1 の PB 制約をブール基数制約 (BC 制 約) と言う．複数の BC 制約の選言を BC 節と呼び，複 数の BC 節の連言を BC-CNF式と呼ぶ．また，BC 節 に含まれる BC 制約を BCリテラルと呼ぶことがある．

3

提案手法の説明

3.1

PB

制約の接頭和表現への変換

PB制約に対し，その接頭和表現を導入する． 定義 2 (接頭和表現). ∑ni=1aixic を PB 制約とする． この時，各 x1+ x2+· · ·+xiを接頭和と呼び，以下の式 を元の PB 制約の接頭和表現と呼ぶ (ただし an+1= 0 とする)． n ∑ i=1 (ai− ai+1) (x1+ x2+· · · + xi) c すなわち，PB 制約∑n_i=1aixi c に対し，biと si を以下のように定めた時，接頭和表現は∑n_i=1bisi c と表せる． bi= ai− ai+1 si= x1+ x2+· · · + xi ここで a1 ≥ a2 ≥ · · · ≥ an > 0より，bi ≥ 0 である． また 0≤ xi≤ 1 より，0 ≤ si ≤ i である． 例 1. 以下に PB 制約とその接頭和表現の例を示す． 5x1+ 3x2+ 3x3+ 3x4+ 3x5+ x6≥ 9 2s1+ 2s5+ s6≥ 9 このように PB 制約中の同一係数の項がまとめられ，接 頭和表現での項数は少なくなる．

3.2

接頭和表現の BC-CNF 式への符号化

接頭和表現は，順序符号化 [14, 13] を用いることで， 接頭和に対する比較式に分解できる．すなわち，接頭 和表現を BC-CNF 式に符号化することが可能である． 例 1 に示した接頭和表現 2s1+ 2s5+ s6≥ 9 を用い て説明する．この式から s1と s5が 0, 1 の値と 0 から 5の値を取ることを考慮することで，以下の式が得ら れる． (s1≥ d1+ 1)∨ (s5≥ d5+ 1)∨ (s6≥ 9 − 2d1− 2d5) (∀d1∈ {0, 1}, ∀d5∈ {0, 1, . . . , 5}) それぞれの式は，s1= d1かつ s5= d5の場合における s6の条件を表している． s6≥ 9 − 2d1− 2d5が恒真になる場合は削除でき，充 足不能になる場合は s1と s5の条件を 1 通りだけ残せ ば良い．整理すると，以下の 8 個の BC 節が得られる． C1: (s1≥ 1)∨(s5≥ 2) C2: (s1≥ 1)∨(s5≥ 3)∨(s6≥ 5) C3: (s1≥ 1)∨(s5≥ 4)∨(s6≥ 3) C4: (s1≥ 1)∨(s5≥ 5)∨(s6≥ 1) C5: (s5≥ 1) C6: (s5≥ 2)∨(s6≥ 5) C7: (s5≥ 3)∨(s6≥ 3) C8: (s5≥ 4)∨(s6≥ 1)

しかし，この方法では接頭和間の関係が考慮されて おらず，無駄な BC 節が生成されている．接頭和 si間 の大小関係を考慮すれば，大幅に節数を削減できる． 例えば C3: (s1≥ 1) ∨ (s5≥ 4) ∨ (s6≥ 3) を見てみ る．この節は s1= 0かつ s5= 3の場合の s6の条件を 表している．しかし，s5= 3と接頭和間の関係 s6≥ s5 より s6≥ 3 は恒真になる．したがって，この節は削除 できる．同様に C4, C8も削除できる． また C2 : (s1 ≥ 1) ∨ (s5 ≥ 3) ∨ (s6 ≥ 5) を見ると， s5 = 2の時，s6 ≥ 5 は充足不能である．したがって s6≥ 5 の BC リテラルは削除でき，(s1≥ 1) ∨ (s5≥ 3) となる．さらに，この節は C1を含意しているから，節 C1は削除できる．同様に，C6は s5≥ 2 となり，この 節は C5を含意しているから，節 C5を削除できる． 以上の処理を順序符号化アルゴリズムに組み込むこ とによって，大幅な節削減を実現できる． 例 2. 例 1 に示した接頭和表現 2s1+ 2s5+ s6≥ 9 に 適用した場合，以下の 3 個の BC 節に符号化される． C2: (s1≥ 1) ∨ (s5≥ 3) C6: (s5≥ 2) C7: (s5≥ 3) ∨ (s6≥ 3)

3.3

BC-CNF

式の簡単化

前節では，順序符号化法を改良したアルゴリズムに ついて述べ，大幅な節数削減が実現できることを示し た．しかし，まだ無駄な BC リテラルや BC 節が存在 する． 本節では，より一般的に BC 節から不要な BC リテラ ルを除去する方法，および BC-CNF 式から不要な BC 節を除去する方法について述べる． 命題 1. ∑ni=1bisi ≥ c を PB 制約の接頭和表現とする． BCリテラル si≥ a, sj ≥ b について，si≥ a ⇒ sj≥ b が成り立つ必要十分条件は (i ≤ j ∧ a ≥ b) ∨ (i ≥ j∧ i − a ≤ j − b) で与えられる． この命題を用いることで不要な BC リテラルの除 去を実現できる．すなわち，BC 節中に BC リテラル si≥ a, sj ≥ b が含まれており si≥ a ⇒ sj ≥ b が成り 立つ時，その BC 節から BC リテラル si≥ a を除去で きる． 例 3. 例 2 の BC-CNF 式に対して，BC リテラル除去 の処理を実行すると，BC 節 C7: s5≥ 3 ∨ s6≥ 3 にお いて，s5≥ 3 ⇒ s6≥ 3 より BC リテラル s5≥ 3 を除 去できる． C2: (s1≥ 1) ∨ (s5≥ 3) C6: (s5≥ 2) C7: (s6≥ 3) 命題 2. ∑ni=1bisi ≥ c を PB 制約の接頭和表現とす る．BC 節 C, C′について，C⇒ C′が成り立つ必要十 分条件は∀l ∈ C ∃l′∈ C′(l⇒ l′)で与えられる． この命題を用いることで不要な BC 節の除去を実現 できる．すなわち，BC-CNF 式中に BC 節 C, C′が含 まれており C ⇒ C′が成り立つ時，その BC-CNF 式 から BC 節 C′を除去できる． 例 4. 例 3 の BC-CNF 式に対して，BC 節除去の処理 を実行すると，C7⇒ C6より BC 節 C6を除去できる． C2: (s1≥ 1) ∨ (s5≥ 3) C7: (s6≥ 3)

3.4

BC-CNF

式の SAT 符号化

BC制約を SAT に符号化する良い手法のうちの 1 つ として知られているシーケンシャルカウンタ法 [12] を 用いると，接頭和表現から得られた BC-CNF 式を容易 に SAT 符号化できる．_∑ n i=1bisi≥ c を PB 制約の接頭和表現とする．si≥ aを意味するブール変数 si,a を導入し，シーケンシャ ルカウンタ法により以下のような SAT 節を生成する． p1∨ ¬s1,1 si,a∨ ¬si+1,a+1 (1≤ a ≤ i < n)

si,a∨ pi+1∨ ¬si+1,a (1≤ a ≤ i < n)

この時，∑n_i=1bisi≥ c を符号化した BC-CNF 式に おいて，各 BC リテラル si ≥ a をブール変数 si,aで置 き換えれば良い． 例 5. 例 4 の BC-CNF 式を SAT 符号化すると，以下 の CNF 式が得られる． C2: s1,1∨ s5,3 C7: s6,3 すなわち PB 制約 5x1+3x2+3x3+3x4+3x5+x6≥ 9 は，ブール基数制約 x1+ x2+· · · + x6 ≥ 3 をシーケ ンシャルカウンタ法で符号化した節と，上記の 2 節に SAT符号化できる．

3.5

PB

制約の係数の 2 進化

PB制約∑aixi ≥ c の係数 aiがすべて異なってい る場合，その接頭和表現の項数が最大となり，符号化 した BC-CNF 式の節数が膨大になる． そこで，PB 制約の係数を 2 のべき乗に変換 (PB制 約の係数の 2 進化) することで接頭和表現の項数を削 減する．たとえば PB 制約中に項 11x1が現れていた場

表 1: 係数の 2 進化無しと有りの場合の BC 節数 n 無し 有り 3 2 2 4 2 2 5 3 3 6 5 5 7 8 7 8 14 14 9 23 19 10 40 23 11 70 27 12 124 33 13 221 50 n 無し 有り 14 397 65 15 722 103 16 1314 206 17 2410 303 18 4441 410 19 8220 518 20 15272 612 21 28460 812 22 53222 998 23 99820 1319 24 187692 1465 合，係数 11 を 2 進化し 8x1+ 2x1+ x1と変換する．こ のような変換を行うと，PB 制約の項数は増えるが，係 数が 2 のべき乗だけの形となり，接頭和表現の項数が 少なくなることが期待できる． 例 6. PB 制約 10x1+ 9x2+ 8x3+· · · + x10≥ 28 の接 頭和表現は s1+ s2+ s3+· · · + s10≥ 28 で，項数は 10 である．一方，係数を 2 進化した PB 制約 8x1+ 8x2+ 8x3+ 4x4+ 4x5+ 4x6+ 4x7+ 2x1+ 2x4+ 2x5+ 2x8+ 2x9+ x2+ x4+ x6+ x8+ x10 ≥ 28 の接頭和表現は 4s3+ 2s7+ s12+ s17≥ 28 で，項数は 4 になる．前者 を符号化した BC-CNF 式の BC 節数は 40 だが，後者 の BC 節数は 23 になり，BC 節数はかなり少なくなる． 表 1 は，係数が各々異なる PB 制約∑n_i=1(n− i + 1)xi≥ ⌊n(n + 1)/4⌋ + 1 を係数の 2 進化無しの場合と 有りの場合で，それぞれ BC-CNF 式へ符号化した時の BC節数を計測したものである．この PB 制約では，2 進化を行わない場合に比べ，2 進化を行った場合は大 幅に改善されている．

4

実験と評価

ここまで 3.1 節から 3.4 節までで，BC 制約を経由し た PB 制約の SAT 符号化法について説明した．また， 3.5節では，係数の 2 進化による BC 節数の削減につい て説明を行った． 本節では，まず係数の 2 進化を用いる場合と用いな い場合の 2 つの提案手法について BC 節数の比較を行 い，次に提案手法の中でより優れていた係数の 2 進化 を用いた手法と，既存手法として論文 [5] に記述されて いる，BDD 法, Adder 法, Sorter 法の 3 つの求解性能 と SAT 符号化節数を比較した．ベンチマーク問題は， 国際 PB ソルバー競技会 (PB Competition) における DEC-SMALLINT-LINの問題の各シリーズの中から数問 表 2: 係数の 2 進化による BC 節の削減率 シリーズ名 削減率 fpga (10) 1.00 army (5) 1.00 caixa (1) 1.00 dbst (15) 0.76 heinz (4) 1.97 lopes (10) 1.00 oliveras-j (20) 0.85 シリーズ名 削減率 pigeon (10) 1.00 ppp (6) 1.00 robin (5) 1.00 tsp (10) 0.59 uclid (28) 1.00 vdw (5) 1.00 wnqueen (10) 0.01 ずつランダムに選択して構成した 139 問を使用した．内 訳は次のようになる：fpga (10)；army (5)；caixa (1)； dbst (15)；heinz (4)；lopes (10)；oliveras-j (20)； pigeon (10)；ppp (6)；robin (5)；tsp (10)；uclid (28)；vdw (5)；wnqueen (10)．

実験では各手法によって符号化された SAT 問題を

MiniSat [3]を用いて求解し CPU 時間を計算した．計

算機には CPU に Intel Xeon 3.00GHz, メモリ 16GB を搭載したマシンを用いた．

4.1

PB

制約の係数の 2 進化の評価

表 2 は，係数の 2 進化による BC 節の削減の効果を 表したものである．表の列は係数の 2 進化を行わない 場合の BC 節の数を 1 とした場合の比率の平均である． シリーズ毎に見ると，係数の 2 進化により，BC 節数の 削減ができた問題シリーズは dbst，oliveras-j，tsp， wnqueenであり，削減の比率の平均はそれぞれ，0.76， 0.85，0.59，0.01 であった．しかし，heinz では節数 が増加した．理由は，heinz の問題には，2 進数にする と 1 となるビットが多い係数がほとんどの PB 制約が あり，2 進化を行うと接頭和表現の項数が多くなるか らだと考えられる． 以下の表は，2 進化を行わない場合と行う場合につ いて，3 節で説明した提案手法の符号化の各段階にお いて，制限時間 1800 秒以内に処理が完了した問題の数 を記載している． 接頭和 BC-CNF式 簡単化 SAT符号化 無し 139 137 124 124 有り 139 139 139 139 係数の 2 進化を行った場合は，139 問全ての問題で符 号化処理が完了した．一方，係数の 2 進化を行わない 場合は BC 節符号化や簡単化の段階で，制限時間超過， もしくはメモリ容量超過により処理が完了しなかった． このことから，係数の 2 進化は BC 節数の削減の有効 な手法と言える．

表 3: 提案手法と既存手法の SAT 符号化節数の比較 (BDD 法を 1 とした場合) シリーズ名 提案手法 BDD Adder Sorter fpga (10) 0.89 1.00 1.97 1.43 army (5) 0.83 1.00 0.58 0.99 caixa (1) 1.00 1.00 1.00 1.00 dbst (15) 5.90 1.00 1.73 5.48 heinz (4) 2.09 1.00 1.83 2.21 lopes (10) 1.46 1.00 1.03 1.47 oliveras-j (20) 9.47 1.00 1.19 1.78 シリーズ名 提案手法 BDD Adder Sorter pigeon (10) 0.92 1.00 1.62 1.38 ppp (6) 1.23 1.00 1.54 1.78 robin (5) 0.79 1.00 1.36 3.80 tsp (10) 1.69 1.00 0.86 2.44 uclid (28) 3.50 1.00 2.10 2.74 vdw (5) 1.03 1.00 1.04 1.03 wnqueen (10) 1.97 1.00 0.65 2.20 表 4: 提案手法と既存手法の解けた問題数と平均 CPU 時間の比較 シリーズ名 提案 BDD Adder Sorter fpga (10) 8 0.65 8 1.80 8 0.89 8 0.70 army (5) 4 205.07 4 225.67 4 3.90 5 228.64 caixa (1) 1 <0.1 1 <0.1 1 <0.1 1 <0.1 dbst (15) 15 95.39 15 41.05 8 389.66 15 197.65 heinz (4) 2 68.81 2 104.84 2 462.58 2 65.09 lopes (10) 10 52.15 10 42.60 10 102.80 10 178.03 oliveras-j (20) 18 1.97 18 0.13 18 0.93 18 0.64 pigeon (10) 4 146.17 4 480.51 4 481.96 4 478.63 ppp (6) 4 504.41 4 38.66 5 92.31 6 241.42 robin (5) 2 3.29 2 17.20 2 33.75 2 22.37 tsp (10) 10 22.97 10 3.62 10 4.68 10 9.28 uclid (28) 28 25.41 28 23.71 28 82.15 28 32.02 vdw (5) 2 652.82 2 284.41 1 61.76 2 253.83 wnqueen (10) 10 8.92 10 5.71 10 94.96 10 6.10 Total 118 1788.03 118 1269.91 111 1812.33 121 1714.4

4.2

提案手法と既存手法の比較評価

本節では，係数の 2 進化表現を用いた提案手法と論 文 [5] に記述された，BDD 法, Adder 法, Sorter 法 の 3つの既存手法を，SAT 符号化節数，求解できた問題 数，求解時間で比較し，評価を行う． 既存手法との節数の比較 表 3 は，各手法の SAT 符 号化節数を BDD 法の SAT 符号化節数を 1 とした場合 の比率の平均で比較した結果である．表より提案手法 は fpga, pigeon, robin において，他の手法より SAT 符号化節数が少なくなった．理由としてこれらの問題 の PB 制約は全て BC 制約となっており，BC-CNF 式 の BC 節数が少なく，SAT 節数がシーケンシャルカウ ンタの部分のみになるからだと考えられる．しかし， oliveral-j, dbst, などでは BDD 法と比較して，節 数が大幅に多くなった．理由としては，問題の中に殆 どの項の係数が異なる PB 制約が多く，接頭和表現の 項数が多くなったことが考えられる． 既存の手法との解けた問題数と平均 CPU 時間の比較 表 4 は，各手法を解けた問題数と平均 CPU 時間で比 較した結果である．解けた問題数が最も多いもの，ま た解けた問題数が同じ場合は平均 CPU 時間が最も短 いものを太字にしている． 表より，提案手法で解けた問題数は他手法とほぼ同 じであり，匹敵する性能を示している．また，提案手法 は fpga, pigeon, robin において，他の手法より求解 数や平均 CPU 時間において，良いことが分かった．高 速化の理由として，上述したように，これらの問題シ リーズは提案手法の符号化節数が他の既存手法より小 さくなることが挙げられる．しかし，ppp は他の手法 と比較して，結果が特に悪く改良の余地があると考え られる．理由として，上述したように，問題の中に，2 進化を行うことで接頭和表現の項数が大きくなるよう な PB 制約が存在することが考えられる．実際，2 進化 しない提案手法では，解けた問題数は 4 問で平均 CPU 時間は 40.97 秒であった．

5

結論

本論文では，BC 制約を経由した PB 制約の新しい SAT符号化手法を提案した．提案手法では，与えられ た PB 制約の接頭和表現を求め，順序符号化を改良し たアルゴリズムを用いて BC-CNF 式に符号化し，さら に無駄な BC リテラルと BC 節を除去した後，シーケ ンシャルカウンタ法を用いて SAT 符号化を行っている． このように BC 制約を経由した SAT 符号化を実現した 点が提案手法の特徴である．さらに，多くの場合につ

いて，PB 制約の係数を 2 進化することでより小さな BC-CNF式が得られ，符号化時間と使用メモリを削減 できることを示した． 国際 PB ソルバー競技会のベンチマーク中から選択 した 139 問について，提案手法を既存手法の BDD 法， Adder法，Sorter 法と比較したところ，解けた問題数 は他手法とほぼ同じであり，匹敵する性能が得られた． 今後の課題としては，2 進化を行わない方が節数， CPU時間が良くなる場合が存在したので，符号化す る PB 制約によって 2 進化を行うか，行わないかの選 択をできるようにすることや，2 進化ではなく，他の数 字のべき乗に PB 制約の係数を変換する手法の実験な どが挙げられる．

参考文献

[1] Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In

Proceedings of the 21st International Joint Con-ference on Artificial Intelligence (IJCAI 2009),

pp. 399–404, 2009.

[2] Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of Boolean cardinality constraints. In Proceedings of the 9th International Joint

Conference on Principles and Practice of Con-straint Programming (CP 2003), LNCS 2833, pp.

108–122, 2003.

[3] Niklas E´en and Niklas S¨orensson. An extensible SAT-solver. In Proceedings of the 6th

Interna-tional Conference on Theory and Applications of Satisfiability Testing (SAT 2003), LNCS 2919,

pp. 502–518, 2003.

[4] Niklas E´en and Niklas S¨orensson. MiniSat: A SAT solver with conflict-clause minimization. In

Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Test-ing (SAT 2005), LNCS 3569, pp. 502–518, 2005.

[5] Niklas E´en and Niklas S¨orensson. Translating pseudo-Boolean constraints into SAT. Journal

on Satisfiability, Boolean Modeling and Compu-tation, Vol. 2, No. 1-4, pp. 1–26, 2006.

[6] 井上克巳, 田村直之. SAT ソルバーの基礎. 人工

知能学会誌, Vol. 25, No. 1, pp. 57–67, 2010. [7] Hidetomo Nabeshima, Koji Iwanuma, and

Kat-sumi Inoue. GlueMiniSat 2.2.8. In Proceedings

of SAT Competition 2014, pp. 35–36, 2014.

[8] 鍋島英知, 宋剛秀. 高速 SAT ソルバーの原理. 人

工知能学会誌, Vol. 25, No. 1, pp. 68–76, 2010. [9] Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa,

Miyuki Koshimura, and Hiroshi Fujita. Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In 2013

IEEE 25th International Conference on Tools with Artificial Intelligence, Herndon, VA, USA, November 4-6, 2013, pp. 9–17, 2013.

[10] Tobias Philipp and Peter Steinke. PBLib - A library for encoding pseudo-Boolean constraints into CNF. In Proceedings of the International

Conference on Theory and Applications of Satis-fiability Testing (SAT 2015), pp. 9–16, 2015.

[11] Masahiko Sakai and Hidetomo Nabeshima. Con-struction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers.

IEICE Transactions, Vol. 98-D, No. 6, pp. 1121–

1127, 2015.

[12] Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In

Proceed-ings of the 11th International Joint Conference on Principles and Practice of Constraint Pro-gramming (CP 2005), LNCS 3709, pp. 827–831,

2005.

[13] Naoyuki Tamura, Mutsunori Banbara, and Take-hide Soh. PBSugar: Compiling pseudo-boolean constraints to SAT with order encoding. In

Pro-ceedings of the 25th IEEE International Confer-ence on Tools with Artificial IntelligConfer-ence (ICTAI 2013), IEEE, pp. 1020–1027, November 2013.

[14] Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear CSP into SAT. Constraints, Vol. 14, No. 2, pp. 254–272, 2009.