日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

順序符号化と対数符号化を融合した制約充足問題のハ
イブリッド符号化
宋 剛秀

番原 睦則

田村 直之

本論文では制約充足問題 (CSP) から命題論理式の充足可能性判定問題 (SAT) への新しい符号化として，順序符号化と対数符号化を融合したハイブリッド符号化を提案する．順序符号化は効率的な制約伝播が特長であり小中規模のドメイン/アリティを持つ制約に対して有効な符号化であるが，それらが大きくなるにつれて符号化によって生成される SAT 節が膨大になる．一方，対数符号化は大規模なドメイン/アリティを持つ制約でも比較的少ない SAT 節で符号化できるが，桁上りのための推論が余分に必要なため制約伝播の効率はよくない．提案手法は両符号化の特長を活かし，小中規模のドメイン/アリティをもつ制約は順序符号化し，その他の制約については対数符号化する．人工的な問題 12 問と CSP ソルバー競技会のベンチマーク問題 1002 問を用いた実験の結果，提案手法は両符号化よりも高速に多くの問題を求解できることを確認した．さらにどちらの符号化でも解けない問題を解くことにも成功し，融合の相乗効果を確認した．

This paper proposes a new hybrid encoding of finite linear CSP to SAT integrating order and log encodings.
The order encoding maintains bound consistency by unit propagation and works well for instances withsmall/middle domain sized variables and/or arity of constraints. The log encoding generates smaller CNF
and is suitable for instances with larger domain sized variables, but its performance is not good in generalbecause more inference steps are required to ripple carries. The proposed hybrid encoding takes advantagesof both encodings by applying order encoding for constraints of small/middle sized domain/arity and log
encoding for other constraints. We carried out experiments on 12 handmade instances and 1002 instancesfrom CSP solver competition. In the result, our proposed hybrid encoding solved more number of instances
within shorter time than each of order and log encodings. Moreover, we succeeded in solving instances
which cannot be solved by both two encodings and confirm the synergy eﬀect of the hybridization.

[7] [16] [21]．それを背景として，CSP を SAT/PB に

1 はじめに変換 (符号化) し，高速な SAT/PB ソルバーを用いて制約充足問題 (CSP; Constraint Satisfaction Prob-

解く方法が成功を収めている [27] [29] [24]．

lem) は，与えられた制約を満たす解を探索する問題

CSP の命題論理への符号化としては，順序符号化であり，人工知能などの分野における多くの組合せ問[8] [28]，対数符号化 [17] [12] など，様々な方法が提案さ

題は，CSP として定式化できることが知られている

れている．しかし，いずれの符号化も長所と短所が存[22]．

在する．特に順序符号化は，2008 年および 2009 年の一方，与えられた命題論理の充足可能性判定問題(SAT) や，その拡張である擬似ブール制約充足問題

国際 CSP ソルバー競技会 [18] の複数部門で優勝した
SAT 型制約ソルバー Sugar †1 に採用されており，多(PB) について，それらを解くプログラムである SAT

くの問題に対して優れた性能を示している [23] [4] [15]．

ソルバーや PB ソルバーの性能が大きく向上している

しかし，順序符号化は変数のドメインサイズが大き

A Hybrid Encoding of CSP to SAT Integrating Orderand Log Encodings
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.

い場合，生成される SAT 問題のサイズが巨大になり，解くことができないという問題点がある．一方，対数†1 http://bach.istc.kobe-u.ac.jp/sugar/符号化は，順序符号化に性能的には劣るが，大きな問

イブリッド符号化は順序符号化，対数符号化と比較し題にも対応できるという利点を持つ．

て良い性能を示すことを確認した．

したがって，複数の符号化を融合させた ハイブリッ

以下，2 節で CSP および 0-1 CSP, PB, SAT を定ド符号化 の研究が重要になる．特に，直接符号化

義する．3 節では，既存の符号化を統一的に説明する[9] [31] と順序符号化のハイブリッドについては論文枠組みとして標準的ブール符号化を提案し，その枠組[13], BEE [19], meSAT [25] で研究されている．これ

みを用いて対数符号化と順序符号化を定義する．4 節

らはいずれも各変数を直接符号化と順序符号化の両で，標準的ブール符号化の枠組みを用い，順序符号化

方で符号化し，さらにそれらの符号化を関連付けるたと対数符号化を融合させたハイブリッド符号化を提めチャネリング制約と呼ばれるものを追加している．

案する．チャネリング制約が不要なハイブリッドを実

この方法 (ここではチャネリング方式と呼ぶ) は，直現できている点が特長である．5 節では，提案したハ接符号化と順序符号化のハイブリッドについては成功

イブリッド符号化を実装した Diet-Sugar を説明する．

したが，対数符号化とのハイブリッドには利用できな

6 節では，国際 CSP ソルバー競技会のベンチマーク

い．なぜなら，対数符号化した変数を，直接符号化あ問題を用いて，ハイブリッド符号化を既存の順序符号

るいは順序符号化と関連付けた場合，チャネリング制化および対数符号化と比較・評価する．最後に，7 節約が膨大になり，対数符号化の利点が失われてしまうで結論を述べる．

からである．
そこで本論文では，チャネリング制約が不要な，順2 制約充足問題

序符号化と対数符号化を融合した CSP のハイブリッ

本節では制約充足問題 (CSP; Constraint Satisfac-

ド符号化を提案する．提案方法では CSP の各整数変tion Problem) を定義し，さらにその一種として 0-1

