混合基数を用いた擬似ブール制約のSAT符号化

混合基数を用いた擬似ブール制約の

SAT

符号化

A SAT Encording of Pseudo-Boolean Constraints based on Mixed

Radix

上村 直輝

1∗

_{藤田 博}

2

_{越村 三幸}

2

_{査 澳龍}

1

Naoki Uemura

1

_{Hiroshi Fujita}

2

_{Miyuki Koshimura}

2

_{Aolong Zha}

1

1

_{九州大学大学院システム情報科学府}

1

_{Graduate School of Information Science and Electrical Engineering}

2

_{九州大学大学院システム情報科学研究院}

2

_{Faculty of Information Science and Electrical Engineering}

Abstract: Weighted Partial MaxSAT (WPMS) is a generalization of Satisfiability problem. Many

optimization problems can be reduced to WPMS in polynomial time. So it is important to develop MaxSAT solvers. Pseudo-Boolean constraints plays an important role in solving MaxSAT. In this paper, we propose Mixed Radix Weighted Totalizer (MRWTO). MRWTO is based on Weighted Modulo Totalizer (WMTO). MRWTO use less variables and clauses than it. Our experimental results show the effectiveness of this methods.

1

はじめに

重み付き部分 MaxSAT 問題 (WPMS) とは，重みを 与えられた CNF 式 (節集合) に対して充足できない節 の重みの最小値を求める最適化問題である．様々な組 合せ最適化問題は WPMS 問題に多項式時間で変換が 可能であるため，このような問題を解く MaxSAT ソル バーを高速化することは重要である．WPMS の解法と しては，SAT ソルバーを利用して解を求める手法が主 流である．高性能汎用 SAT ソルバーは CNF 式のみを 入力として受容するのが通常であるため，利用するに あたって重みに関する情報を CNF 式に符号化する必 要がある (PB 制約符号化)．PB 制約符号化の効率化を 行うことにより MaxSAT ソルバーの性能を向上させる ことが可能となる． 既存の PB 制約符号化手法の一つに Weighted Mod-ulo Totalizer(WMTO) がある．WMTO は Weighted Totalizer[5] （あるいは Generalized Totalizer

Encording[1]）に modular arithmetic を導入している． WMTO では重みの正整数値の和を適切な基数で割り， 商と余りに分けて表現することにより，符号化後のサ イズを削減している．しかし，重みの組合せ数が多い 問題に対しては符号化後のサイズが膨大になるため，現 実的なメモリ制限内に収めることができず符号化に失 敗する． ∗_{連絡先： 九州大学大学院システム情報科学府}        〒 819-0395 福岡県福岡市西区元岡 744        E-mail:[email protected] 本研究では，混合基数を用いて WMTO の桁数を増 やすことで使用するメモリ量を削減する手法を提案す る．また既存の手法と比較実験を行い，提案する手法 の有用性について評価する．

2

既存の符号化手法

SAT ソルバーを推論エンジンとして用いる MaxSAT ソルバーは WPMS 問題を解く場合，PB 制約を付加し た問題に対して，SAT ソルバーを繰り返し適用するこ とで MaxSAT 解を求める．この時付加される PB 制約 式は∑n_i=1wi· bi< k で与えられるが，SAT ソルバー は CNF 式しか解くことができないため，PB 制約式を CNF 式に符号化する必要がある．この符号化には様々 な方式があり，同一の式を符号化をしても生成される 変数や節の数，クリティカルパスの長さなどが同一に なるとは限らない．一般的に，SAT 問題を構成する変 数や節の数は多いほど問題を解くのは困難になる．そ のため，PB 制約を CNF 式に符号化する際にも，変数 や節の数はより少ないほうが好ましい．以下に，既存 の符号化手法を記載する． • Binary Adder(WARN) Warners による符号化手法 [2]．重み wiを二進数 で符号化し，それぞれをトーナメント方式で二 進加算して総和を求める機構を SAT 符号化して いる． 人工知能学会研究会資料 SIG-FPAI-B506-03