数は順序符号化もしくは対数符号化のどちらか一つ

制約充足問題 (0-1 CSP)，擬似ブール制約充足問題

で符号化され，各制約は両方の符号化変数を含むこと(PB)，命題論理の充足可能性判定問題 (SAT) を定義ができる．どの変数にどの符号化を用いるかは任意にする．

決めることができるため，どの問題・制約にどの符号一般の制約充足問題では，整数，実数，集合等のド化を適用するかを自由に切り替え可能なことも特長

メイン上の様々な制約を対象としているが，本稿ではである．本論文では各変数の符号化方法を自動的に選整数有限領域上の線形の制約を対象とする．なお，実択する方法についても考察を行い，ドメイン積を用い用的な制約充足問題の多くは，整数有限領域上の線形た方法の提案を行う．

制約で表現できることが知られている．

提案方法は SAT 型 CSP ソルバー Diet-Sugar として実装を行った †2 . Diet-Sugar は Sugar を基に実装

X を 変数 の集合とする (以下 x, y, x1 , y1 等で変を含む CSP に対応している [18]．計算機実験では，数を表す)．x1 , x2 , . . . , xn が変数，a1 , a2 , . . . , an お∑
よび c が整数定数の時， ni=1 ai xi の形の式を 線形∑
和 (linear summation) と呼び， ni=1 ai xi # c の形

Diet-Sugar を用いて順序符号化，対数符号化，提案の式を 線形比較 (linear comparison) と呼ぶ (以下 S,

され，XCSP [18] 形式で記述されたグローバル制約

するハイブリッド符号化の比較を行った．比較には 2

S1 等で線形和を表し， E, E1 等で線形比較を表す)．

種類のベンチマークを用いた．一つ目は人工的な問題

ただし ai ̸= 0 かつ xi はすべて異なると仮定する．

で順序符号化と対数符号化のハイブリッド符号化にお線形比較 S ≥ c の否定 ¬(S ≥ c) を −S ≥ −c + 1 でける相乗効果を確認するために用いた．二つ目はより定義する．なお，線形比較の比較演算子が =, ̸=, ≤広範な問題で評価を行うために CSP ソルバー競技会等の場合も簡単に ≥ の線形比較に書き換えることがの 1002 問の問題を用いた．結果として，提案するハできるため，比較演算子を ≥ に限定しても一般性を失わない．線形和もしくは線形比較中に含まれる変数†2 http://kix.istc.kobe-u.ac.jp/~soh/dsugar/の数を アリティ (ality) と呼ぶ．線形比較の有限集合

を 制約 (constraint) と呼び，制約の有限集合を 制約

擬似ブールの CSP を 擬似ブール制約充足問題 (PB)

集合 (constraint set) と呼ぶ．以下 C, C1 等で制約と呼ぶ．

{p1 + 2p2 ≥ 1} は擬似ブール制約の例である．擬を表し，C 等の斜体太字で制約集合を表す．
定義 1 制約充足問題 (CSP; Constraint Satisfac-

似ブール制約は単純 0-1 制約，PB は単純 0-1 CSP でtion Problem) は，以下を満たす組 (X, Dom, C) で

ある．

ある．

定義 5 すべての線形比較がリテラルの制約を 節• X は 変数 の有限集合 (X ⊂ X )．

(clause) と呼び，すべての制約が節の CSP を 命題論• Dom は各変数の取りうる値の集合である ドメ

理の充足可能性判定問題 (SAT) と呼ぶ．

{p, ¬q} は節の例である．節は単純 0-1 制約，SAT

イン を定める関数．ここでは，ドメインは整数の有界の範囲とする．

は単純 0-1 CSP である．

• C は X 上の線形比較から成る制約集合．

3 標準的ブール符号化としての対数符号化と制約集合 C = {C1 , . . . , Cn } は制約 Ci の連言を意

順序符号化

味し，C1 ∧ · · · ∧ Cn あるいは Ci の列で表すことがある．また，制約 C = {E1 , . . . , Em } は線形比較 Ej の

本節の前半では， 標準的ブール符号化 の定義を行

選言を意味し，E1 ∨ · · · ∨ Em で表すことがある．すう．この枠組では SAT 符号化は与えられた変数集合

なわち制約集合は，線形比較の CNF 式 (Conjunctive

に対して部分的に適用され，これを利用することでNormal Form 式) である．

チャネリング制約を用いることなく SAT 符号化のハ線形比較 E 中に現れる変数の集合を Var (E) で表

イブリッドを行うことが可能になる．本節の後半です．制約 C についても同様に Var (C) で表示する．

は，対数符号化と順序符号化を標準的ブール符号化を

変数 x のドメイン Dom(x) の下限と上限を，それぞ用いて定式化する．

れ lb(x) と ub(x) で表す．同様に線形和 S の下限と上限を，それぞれ lb(S) と ub(S) で表す．

3. 1 標準的ブール符号化

CSP (X, Dom, C) において，Dom(x) ⊂ {0, 1} のCSP から CSP への 変換 (あるいは 符号化) τ にお場合，x を ブール変数 と呼ぶ (以下 p, q, p1 , q1 等

いて，元の CSP P と変換後の CSP P ′ の充足可能性

でブール変数を表す)．

が一致する時，変換 τ は 充足同値 (equi-satisfiable)