MRWTO(⟨i1. . . in⟩, ⟨p1. . . pd−1⟩) = (⟨od1. . . o d md|pd−1. . .|p1o 1 1. . . o 1 m1⟩, ϕl∧ ϕr∧ ϕ) (n > 1)

MRWTO(⟨i1. . . i_⌊n/2⌋⟩, ⟨p1. . . pd₋₁⟩) = (⟨ad1. . . a

d αd|pd−1. . .|p1a 1 1. . . a 1 α1⟩, ϕl) MRWTO(⟨i_⌈n/2⌉. . . in⟩, ⟨p1. . . pd−1⟩) = (⟨b1d. . . bdβd|pd−1. . .|p1b 1 1. . . b1β1⟩, ϕr) MRWA(⟨ad₁. . . ad_α d|pd−1. . .|p1a 1 1. . . a 1 α1⟩, ⟨b d 1. . . b d βd|pd−1. . .|p1b 1 1. . . b 1 β1⟩) = (⟨od₁. . . od_md|p_d−1. . .|p1o 1 1. . . o 1 m1⟩, ϕ)

MRWTO(⟨i1⟩, (⟨p1. . . pd−1⟩) = ⟨od1|p_d−1. . .|p1o

1

1⟩) (n = 1)

図 1: Mixed Radix Weighted Totalizer の計算手続き（本体）

• Totalizer(TO) Bailleux らによる符号化方式 [3]．重みを一進数 で符号化，つまり wi個のビット列で符号化し， それぞれをトーナメント方式で一進加算して総和 を求める機構を SAT 符号化している． • Modulo Totalizer(MTO) 小川らによる符号化方式 [4]．wiを正整数 p を基 数とする modulo 数で符号化し，それぞれをトー ナメント方式で modulo 加算して総和を求める機 構を SAT 符号化している．Modulo の「商」と 「余り」の加算の符号化に，Bailleux の符号化が 用いられている． • Weighted Totalizer(WTO) 早田らによる符号化手法 [5]．wiに対応する変数 を別個に保持し，それぞれをトーナメント方式で 重みの部分和を計算して総和を求める機構を SAT 符号化している．

• Weighted Modulo Totalizer(WMTO)

有村らによる符号化手法 [6]．wiを正整数 p を基 数とする modulo 数で符号化し，それぞれをトー ナメント方式で modulo 加算して総和を求める機 構を SAT 符号化している．Modulo の「商」と 「余り」の加算の符号化に，早田らの符号化が用 いられている．

3

提案手法

3.1

Mixed Radix Weighted Totalizer

Mixed Radix Weighted Totalizer（MRWTO）とは， 前述の WMTO をさらに拡張した符号化方式である． WMTO では１つの基数 p を用い，重みを上位桁と下 位桁の二桁に分けることで生成する変数や節を削減し ていた．MRWTO では混合基数表記法 (Mixed Radix notation system)[7] を用い，重みを複数の桁に分ける ことで生成する変数や節を WMTO よりさらに削減し ている． 混合基数表記法とは，2 つ以上の基数を用いて数を表 現する手法である．ある数 W を混合基数で表すとき， 基数を_⟨p1. . . pd−1⟩ とすると W = qd· d_∏−1 i=1 pi+ . . . + q2· 1 ∏ i=1 pi+ q1 = (qd|p_d−1. . .|p2q2|p1q1) となる．基数が d− 1 個あるならば桁数は d となる． 身近に使用されている例として，時間の表記がある．例 えばある時点から時間の計測を始めたとして，T = 2 日 13 時間 46 分 32 秒経過したとする．これは表記を変 えると T = 2|2413|6046|6032 と表せる．MRWTO では 基数が 1 つの場合でも混合基数に含めるものとする． 図 1 は MRWTO の計算手続きである．MRWTO で は入力変数に対応する重さ wiを，基数_⟨p1. . . pd−1⟩ を 用いて混合基数表記にする．MRWTO は入力変数数列