1 つのブール変数から成る線形比較を リテラル
(literal) と呼ぶ (以下 L, L1 等でリテラルを表す)，リであるという．変換 τ1 , τ2 が充足同値な時，合成τ ◦ τ †3 もまた充足同値な変換である．
1

2

テラルでない線形比較を 複雑な線形比較 と呼ぶ．

与えられた変数集合に関して部分的に符号化を行

定義 2 複雑な線形比較 (リテラルでない線形比較) をうように対数符号化と順序符号化を定義するために，

高々1 つ含む制約を単純な制約 (simple constraint)

以下の 標準的ブール符号化 を導入する．

と呼び，すべての制約が単純な CSP を 単純 CSP と

定義 6 与えられた変数の部分集合 V に関する 標準呼ぶ．

的ブール符号化 は以下を満たす組 (U, A, T ) である．

{p, ¬q}, {p1 , p2 , x − y ≥ 0} は単純な制約の例である．
定義 3 すべての変数がブール変数の制約を 0-1 制

ただし，CSP P = (X, Dom, C) ， V ⊆ X とする．

• U は符号化によって追加される変数の集合を表す． X ∩ U = ∅ とする．

約 と呼び，すべての制約が 0-1 制約の CSP を 0-1• A は追加する制約集合を表す．

CSP と呼ぶ．

• T は与えられた線形比較を制約集合に変換する{p1 − p2 ≥ 0, p2 − p3 ≥ 0} は 0-1 制約の例である．

関数である．