⟨i1. . . in⟩ を ⟨i1. . . i_⌊n/2⌋⟩，⟨i_⌈n/2⌉. . . in⟩ に二分割し，そ れぞれを入力とする MRWTO を再帰的に呼び出す．そ の後，再帰的に呼び出された MRWTO の出力結果を混合 基数加算器（Mixed Radix Weighted Adder：MRWA）に

送り，その結果として (⟨od 1. . . odmd|pd−1. . .|p1o 1 1. . . o1m1⟩ と節集合 ϕ を出力する． 図 2 は MRWTO の加算器 MRWA の計算手続きであ る．MRWTO は入力変数数列を ⟨ad 1. . . adαd|pd−1. . .|p1a 1 1. . . a1α1⟩， ⟨bd 1. . . bdβd|pd−1. . .|p1b 1 1. . . b1β1⟩ とすると，出力として ⟨rd 1. . . rmdd|pd−1. . .|p1r 1 1. . . r1m1⟩ と節集合 ϕ を生成す る．ここで，変数 x に対応する重みを w(x) とし，ch(h = 1, . . . d) は各桁での桁上がりを意味する変数である．ま た，それぞれ ϕ1は第 1 桁（最下位桁），ϕh(h = 2, . . . , d− 1) は第 h 桁（中間桁），ϕdは第 d 桁（最上位桁）の節 集合を表し，それぞれの桁に対応する基数が phである ものとする．

MRWA(⟨ad₁. . . ad_α d|pd−1. . .|p1a 1 1. . . a 1 α1⟩, ⟨b d 1. . . b d βd|pd−1. . .|p1b 1 1. . . b 1 β1⟩) = (⟨r₁d. . . rd_md|p_d−1. . .|p1r 1 1. . . r 1 m1⟩, ϕ) ϕ = ϕ1∧ . . . ∧ ϕh∧ . . . ∧ ϕd ϕ1= α1 ∧ i=0 β1 ∧ j=0 { (a1 i ∨ b1j∨ r 1 k1∨ c1) (σ1< p1) (a1 i ∨ b1j∨ rk11), (a 1 i ∨ b1j∨ c1) (σ1≥ p1) .. . ϕh=                  αh ∧ i=0 βh ∧ j=0 { (ah i ∨ bhj ∨ r h k1∨ ch) (σh< ph) (ah i ∨ bhj ∨ r h k1), (a h i ∨ bhj ∨ ch) (σh≥ ph) αh ∧ i=0 βh ∧ j=0 { (ch₋₁∨ ah i ∨ bhj ∨ rhk2∨ ch) (σh+ 1 < ph) (ch−1∨ ahi ∨ b h j ∨ r h k2), (ch−1∨ a h i ∨ b h j ∨ ch) (σh+ 1≥ ph) (h = 2, . . . , d− 1) .. . ϕd= αd ∧ i=0 βd ∧ j=0 (ad i ∨ bdj∨ r d k1), (cd−1∨ a d i ∨ bdj∨ r d k2) σh= w(ahi) + w(b h j) (h = 1, . . . , d− 1) w(rhk1) = σhmod ph (h = 1, . . . , d− 1) w(rh_k 2) = (σh+ 1) mod ph (h = 1, . . . , d− 1) w(rd_k1) = w(ad_i) + w(bd_j) w(rdk2) = w(a d i) + w(bdj) + 1 ah₀ = bh₀ = 1 (h = 1, . . . , d) w(ah₀) = w(bh₀) = 0 (h = 1, . . . , d)

図 2: Mixed Radix Weighted Totalizer の計算手続き（加算器）

ϕ1は a1i と b1j において σ1 = w(a1i) + w(b1j) の値に よって生成する節が異なる．σ1が p1より小さな値であ るとき，ϕ1では (a1i∨b1j∨r1k1∨c1) を生成する．これは 式変形すると ((a1 i∧b1j∧c1)→ rk11) となり，a 1 iと b1jがと もに 1 であり，かつ桁上がりが発生しないならば r1 k1が 1 となることを意味する．このとき，r1 k1は w(r 1 k1) = σ1 を満たすものとする．σ1が p1以上である場合は二つ の節を生成する．一つ目は (a1 i∨ b1j∨ r 1 k1) であり，これ は a1 i と b1j がともに 1 であるならば rkh1が 1 となるこ とを表している．このとき r1 k1 は w(r 1 k1) = σ1mod p1 を満たすものとする．二つ目は (a1 i ∨ b1j∨ c1) であり， a1 i と b1j がともに 1 であるならば，第 1 桁で桁上がり があることを意味する変数 c1が 1 となることを表す． 中間桁の ϕhでは，一つ前の桁からの桁上がりの有無 によりそれぞれ節を生成する．桁上がりがない場合は， ϕhでは ϕ1とほぼ同じような節を生成する．この場合， ϕhは ahi と bhjにおいて σh= w(ahi) + w(bhj) の値によっ て生成する節が異なる．σhが phより小さな値であると き，ϕhでは (ah i∨bhj∨rhk1∨ch) を生成する．これは式変 形すると ((ah i∧bhj∧ch)→ rkh1) となり，a h i と bhjがとも に 1 であり，かつ桁上がりが発生しないならば rh k1が 1 となることを意味する．このとき，rh k1は w(r h k1) = σh を満たすものとする．σhが ph以上である場合は二つ の節を生成する．一つ目は (ah i∨ bhj∨ rhk1) であり，これ は ah i と bhj がともに 1 であるならば rkh1が 1 となるこ とを表している．このとき rh k1は w(r h k1) = σhmod ph を満たすものとする．二つ目は (ah i ∨ bhj ∨ ch) であり， ah i と bhj がともに 1 であるならば，第 h 桁で桁上がり

があることを意味する変数 chが 1 となることを表す． ϕhで一つ前からの桁上がりがある場合でも σhの値に よって生成する節が異なる．σh+ 1 が phより小さな値 であるとき，ϕhでは (ch−1∨ahi∨bhj∨rhk2∨ch) を生成す る．これは式変形すると ((ch₋₁∧ah i∧bhj∧ch)→ rhk2) と なり，一つ前からの桁上がりがあり，かつ ah i と bhjがとも に 1 であり，かつ桁上がりが発生しないならば rh k2が 1 と なることを意味する．このとき，rh k2は w(r h k2) = σh+ 1 を満たすものとする．σh+ 1 が ph以上である場合は二 つの節を生成する．一つ目は (ch₋₁∨ ah i ∨ bhj ∨ rhk2) で あり，これは一つ前からの桁上がりがあり，かつ ah i と bh j がともに 1 であるならば rkh2が 1 となることを表し ている．このとき rh k2は w(r h k2) = (σh+ 1) mod phを 満たすものとする．二つ目は (ch₋₁∨ ah i ∨ bhj ∨ ch) で あり，一つ前からの桁上がりがあり，かつ ah i と bhj が 1 であるならば，第 h 桁で桁上がりがあることを意味 する変数 chが 1 となることを表す． ϕdでも一つ前からの桁上がりの有無のそれぞれで節 を生成する．一つ前からの桁上がりがない場合，ϕdで は (ad i ∨ bdj∨ rdk1) を生成する．これは，a d i と bdjがとも に 1 であるならば rd k1 が 1 となることを表す．このと き，rd k1は w(r d k1) = w(a d i) + w(bdj) を満たすものとす る．また，一つ前からの桁上がりがある場合には，ϕd は (cd₋₁∨ ad i ∨ bdj∨ r d k2) を生成する．これは，cd−1と ad i と bdjが 1 であるならば rdk2が 1 となることを表す． このとき，rd k2は w(r d k2) = w(a d i) + w(bdj) + 1 を満たす ものとする．

4

実験

4.1

実験環境

各符号化手法を用いて WPMS 問題を解き，性能評価 を行う．使用する MaxSAT ソルバーは QMaxSAT[8] であり，推論エンジンとして glucoce3.0[9] を使用する． 実験環境は以下のとおりである．

• CPU：Intel Corei5 [email protected] × 4 • メモリ：3.2GB

• OS：ubuntu14.10

• 使用したソルバー：QMaxSAT（glucose3.0） • 実験問題

– MaxSAT Evaluation 2016[10] の Weighted

PartialMaxSAT 部門の crafted 分野と in-dustrial 分野 • 制限時間：1800 秒

4.2

実験結果

表 1 は QMaxSAT が問題を解く過程でメモリアウト することがなかった問題数を表にまとめたものである． 1 行目は使用した符号化手法，2 行目は Crafted 分野で の結果，3 行目は Industrial 分野での結果を表す．#Ins. の列はそれぞれの分野に含まれる問題数を表し，符号 化手法の列にある数値はメモリアウトしなかった問題 数を表す． MRWTO は Crafted 分野ではメモリアウトした問題 はなく，Industrial 分野ではメモリアウトした問題は 8 問だけだった．WMTO の結果と比較すると，生成する 変数や節の数を大幅に削減することに成功したことは 明らかである．また，MRWTO がメモリアウトした問 題で WARN がメモリアウトしなかった問題は 5 問あ る．この 5 問の中で WARN が制限時間以内に解けた問 題は 1 問もなかった．そのため，MRWTO と WARN の間でメモリアウトによって解答した問題数に差は生 じることはない． 表 2 は各符号化手法で問題を解いた際の解答数と平 均解答時間である．各表の最初の列は，各問題に含まれ ている問題セットを表している．2 列目の#Ins. は，各 問題セットに含まれている問題数を表している．3 列目 以降は，QMaxSAT が使用した符号化方式での結果を表 している．それぞれ WARN は warners による符号化方 式，TO は Totalizer，MTO は Modulo Totalizer，WTO は Weighted Totalizer，WMTO は Weighted Modulo Totalizer，MRWTO は Mixed Radix Weighted Total-izer である．表の中の数値のうち，括弧の中にある値 は各符号化手法が各問題セットで解けた問題数を表し ており，括弧の外にある数値は解けた問題での平均時 間を表す． 表 2 より，MRWTO は Crafted 分野で 192 問解いて おり，WARN と並んで最も多く解けていることがわか る．また，WMTO と比べて 68 問多く解けていること がわかる．Industrial 分野では MRWTO は 345 問解い ており，最も多く解けていることがわかる．WMTO と 比較すると，MRWTO のほうが 157 問多く解いている． 図 3，図 4 はそれぞれ Crafted 分野，Industrial 分 野での結果をグラフにしたものである．横軸が問題数 を表し，縦軸が実行時間を表す．実行時間は昇順に並 び直したものを使用している．このグラフでは，右に あるものほど優れた符号化手法であることを示してい る．例として，400 秒以内に解けた問題数を比較する と，MRWTO では約 170 問あるのに対し，MTO は約 105 問ほどである．

図 3 を見ると，Crafted 分野では MRWTO と WARN は同じ解答数であるためグラフの最後の方で交わってい る．しかしながら，グラフの途中では MRWTO は常に WARN より右側に来ているため，MRWTO は WARN

表 1: MaxSAT Evaluation 2016 WPMS 問題でのメモリアウトしなかった問題数

Encording #Ins. WARN TO MTO WTO WMTO MRWTO

Crafted 331 331 127 235 152 226 331

Industrial 630 627 79 125 113 239 622

表 2: MaxSAT Evaluation 2016 WPMS 問題の解答数・平均解答時間

Encording #Ins. WARN TO MTO WTO WMTO MRWTO

Crafted 331 211.24(192) 76.46(48) 93.10(114) 97.66(70) 104.59(124) 154.67(192) Industrial 630 381.84(286) 79.17(50) 109.19(84) 85.65(84) 129.74(188) 216.30(345) 図 3: Crafted での解答時間と解答数の比較 図 4: Industrial での解答時間と解答数の比較 よりより結果であったと考えることができる．また， WARN 以外の手法と比較すると MRWTO は明らかに 良いことがわかる． 一方，図 4 を見ると Industrial 分野では MRWTO は他の手法より多く右側に来ている．このことから， MRWTO は他の手法より優れていることは明らかで ある．

5

おわりに

本研究では Weighted Modulo Totalizer に対して，重 み表現の桁数をさらに多くすることで変数や節を削減す ることを目的とした Mixed Radix Weighted Totalizer を提案した．結果を見ると，MRWTO は WMTO と比 べて変数や節の数を大幅に削減することに成功した． また，問題の解答数も MRWTO が一番多く，いままで QMaxSAT で一番成績の良かった WARN より結果が 良くなった． 本研究では，基数の決め方を一通りしか行っていな い．そのため，別の方法で基数を決定しより良いもの を探していく必要がある．特に，本研究では基数をす べて同じ値に設定していた．複数の種類の基数を組み 合わせることでより効率的になると考えられる．具体 的には，ある数の集合に対して，混合基数を用いて表 記するときの最適な基数の組み合わせを考える．この 基数組み合わせを採用することにより，MRWTO が生 成する変数や節を削減できる可能性がある．

謝辞

本研究は科研究費 16K00304 の助成を受けたもので ある．

参考文献

[1] Joshi, Saurabh, Ruben Martins, and Vasco Manquinho. “Generalized Totalizer Encoding for Pseudo-Boolean Constraints.” International Conference on Principles and Practice of Con-straint Programming. Springer International Publishing, 2015.

[2] Joost P. Warners. A linear-time transformation of linear inequalities into conjunctive normal

form. Information Processing Letters, 68:63-69, 1998.

[3] Olivier Bailleux and Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality straints. In Proceedings of 9th International

Con-ference on Principles and Practice of Constraint Programming (CP 2003), pages 108-122, 2003.

[4] Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Mod-ulo Based CNF Encoding of Cardinality Con-straints and Its Application to MaxSAT Solvers. In Proceedings of IEEE 25th International

Con-ference on Tools with Artificial Intelligence (IC-TAI 2013), pages 9-17, 2013. [5] 早 田 翔, 長 谷 川 隆 三. (2015). 重 み 付 き 部 分 MaxSAT 問題における基数制約符号化手法の改 良. SIG-FPAI= SIG-FPAI, 4(04), 85-90. [6] 有村寿高, 長谷川隆三, 藤田博, 上村直輝. (2016). Modulo 計算に基づく重み付部分 MaxSAT 問題 の基数制約符号化手法の改良. FPAI= SIG-FPAI, 5(03), 66-69.

[7] Codish, M., Fekete, Y., Fuhs, C., & Schneider-Kamp, P. (2011, March). Optimal base encodings for pseudo-Boolean constraints. In International Conference on Tools and Algorithms for the Con-struction and Analysis of Systems (pp. 189-204). Springer Berlin Heidelberg.

[8] Miyuki Koshimura, Tong Zhang, Hiroshi Fu-jita, and Ryuzo Hasegawa. QMaxSAT: A Partial Max-SAT Solver: JSAT, Vol.8(2012), system de-scription, pages 95-100.

[9] http://www.labri.fr/perso/lsimon/glucose/ [10] http://maxsat.ia.udl.cat/requirements/