定義 4 1 つの線形比較からなる 0-1 制約を 擬似ブール制約 (あるいは PB 制約) と呼び，すべての制約が†3 ((f ◦ g)(x) = g(f (x))

この標準的なブール符号化によって得られる CSP

考える．τVL によって以下が得られる．

P ′ = (X ′ , Dom ′ , C ′ ) は以下になる．
′(X \V)∪U Dom(x) (x ∈ X \ V )Dom ′ (x) = {0, 1}(x ∈ U )∧∨′C = A ∪ C∈C E∈C T (E)∨
ここで注意したいのは， E∈C T (E) の組合せが場
X={px,0 , px,1 }ALV={{1 + px,0 + 2px,1 ≤ 3}}

TVL ({E})={{1 + px,0 + 2px,1 − y ≥ 1}}

UVL=

合によっては膨大になることである．例えば複雑な線形比較のみで構成される制約 C = {E1 , ..., En } が与えられた時に，C を標準的ブール符号化することを∏考える．制約 C は素朴に考えると ni=1 |T (Ei )| 個の制約になる．しかし，Tseitin 変換 [30] を用いると制約の増加を抑えながら CSP から単純 CSP への変換が可能になる．
例 1 複雑な線形比較で構成される制約 C = {E1 , E2 }が与えられたとする．Tseitin 変換により，充足同値
な単純制約の集合 {{p, q}, {¬p, E1 }, {¬q, E2 }} が得

3. 3 順序符号化
順序符号化 (order encoding) は，CSP から 0-1

CSP への充足同値な変換である．元の CSP の変数 xおよび値 d ∈ Dom(x) \ {lb(x)} に対し x ≥ d を意味
する新しいブール変数 px≥d を導入する [8] [28] (引用
論文では x ≥ d ではなく x ≤ d にブール変数を対応させている)．
例えば Dom(x) = Dom(y) = {1 .. 5} なる変数 x,y および制約 x − y ≥ 0 の符号化を考える．
• 変数 x について以下の 4 つのブール変数を導入する (px≥1 は x ≥ 1 が常に真のため不要)．変数

y についても同様とする．

られる. 元の制約と比較すると符号化後の制約数は|T (E1 )| × |T (E2 )| から |T (E1 )| + |T (E2 )| + 1 へと削減できることが分かる．

px≥2

px≥3

px≥4

px≥5

• 導入したブール変数に対し，以下の制約を導入する．変数 y についても同様とする．

{px≥2 , ¬px≥3 }, {px≥3 , ¬px≥4 }, {px≥4 , ¬px≥5 }3. 2 対数符号化

x = 1 は px≥d のすべてが偽の時に対応し，x = 5

対数符号化 (もしくは 2 進符号化) は CSP から 0-1

CSP への充足同値な変換である．元の CSP の変数 xに対し，x − lb(x) の 2 進表現の i ビット目を表す新はすべてが真の時に対応する．

• この時 x − y ≥ 0 は，以下のように符号化できる．

しいブール変数 px,i を導入し，x をそれらの重み付
き和で表す [17] [12]．

変数 x に対する順序符号化 τxo を標準的変換と変数集合 V に対する対数符号化
下のL(UVL , AL
V , TV ){{px≥d , ¬py≥d } | 1 < d ≤ 5}

τVL

を以

で 表 す．た だ し ，CSP P =(X, Dom, C), V ⊆ X とする．
UVL={px,i | x ∈ V, 0 ≤ i ≤ mx }

AL
V

=

{{xσ ≤ ub(x)} | x ∈ V }TVL (E)={{Eσ}}

σ={x 7→ lb(x) +∑mxii=0 2 px,i | x ∈ V }ここで記号 7→ は変数集合から線形和への写像を表す．

Eσ は線形比較 E において変数 x を線形和 σ(x) でして以下の (U, V, D, A, ∥·∥) で定める (τxo の o はorder を 表 す)．変 数 集 合 V に 対 す る 順 序 符 号 化OτVO を以下の (UVO , AO
V , TV ) で表す．ただし，CSP

P = (X, Dom, C), V ⊆ X とする．
UVO=

{px≥d | x ∈ V, lb(x) < d ≤ ub(x)}

AO
V

=

{{px≥d , ¬px≥d+1 }TVO (E)=

置換した結果を表す．
例 2 変数集合 X = {x, y}, ドメイン Dom(x) ={1, 2, 3}, 制約 C = {{E}} = {{x − y ≥ 1}} から構成される CSP (X, Dom, C) と変数集合 V = {x} を

ここで E =
定義される.

 | x ∈ V, lb(x) < d < ub(x)} {{E}} (Var (S) ∩ V = ∅)
 T ′ (E)∑n(Var (S) ∩ V ̸= ∅)′i=1 ai xi と T (E) は以下のように

4 順序符号化と対数符号化を融合したハイブT′ (E) =
リッド符号化{{px1 ≥⌈c/a1 ⌉ }}(n = 1, x1 ∈ V, a1 > 0)






(n = 1, x1 ∈ V, a1 < 0)x ≥⌊c/a1 ⌋+1 }}
本節では前節までで定義した変数の部分集合に対 {{¬p
∑
∧1


O


({{p
}}
∨
T
(
a
x
≥
c
−
a
d))
j j
i
xi ≥d+1
V
する対数符号化と順序符号化を用いてそれらを融合


j̸=i

d∈Dom(xi )したハイブリッド符号化を説明する．
(n > 1, xi ∈ V, ai > 0)



∧
∑



({{¬pxi ≥d }} ∨ TVO ( aj xj ≥ c − ai d))
4. 1 ハイブリッド符号化j̸=i d∈Dom(xi )(n > 1, xi ∈ V, ai < 0)
CSP P = (X, Dom, C) と X の分割 {VO , VL } が
上述の定義において，d ≤ lb(x) の時 px≥d = 1,

d > ub(x) の時 px≥d = 0 とする．
例 3 変数集合 X = {x, y}, ドメイン Dom(x) =与えられた時，順序符号化と対数符号化を融合したハH
イブリッド符号化ハイブリッド符号化 τX= τVLL ◦ τVOO

は以下のように定義される．
H
UX=

UVLL ∪ UVOO

AH
X

=

O
AL
VL ∪ AVO

H
TX
(E)

=

TVOO (TVLL (E)){0, 1, 2}, 制約 C = {{E}} = {{x + y ≥ 0}} から構成される CSP (X, Dom, C) と変数集合 V = {x} を考える．τVO によって以下が得られる．

UVO={px≥1 , px≥2 }

AO
V

=

{{px≥1 , ¬px≥2 }}TVO ({E})={{px≥1 , y ≥ 0}, {px≥2 , y ≥ −1},{y ≥ −2}}

3. 4 0-1CSP から SAT への符号化
ここまで説明してきた対数符号化，順序符号化を用いることで, CSP をブール変数しか含まない 0-1CSP
へと符号化できる．さらに 3. 1 節で説明した Tseitin
変換を適用することで単純 0-1CSP が得られる．単純 0-1CSP は Big-M 法 [14] により PB へと変換する
ことができる．例えば，ブール変数 p と線形和 S から構成される制約 {p, S ≥ c} を考える．この制約はBig-M 法により (c − lb(S))p + S ≥ c へと変換される．ここで lb(S) は線形和の下限値を表す．この制約
は p = 1 の時に明らかに充足可能であり，p = 0 の時は S ≥ c と同値になる．
以上により，CSP は単純 CSP，単純 0-1 CSP を経て PB に変換できる．PB に変換されれば，これまで数多く提案されている PB を SAT への符号化方法を利用することができる [10] [3] [1] [26] ．他の方法としては直接 PB ソルバーを使う方法であり [5] [11] [10] ，この場合は PB から SAT への符号化は必要ない．

ここで対数符号化と順序符号化の合成は可換であることに注意されたい．すなわち τVLL ◦ τVOO = τVOO ◦ τVLL
が成り立つ．
例 4 変数集合 X = {x, y}, ドメイン Dom(·) ={0, 1, 2}, 制約 C = {{E}} = {{x + y ≥ 0}} から構成される CSP (X, Dom, C) を考える. また対数符号
化，順序符号化する変数集合をそれぞれ VL = {x},HVO = {y} とする．ハイブリッド符号化 τXによって以下が得られる．
H
UX={px,0 , px,1 } ∪ {py≥1 , py≥2 }

AH
X

=

{{2px,1 + px,0 ≤ 2}} ∪ {{py≥1 , ¬py≥2 }}

H
TX
(E)

=

TVOO (TVLL (E))=

TVOO ({2px,1 + px,0 + y ≥ 0})={{2px,1 + px,0 ≥ 0, py≥1 },{2px,1 + px,0 ≥ −1, py≥2 },{2px,1 + px,0 ≥ −2}}

4. 2 変数の分類
提案するハイブリッド符号化では，順序符号化すべき変数，対数符号化すべき変数をどのように分類してX の分割 VL と VO を作るのかが重要になる．分類の方法は大きく二つある：一つ目は変数に着目する方法でドメインサイズが分類の指標になる．二つ目は変数のドメインサイズと制約のアリティの両方を用いる方法である．一つ目の変数だけに着目する方法は直感

的だが順序符号化によって生成される節数が膨大にな

5 Diet-Sugar の実装

る場合がある．
例 え ば 3 つ の 整 数 変 数 x, y ∈ {1, . . . , 1000},

提案するハイブリッド符号化を用いた SAT 型 CSPz ∈ {1, . . . , 10000} と二つの制約 x ≤ z と x + y ≤ z

ソルバー Diet-Sugar を Sugar を基にして実装した．

が与えられたとする．ドメインサイズのみを指標とし，外延的制約を除いて，Diet-Sugar は alldiﬀerent など

閾値を 1000 に設定した場合，x と y は順序符号化のグローバル制約を含む全ての XCSP 形式 [18] に対に分類され z は対数符号化に分類される．この場合，応可能である．また Sugar の専用 CSP 言語にも対応

一つ目の制約 x ≤ z の符号化節数は 12993 となるが，している．Diet-Sugar は以下の手順で CSP の解を計

二つ目の制約 x + y ≤ z の符号化節数は 1011993 で算する:あり，これは明らかに SAT ソルバーが扱える節数の1. CSP を定義 1 の形式に変換し, 3. 1 節に記載し限界に近い．この例からも明らかなように，順序符号

た Tseitin 変換によって単純 CSP を得る．

化によって得られる節数は制約のアリティが増えるに

2. 4 節に記載したハイブリッド符号化によって単伴って急激に増加する．このような増加を避けるためにドメインサイズだけでなく制約のアリティも考慮し

純 CSP を単純 0-1CSP に変換する．

3. 単純 0-1CSP を 3. 4 節に記載した方法で SATに変換する．

た指標が必要になる．
そこで本論文ではドメインサイズの積， ドメイン

今回 Diet-Sugar のバックエンドソルバーには最新

積 を変数の分類の指標に使うことを提案する．線形比∑較E= ni=1 ai xi ≥ c に対してドメイン積 DP (E)バージョンの minisat+ (ver. 1.1) とそのデフォルトは次のように定義される．
n−1∏
DP(E) =
|Dom(xi )|i=1

ここで変数はドメインサイズの昇順にソートされているものとする．順序符号化による符号化節数の上限は d をドメインサイズ，n をアリティとした時にO(dn−1 ) に与えられることから，ドメイン積は順序符
号化によって生成される節数の概算にもなっている．
この指標に加えて，PB 制約は 0-1 変数しか含まない
ことから対数符号化を用いるのが妥当なので，PB 制約に含まれる変数は対数符号化するのが適当である．
提 案 す る 分 類 方 法 を 以 下 に 定 義 す る ．CSP

(X, Dom, C) と閾値 θ が与えられた時，ハイブリッ
ド符号化において対数符号化する変数の部分集合は
以下のように定義される．
VL = {v ∈ Var (E) |DP(E) > θ or E は 0-1 線形比較, E ∈ c, c ∈ C}.
ハイブリッド符号化は以下のように動作する．

の SAT ソルバーである minisat (ver. 2.2) を用いた．
両ソフトウェアは github†4 から入手可能である．この他に Diet-Sugar では minisat+ を PB から SAT への符号化器として用いることで任意の SAT ソルバー
を利用可能である [2] [6] [11] [20] [5].

6 計算機実験
本節では提案するハイブリッド符号化の求解性能を
順序符号化と対数符号化と比較する．実験条件を揃えるために三つの符号化は 5 節の手順 2 で切り替えた．計算機は CPU として Xeon E5 3.7GHz，メモリを 32GB 搭載したものを使用した．
比較には二つのベンチマークセットを用いた．一つ目のベンチマークは人工的な問題であり，ハイブリッ
ドの相乗効果を確認するために用いた．二つ目のベンチマークは 2009 年の CSP ソルバー競技会の 1002
問であり，多種の問題を用いた広範な比較を行うために用いた．

• VL = ∅ の時は順序符号化と同じ

本実験の前にドメイン積の閾値 θ を決定するための• VL = X の時は対数符号化と同じ予備実験を行った． θ として 1024, 2048, 4096, 8192

• ∅ ⊊ VL ⊊ X の時，順序符号化と対数符号化のを実験した結果，最も性能が良かった 4096 を以降のハイブリッド†4 https://github.com/niklasso

実験では使用する．

メインが大きいため対数符号化が効果的であると考えられる.

• 二つ目のパラメータ集合は n = 8 で固定とし，

6. 1 人工的な問題を用いた評価
本節では, 順序符号化に適した制約，対数符号化に

d を 10, 20, 30, 40, 50, 60 で変化させた．ドメイ

適した制約の両方の制約を含むような人工的な問題

ンがあまり大きくなく，n が比較的大きいため問を考え，提案するハイブリッド符号化による相乗効果

題を解くために伝播が必要で順序符号化が効果を確認する．

的であると考えられる．

6. 1. 1 問題定義

6. 1. 2 実験結果

整数のパラメータ n, d と，ドメイン {0, . . . , d} を

表 1 は CPU 時間，各符号化で生成された節の数，持つような整数変数 xi , yi (1 ≤ i ≤ n) が与えられた

SAT ソルバーによる求解過程で生じた矛盾の回数を時に，以下のような制約をもつ CSP を考える．
n
n
n
∧
∑
∑
xi ≥ yi ∧xi <yi

比較したものである．以降，実験結果の表や図では順

i=1

i=1

i=1

x の和が y の和以上にならない制約からこの問題

序符号化を Order，対数符号化を Log，提案するハ
イブリッド符号化を Hybrid と参照する．

は任意の n と d に対して充足不能である．このベン表より対数符号化は非常にコンパクトな符号化をチマーク問題を生成する際には線形和 x1 + · · · + xn

行っており，n = 4 の場合には d = 300 になってものアリティが 3 になるまで新しい変数を導入して再10 秒以内に問題を解いていることが分かる．しかし

帰的に分割した (y についても同様)．例えば n = 4

ながら，n = 8 では対数符号化の求解性能が落ちていの時に問題は以下のようになる．

ることも分かる．理由は対数符号化では桁上げのため

x1 ≥ y1

x1 + x2 = u1x2 ≥ y2x3 + x4 = u2x3 ≥ y3

y1 + y2 = v 1

u1 + u2 = s

s<tの推論手続きが必要であり，より多くの値の伝播が必要な n = 8 で解を求めることが難しくなったのだと

v1 + v2 = t

考えられる．
対照的に，順序符号化は n = 8 の時に対数符号化

x4 ≥ y4
y3 + y4 = v 2
ここで u と v は部分和を表す補助変数であり，s とよりも少ない矛盾回数でより多くの問題を解いている

t は全体の和を表している．

ことが分かる．しかしながら，順序符号化では n = 4

この CSP は様々なドメイン積を一つの問題中にの時にドメイン d の大きさが 250 を超えると問題が含む．例えば，上述の例で d = 10 とするとドメイ

解けなくなった．原因として節数が膨大になったこと

ン積 DP(x1 + x2 = u1 ) は 100 であるのに対してが挙げられる．実際，n = 4 で d = 300 の時に順序DP(u1 + u2 = s) は 10000 になる．また n と d を符号化で生成される節数は 2179179 であり，これは変更することで問題の性質を制御することができる．

対数符号化の節数 1677 の 1000 倍以上になっている．

例えば d が大きくなると符号化節数が大きくなり対提案するハイブリッド符号化は適切にそれぞれの符数符号化に適した問題となる．一方，n が大きくなる

号化の長所を引き継いでおり，両符号化で解けた問題と xi への値割当が ⌊log2 n⌋ 個の補助変数を介してを全て解くことができた．また引き継ぐだけでなく，s へと伝播する必要があるため，伝播に優れた順序符

n = 8 の時にハイブリッド符号化は順序符号化，対数

号化に適した問題となる．

符号化のいずれよりも少ない矛盾回数で問題を解く

今回は以下二つのパラメータ集合を用いてベンチことに成功しており，ハイブリッドの相乗効果を確認

マークを生成し実験を行った．制限時間は 300 秒でできた．特に n = 8 と d = 60 の問題を制限時間内ある．

に解くことができたのはハイブリッド符号化のみで• 一つ目のパラメータ集合は n = 4 で固定とし，dを 50, 100, 150, 200, 250, 300 で変化させた．ド

あった．

表1

n

d

4

人工的な問題における CPU 時間，節数，矛盾回数の比較

CPU 時間 (秒)

符号化節数

矛盾回数

Order

Log

HybridOrder

Log

HybridOrder

Log

Hybrid

50

4.40

1.05

4.69

63,1791,088

33,64450,026

67,154

8,078

4

100

19.26

1.86

1.86

246,379

1,283

1,283

156,794

168,198

168,198

4

150

85.33

2.35

2.35

549,579

1,482

1,482

422,925

218,686

218,6864

200

257.63

4.14

4.13

972,779

1,470

1,470

935,133

436,850

436,850

4

250

TO

2.47

2.49

1,515,979

1,438

1,438

—

249,755

249,755

4

300

TO

6.88

6.90

2,179,179

1,677

1,677

—

716,163

716,163

8

10

1.29

1.24

1.28

12,923

1,691

12,923

8,508

61,529

8,508

8

20

4.43

31.80

3.95

48,283

2,118

29,77464,0662,339,531

11,722

8

30

35.91

87.11

7.80

106,043

1,998

62,986

536,078

6,498,426

26,737

8

40

45.63

TO

12.05

186,2032,529

45,177

500,552—

87,173850

131.39TO

22.19

288,763

2,487

67,5991,150,698—

142,961

8

60

TO

TO

35.95

413,723

2,441

94,633——

190,635

6. 2. 2 実験結果

Hybrid (815)

図 1 に示すベン図において，中心の数字 725 は各4

符号化で共通に解けた問題数を表している．同様に左4640

側の数 46 + 1 は順序符号化で解けて対数符号化で解725けない問題，右側の数 40 + 5 は対数符号化で解けて
1

0

5

Order (772)Log (770)

順序符号化で解けない問題を表している．ハイブリッ
ド符号化は，それらの 93% (86/92) を解いたうえで，図1求解できた問題を表すベン図

さらに両方の符号化で解けなかった 4 問の問題を解くことに成功した．これらのことより，提案するハイ

6. 2 CSP ソルバー競技会の問題を用いた評価

ブリッド符号化は CSP 競技会の問題 1002 問におい6. 2. 1 ベンチマークの説明て，順序符号化と対数符号化の融合を高いレベルで実

本節では 2009 年の CSP ソルバー競技会で用いられ現できたといえる．

た問題 1002 問についての比較結果を説明する．1002

表 2 は，それぞれの符号化によって解けた問題の数問の問題は競技会で使われた問題の全体集合から内包をシリーズ毎に示している．太字で示されたシリーズ

的制約であり連続ドメインを持つ全ての問題を抽出

はハイブリッド符号化の閾値をまたぐ複数のドメイン

した．ただし，PB の問題(363 問) については取

サイズの制約を含む問題である．すなわちこれらのり除いた．理由は 0-1 変数のみで構成される PB 制

シリーズでハイブリッド符号化は順序符号化，対数符

約には明らかに対数符号化が適しており，PB 制約に号化の両方も利用する．図 1 は，それぞれの符号化

は対数符号化が選ばれるようハイブリッド符号化が動で解けた問題の包含関係を示したベン図である．図 2

作するためである．実験で使用した 1002 問のドメイは，それぞれの符号化で解けた問題数と CPU 時間のンサイズは 1〜20001，アリティは 1〜50 に分布して関係を記載したカクタスプロットである．

おり，このことから様々な種類の問題が含まれている

順序符号化と対数符号化が 772 問と 770 問を解ことが分かる．全ての実験は 900 秒の時間制限で実いたのに対して，提案するハイブリッド符号化は最行した．

も多い 815 問を解いた．特に，“Fischer”, “Square表2

チマークに対して，Sugar を用いて実験を行った．結シリーズ毎の求解数

シリーズ名 (問題の数)

Ord.

Log Hyb.

果として，求解数は 787 でオーバーヘッドを抱えて

2D Strip Packing

(20)

8

7

8

いる提案方法による求解数が多かった．この差は既にAll Interval Series

(15)

9

9

9

節形式になっている PB から SAT への符号化のオー

BMC

(15)

15

15

15

バーヘッドが小さくなれば，より大きくなると考えら

Chessboard Col.

(15)

12

12

12

れる．

C. Job-Shop

(10)

5

4

5

Domino

(10)

9

10

9

Fischer

(25)

17

23

24

本論文では，順序符号化と対数符号化を融合した

Golomb Ruler

(28)

23

18

23

CSP のハイブリッド符号化を提案した．まず CSP のGraph Coloring

(141)

98

97

98

変数集合毎に異なる符号化を適用可能にする標準的Haystacks

(15)

3

1

3

ブール符号化の枠組みを提案し，次に具体的なハイブ

Job-Shop

(76)

67

61

67

リッド符号化の説明を行った．提案方法では与えられKnights

(10)

7

10

9

た CSP の変数集合を対数符号化するものと順序符号

Langford

(43)

27

24

27

化するものに分類する必要があるが，分類方法としてLatin Square

(10)

9

5

9

ドメイン積を用いた方法を提案した．

Magic Square

(18)

8

13

13

提案方法は公開ソフトウェア Diet-Sugar として実Multi Knapsack

(6)

4

6

6

装し，二つのベンチマークを使って評価を行った．人NengFa

(7)

7

6

7

工的なベンチマークを用いた評価では，提案するハ

Open-Shop

(75)

71

60

71

イブリッド符号化が順序符号化，対数符号化と比較しSquare Packing

(74)

56

56

57

てより少ない CPU 時間と矛盾回数で問題を解くこと

Pigeons

(29)

23

23

23

ができることを示した．特に n = 8, d = 60 の問題でPrimes

(76)

44

69

70

は，どちらの符号化でも解けない問題を解くことにQuasigroup Exist.

(5)

5

5

5

成功した．二つ目のベンチマークでは，順序符号化

Queens

(16)

11

12

11

で解けて対数符号化で解けない問題，対数符号化でQueens-Knights

(9)

9

9

9

解けて順序符号化で解けない問題の 93%を解くこと，

RCPSP

(78)

78

78

78

またどちらの符号化でも解けなかった 4 問をハイブ

Rader Surveillance (65)

65

65

65

リッド符号で解くことに成功した．最終的に求解した

Ramsey

(16)

10

10

10

問題数は順序符号化が 772 問，対数符号化が 770 問

Schurr’s Lemma

(10)

9

8

9

であるのに対して提案するハイブリッド符号化は 815

Super-solutions

(85)

63

54

63

問と最も多くの問題を解いた．これらの結果から提案(1002)

772

770

815

方法は高いレベルで二つの符号化のハイブリッド化を

Total

7 おわりに実現できているといえる．今後の研究課題として他の

Packing”, “Primes” ではハイブリッド符号化がどち

既存の SAT 符号化を実装し，ハイブリッド符号化にらの単一符号化でも解けない問題を解くことに成功

組み込むことは重要だと考えている．

した．
ここで注意したいのは，CSP の SAT 符号化に必要な時間は PB 制約が本質的に節形式になっている場合
でも PB を SAT に変換する時間を含むということである．このオーべーヘッドを調べるために，同じベン

参 考 文 献[ 1 ] Abı́o, I., Nieuwenhuis, R., Oliveras, A.,
Rodrı́guez-Carbonell, E., and Mayer-Eichberger,
V.: A New Look at BDDs for Pseudo-Boolean Constraints, Journal of Artificial Intelligence Research,

900
800

CPU Time (sec.)

700

Log
Order
Hybrid

600
500
400
300
200
100
0
500

550

600

650

700

750

800

850

#Instances Solved
図2

解けた問題の数と CPU 時間のカクタスプロット

Vol. 45(2012), pp. 443–480.
[ 2 ] Audemard, G. and Simon, L.: Predicting Learnt
Clauses Quality in Modern SAT Solvers, Proceedings of the 21st International Joint Conference on
Artificial Intelligence (IJCAI 2009), 2009, pp. 399–
404.
[ 3 ] Bailleux, O., Boufkhad, Y., and Roussel, O.:
A Translation of Pseudo Boolean Constraints to
SAT, Journal on Satisfiability, Boolean Modelingand Computation, Vol. 2, No. 1-4(2006), pp. 191–
200.
[ 4 ] Banbara, M., Matsunaka, H., Tamura, N., andInoue, K.: Generating Combinatorial Test Cases byEﬃcient SAT Encodings Suitable for CDCL SAT
Solvers, Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS 6397,
2010, pp. 112–126.
[ 5 ] Berre, D. L. and Parrain, A.: The Sat4j Library, release 2.2, Journal on Satisfiability, Boolean
Modeling and Computation, Vol. 7, No. 2-3(2010),
pp. 59–64.
[ 6 ] Biere, A.: Lingeling Essentials, A Tutorial on
Design and Implementation Aspects of the the SAT
Solver Lingeling, POS-14. Fifth Pragmatics of SAT
workshop, a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic, July 13, 2014, Vienna, Austria, 2014,
pp. 88.
[ 7 ] Biere, A., Heule, M., van Maaren, H., andWalsh, T.(eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications(FAIA), Vol. 185, IOS Press, 2009.
[ 8 ] Crawford, J. M. and Baker, A. B.: Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems, Proceedings of the

12th National Conference on Artificial Intelligence(AAAI 1994), 1994, pp. 1092–1097.
[ 9 ] de Kleer, J.: A Comparison of ATMS and CSP
Techniques, Proceedings of the 11th International
Joint Conference on Artificial Intelligence (IJCAI1989), 1989, pp. 290–296.
[10] Eén, N. and Sörensson, N.: Translating PseudoBoolean Constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation, Vol. 2,
No. 1-4(2006), pp. 1–26.
[11] Gebser, M., Kaufmann, B., Neumann, A., andSchaub, T.: Conflict-Driven Answer Set Solving,
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), 2007,
pp. 386–392.
[12] Gelder, A. V.: Another Look at Graph Coloring via Propositional Satisfiability, Discrete Applied
Mathematics, Vol. 156, No. 2(2008), pp. 230–243.
[13] Gent, I. P. and Nightingale, P.: A New Encoding of Alldiﬀerent into SAT, Proceedings of the 3rdInternational Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2004.
[14] Griva, I., Nash, S. G., and Sofer, A.: Linear
and Nonlinear Optimization, Society for Industrial
Mathematics, 2009.
[15] Heule, M. and Szeider, S.: A SAT Approach to
Clique-Width, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, 2013, pp. 318–334.
[16] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 57–67.
[17] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer
Congress, 1994, pp. 253–258.

[18] Lecoutre, C., Roussel, O., and van Dongen,
M. R. C.: Promoting Robust Black-box Solvers
Through Competitions, Constraints, Vol. 15,
No. 3(2010), pp. 317–326.
[19] Metodi, A. and Codish, M.: Compiling finite domain constraints to SAT with BEE, Theory andPractice of Logic Programming, Vol. 12, No. 45(2012), pp. 465–483.
[20] Nabeshima, H., Iwanuma, K., and Inoue, K.:
GlueMiniSat 2.2.8, Proceedings of SAT Competition
2014, 2014, pp. 35–36.
[21] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 68–76.
[22] Rossi, F., van Beek, P., and Walsh, T.: Handbook of Constraint Programming, Elsevier, 2006.
[23] Soh, T., Inoue, K., Tamura, N., Banbara, M.,
and Nabeshima, H.: A SAT-based Method for Solving the Two-dimensional Strip Packing Problem,
Fundamenta Informaticae, Vol. 102, No. 3-4(2010),
pp. 467–487.
[24] Soh, T., Tamura, N., and Banbara, M.: Scarab:
A Rapid Prototyping Tool for SAT-based Constraint Programming Systems, Proceedings of the
16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013),
LNCS 7962, July 2013, pp. 429–436.
[25] Stojadinovic, M. and Maric, F.: meSAT: multi-

ple encodings of CSP to SAT, Constraints, Vol. 19,
No. 4(2014), pp. 380–403.
[26] Tamura, N., Banbara, M., and Soh, T.: PBSugar: Compiling Pseudo-Boolean Constraints to
SAT with Order Encoding, Proceedings of the 25th
IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013), IEEE, November
2013, pp. 1020–1027.
[27] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Proceedings of the 12th International Conference on
Principles and Practice of Constraint Programming(CP 2006), LNCS 4204, 2006, pp. 590–603.
[28] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[29] 田村直之, 丹生智也, 番原睦則: SAT 変換に基づく
制約ソルバーとその性能評価, コンピュータソフトウェ
ア, Vol. 27, No. 4(2010), pp. 183–196.
[30] Tseitin, G. S.: On the complexity of derivations in the propositional calculus, Studies in Mathematics and Mathematical Logic Part II, (1968),
pp. 115–125.
[31] Walsh, T.: SAT v CSP, Proceedings of the 6thInternational Conference on Principles and Practice of Constraint Programming (CP 2000), 2000,
pp. 441–456.