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

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

宋 剛秀

番原 睦則

田村 直之

本論文では，擬似ブール (Pseudo-Boolean; PB) 制約の集合を命題論理式の充足可能性判定 (SAT) 問題へ符号化する新しい手法として，ブール基数 (Boolean Cardinality; BC) 制約を経由する方法を提案する．提案手法は，次の 3 つの特長を持つ．1 つ目は，SAT ソルバーの単位伝播により一般化アーク整合性の維持が可能な点である．2
つ目は，同じ解を持つ同値な PB 制約であれば係数や右辺の値が異なっても，同一の中間表現および SAT 問題に符号化可能な点である．3 つ目は，項数に対して係数の種類が少ない PB 制約に対しては，中間表現が簡潔になり少ない節数で SAT 符号化可能な点である．このような PB 制約は，国際 PB ソルバー競技会のベンチマーク問題にも頻出している．計算機実験では，代表的な既存手法で一般化アーク整合性維持が可能な BDD 法，およびそれより弱い
整合性検査が可能な Sorter 法と符号化後の節数と求解性能を比較した．結果として，異なる係数の種類が 10%以下であるような PB 制約について，提案手法が節数と求解性能に関して比較した 2 手法よりも良いことを確認した．

In this paper, we propose a new encoding method for a set of PB (Pseudo-Boolean) constraints into propositional satisfiability (SAT) problems, in which Boolean Cardinality (BC) constraints are used as an intermediate form. The proposed method has the following three features. First, it can maintain general arc
consistency by unit propagation of a SAT solver. Second, it can encode equivalent PB constraints withthe same solutions—even their coeﬃcients and right hand side value are diﬀerent—into the same intermediate form and SAT instance. Third, for PB constraints whose number of kinds of coeﬃcients is relatively
small compared with the number of terms, the intermediate form becomes simpler and they can be encodedwith a small number of clauses. Such PB constraints often appear in international PB solver competition
benchmarks. In experiments, we compared the proposed encoding method with existing methods, BDD
and Sorter. The former maintains general arc consistency by unit propagation, while the later maintains
consistency checking that is weaker than general arc consistency. As the result, for PB constraints in which
the number of diﬀerent coeﬃcients is not more than 10%, we confirmed that the proposed method is better
than those two methods in terms of the number of encoded clauses and the eﬃciency in solver performance.

可能性を判定する PB 問題は SAT 問題の拡張になっ

1 はじめにている．

SAT (Satisfiability) とは，与えられた命題論理式

SAT 問題を解くプログラムである SAT ソルバーの充足可能性を判定する問題である [8]．本論文で対[10] の性能が飛躍的に向上していることを背景とし象とする擬似ブール (Pseudo-Boolean; PB) 制約はて，PB 問題を SAT 問題に符号化 (変換) する研究

命題変数上の線形制約であり，PB 制約の集合の充足が活発に行われ，数多くの手法が提案されている[12] [7] [16] [11] [14]．これらの SAT 符号化手法の良し

A SAT Encoding of Pseudo-Boolean Constraints via
Boolean Cardinality Constraints
Yushi Minami, 神 戸 大 学 大 学 院 シ ス テ ム 情 報 学 研 究科, Graduate School of System Informatics, Kobe
University.
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.

悪しを考える代表的な基準には，整合性検査 (Consis-

tency Checking) あるいは一般化アーク整合性 (Generalized Arc Consistency; GAC) の維持が SAT ソル
バーの単位伝播により可能か否かという点がある [2]．
また，その上で符号化後の節数が少ない手法ほど良いとされるのが一般的である．整合性検査は，命題変数

への部分的な値割当てにより PB 制約が矛盾した場

機実験を行う．1 つ目では，異なった係数の種類が合，その矛盾を SAT ソルバーの単位伝播により検出一定の割合より少ない PB 制約をランダムに生成できるかどうかという基準である．一般化アーク整合
性は，現時点で PB 制約は矛盾していないが，さらにし，BDD 法，Sorter 法と符号化後の節数を比較する．
2 つ目では，2016 年国際 PB ソルバー競技会 †2 の

x = 0 (あるいは x = 1) とすると矛盾する時，x = 1

DEC-SMALLINT-LIN 部門の 1783 問を用い，同じ 2 手(あるいは x = 0) を単位伝播により検出できるかど

法と求解性能を比較する．これら 2 つの実験結果をうかという基準である．一般化アーク整合性のほうが通し，異なった係数の種類が比較的少ない PB 制約，より強く，その維持のほうが望ましい．

およびそれらを含む PB 問題について提案手法の有

国際 PB ソルバー競技会における優勝ソルバーの一つである MiniSat+†1 は BDD (Binary Decision Di-

効性を示す．

agram) 法，Sorter 法，Adder 法の 3 種類を利用して制約の連言標準形の式である BC-CNF 式を導入する．

n以降，第 2 節では SAT，PB 制約，BC 制約，BCいる [7]．BDD 法では，節数のオーダーは O(2 ) と第 3 節では提案する符号化手法の各ステップについ

最悪の場合に指数関数的となるが，一般化アーク整合て説明する．第 4 節で提案手法の特長と限界につい性が維持される．Sorter 法はソーティング回路を用て述べ，第 5 節で計算機実験の結果を考察する．最2

いた手法で，節数のオーダーは O(n log n) だが，一後に第 6 節で，本論文の結論を述べる．

般化アーク整合性が維持されず整合性検査のみが維持される．Adder 法は，加算回路を用いた手法で節2 SAT，PB 制約，BC 制約数のオーダーは O(n) で最も小さいが，一般化アーク

命題変数 p およびその否定 ¬p をリテラル (literal)，

整合性も整合性検査も維持されない．このように符号複数のリテラルの選言 (OR) を節 (clause)，複数の化手法には，それぞれ特徴があり得意な PB 制約は異節の連言 (AND) を CNF 式 (Conjunctive Normal

なる．既存手法にない特徴を持った符号化を考案する

Form formula) と呼ぶ．

ことは，重要な研究課題といえる．

SAT 問題とは，与えられた CNF 式を真にする命本 論 文 で は ，符 号 化 の 中 間 表 現 に ブ ー ル 基 数

題変数への値割当てが存在するか否かを判定する問(Boolean Cardinality; BC) 制約を用いる新しい手題である [8]．値割当てが存在する場合，CNF 式は法を提案する．BC 制約は係数が 1 の PB 制約であ充足可能 (satisfiable; sat) であると言い，存在しなり，効果的な SAT 符号化手法が知られている [15] [3]．

い場合，充足不能 (unsatisfiable; unsat) であると提案手法は，次の 3 つの特長を持つ．

言う．SAT ソルバーは，与えられた CNF 式が sat• SAT ソルバーの単位伝播により一般化アーク整合性の維持が可能• 同じ解を持つ同値な PB 制約であれば，係数や右辺の値が異なっていても，同一の中間表現および SAT 問題に符号化可能• 異なった係数の種類が比較的少ない PB 制約にか unsat かを判定し，sat ならその解となる値割当てを返すプログラムである [10] [6] [1] [9]．また，元の問題を CNF 式に変換することを SAT 符号化 (SAT

encoding) という．
擬似ブール制約 (PB 制約) は命題変数上の線形制
約であり，以下のように定義される [13]．

対しては，中間表現が簡潔になり少ない節数で定義 1 (PB 制約). Xn = (x1 , x2 , . . . , xn ) は同一の

SAT 符号化可能．このような PB 制約は，国際変数を含まないリテラルの列，ai および c は整数定

PB ソルバー競技会のベンチマーク問題にも頻出数， は関係演算子 (=, ≤, ≥) とする．この時，以している．

下の式を Xn 上の擬似ブール制約あるいは PB 制約

提案手法の有効性を評価するため，2 種類の計算†1 https://github.com/niklasso/minisatp†2 http://www.cril.univ-artois.fr/PB16/

図1

提案手法の概要と呼ぶ (真を 0，偽を 1 と解釈する)．
n∑ai xi  ci=1

項 ai xi で係数 ai が負の場合，その項を −ai ¬xi +aiに置き換えることで，係数を正にできる．また，項のを改良した方法により BC-CNF 式に符号化する(3. 2 節)．例えば，接頭和表現 2s1 + 2s5 + s6 ≥ 9は以下のような 3 つの BC 節から成る BC-CNF
式に符号化される．

(s1 ≥ 1) ∨ (s5 ≥ 3)

順序を入れ換えることで，PB 制約の左辺は係数の降(s5 ≥ 2)

順に項が並んでいるとしても一般性を失わない．すな(s5 ≥ 3) ∨ (s6 ≥ 3)

わち，以下では a1 ≥ a2 ≥ · · · ≥ an > 0 を仮定し，各PB 制約毎に定めるリテラル列 Xn = (x1 , x2 , . . . , xn )も対応する順序になっていると仮定する．さらに，特3. BC リテラル間および BC 節の関係を利用して不要な BC リテラルと BC 節の除去を行い，に必要がない限り関係演算子  が ≥ の場合について

BC-CNF 式を簡単化する (3. 3 節)．例えば，上議論し，≤ や = の場合の説明は省略する．

記の BC-CNF 式は以下のような 2 つの BC 節か関数 α : Xn → {0, 1} を Xn 上の値割当てと呼び，ら成る BC-CNF 式に簡単化される．

(s1 ≥ 1) ∨ (s5 ≥ 3)

これを n 桁の 2 進列 (α(x1 ), α(x2 ), . . . , α(xn )) で表(s6 ≥ 3)

す．すなわち，Xn 上の値割当て全体は {0, 1}n であり，これを Xn と表記する．値割当て α が PB 制約などの式 ϕ を満たす時，α を ϕ の解と呼び，ϕ の解の集合を Sol (ϕ) で表す．
ブール基数制約 (BC 制約) とは係数が全て 1 の PB∑
制約 ni=1 xi ≥ c のことを言う [13]．Xn 上の複数のBC 制約の選言を BC 節と呼び，BC 制約の集合で表す．複数の BC 節の連言を BC-CNF 式と呼び，BC節の集合で表す．また，BC 節に含まれる BC 制約をBC リテラルと呼ぶことがある．

4. BC 制約の SAT 符号化の 1 つであるシーケン
シャルカウンタ法 [15] を用いて，BC-CNF 式に現れるブール基数制約を SAT 問題に符号化し，さらに各 BC リテラルを命題変数のリテラルで置き換える (3. 4 節)．例えば，上記の BC-CNF
式は 2 つの節から成る CNF 式に SAT 符号化される．

s1,1 ∨ s5,3
s6,3
た だ し ，si,a は ，ブ ー ル 基 数 制 約 x1 + x2 +3 提案する SAT 符号化手法
提案手法により，PB 制約を BC-CNF 式を経由して命題論理の CNF 式へと符号化する各ステップは，
以下の通りである (図 1 参照)．

· · · + x6 ≥ 3 をシーケンシャルカウンタ法でSAT 符号化する時に導入された命題変数であり，
x1 + x2 + · · · + xi ≥ a を表す．
以下では，各ステップの詳細を述べる．

1. PB 制約を接頭和表現と呼ぶ形式に変換する (3. 1節)．例えば，PB 制約 5x1 + 3x2 + 3x3 + 3x4 +

3x5 + x6 ≥ 9 は，接頭和表現 2s1 + 2s5 + s6 ≥ 9に変換される．ただし，各 si は x1 + · · · + xi を表す．

2. 接頭和表現を，順序符号化アルゴリズム [17] [16]3. 1 PB 制約の接頭和表現への変換∑4
ある X4 上の PB 制約 ϕ :i=1 ai xi ≥ c について考える．もし (1, 0, 1, 0) が ϕ の解ならば，a2 ≥ a3
より (1, 1, 0, 0) も必ず解である．同様に (1, 0, 1, 1),(1, 1, 0, 1), (1, 1, 1, 0), (1, 1, 1, 1) も解となる．すなわ

ち，PB 制約∑ni=1 ai xi ≥ c の解の集合は，Xn 上のこ の 時 ，(Sn , ⪯) は 分 配 束 を 成 す．結 び v ⊔ v ′ =なんらかの順序の上方集合になっていると考えられる．

(max(v1 , v1′ ), . . . , max(vn , vn′ )) であり，交わり v ⊓以下では，PB 制約の接頭和表現を定義し，そのよ

v ′ = (min(v1 , v1′ ), . . . , min(vn , vn′ )) である．また，⪯

うな順序構造を導入する．
定義 2 (接頭和表現). Xn = (x1 , x2 , . . . , xn ) 上の PB∑
制約 ni=1 ai xi ≥ c に対し，以下の式をその接頭和表現という (ただし an+1 = 0 とみなす)．
n∑(ai − ai+1 ) (x1 + x2 + · · · + xi ) ≥ ci=1

以下では，各 x1 + x2 + · · · + xi を si で表し，Xn に対する i 番目の接頭和と呼ぶ．したがって，接頭和表の定義および bi ≥ 0 から明らかに，v ∈ Sn が接頭和∑′
表現 ni=1 bi si ≥ c の解の時，v ⪯ v を満たすべての v ′ ∈ Sn も解である．
次に，Xn 上の順序 ⪯ を対応する昇順列の順序 ⪯として定義する．
定義 3 (Xn 上の順序 ⪯). α = (u1 , u2 , . . . , un ) ∈ Xn ,α′ = (u′1 , u′2 , . . . , u′n ) ∈ Xn とする．Xn 上の順序 ⪯を以下のように定義する．

現を

n
∑

bi si ≥ cα ⪯ α′ ⇐⇒(u1 , u1 + u2 , . . . , u1 + · · · + un )⪯ (u′1 , u′1 + u′2 , . . . , u′1 + · · · + u′n )i=1のように記述する．ただし bi = ai − ai+1 であり，

a1 ≥ a2 ≥ · · · ≥ an > 0 より ∀i(bi ≥ 0) である．
例 1. PB 制約

5x1 + 3x2 + 3x3 + 3x4 + 3x5 + x6 ≥ 9の接頭和表現は，

2s1 + 2s5 + s6 ≥ 9である．

PB 制約と接頭和表現は 1 対 1 に対応する．また
Xn 上の PB 制約に対する可能な値割当ては n 桁の2 進列，すなわち Xn の要素で表され，一方，接頭和表現中の (s1 , s2 , . . . , sn ) に対する可能な値割当て
は，初期値が 0 か 1 で増分が 1 以下の昇順列で表される．例えば，2 進列 (1, 1, 0, 0, 0, 1) には昇順列(1, 2, 2, 2, 2, 3) が対応する．2 進列が PB 制約の解であることと，対応する昇順列がその接頭和表現の解であることは明らかに同値である．例えば，2 進列(1, 1, 0, 0, 0, 1) は例 1 の PB 制約の解になっており，対応する昇順列 (1, 2, 2, 2, 2, 3) はその接頭和表現の解になっている．また，2 進列 (1, 0, 1, 0, 0, 0) と対応する昇順列 (1, 1, 2, 2, 2, 2) のどちらも，それぞれの解ではない．
初期値が 0 か 1 で増分が 1 以下である長さ nの昇順列の集合を Sn で表し，それに直積順序を導 入 す る ．す な わ ち v = (v1 , v2 , . . . , vn ) ∈ Sn ,v ′ = (v1′ , v2′ , . . . , vn′ ) ∈ Sn の 時 ，v ⪯ v ′ ⇐⇒∀i(vi ≤ vi′ ) に よ り Sn 上 の 順 序 ⪯ を 定 義 す る ．

ただし右辺の ⪯ は上記の直積順序である．

(Xn , ⪯) は分配束を成し，結び α ⊔ α′ と交わり
α ⊓ α′ も対応する Sn の要素の結びと交わりとして定∑義できる．そして，α ∈ Xn が PB 制約 ni=1 ai xi ≥ cの解の時，α ⪯ α′ を満たすべての α′ ∈ Xn も解である．また，以下の命題が成り立つ (証明は省略)．
命題 1. α, α′ ∈ Xn とする．α ⪯ α′ ならば，Xn 上の任意の PB 制約 ϕ について α ∈ Sol (ϕ) ⇒ α′ ∈Sol (ϕ) である．逆もまた成り立つ．
PB 制約 ϕ の解の集合 Sol (ϕ) は (Xn , ⪯) の上方
集合 (upper set) になっている．したがって，Sol (ϕ)の極小元の集合を min(Sol (ϕ)) で表すと，Sol (ϕ) ={α′ ∈ Xn | α ∈ min(Sol (ϕ)), α ⪯ α′ } である．
また，補集合 Sol (ϕ) = Xn \ Sol (ϕ) は，(Xn , ⪯)の下方集合 (lower set) になっている．したがって，Sol (ϕ) の 極 大 元 の 集 合 を max(Sol (ϕ)) で 表 す と ，Sol (ϕ) = {α′ ∈ Xn | α ∈ max(Sol (ϕ)), α′ ⪯ α} である．
解 の 補 集 合 Sol (ϕ) に つ い て ，さ ら に 考 察 する ．例 1 の PB 制 約 5x1 + 3x2 + 3x3 + 3x4 +

3x5 + x6 ≥ 9 を ϕ で 表 し た 時 ，max(Sol (ϕ)) は{(0, 1, 1, 0, 0, 1), (1, 1, 0, 0, 0, 0)} で あ る ．す な わ ち
Sol (ϕ) は，α ⪯ (0, 1, 1, 0, 0, 1) ∨ α ⪯ (1, 1, 0, 0, 0, 0)を満たす α ∈ X4 の集合に一致する．(0, 1, 1, 0, 0, 1)に 対 応 す る S4 の 要 素 は (0, 1, 2, 2, 2, 3) だ か ら ，α ⪯ (0, 1, 1, 0, 0, 1) の 条 件 は ，接 頭 和 を 用 い てs1 ≤ 0 ∧ s2 ≤ 1 ∧ s3 ≤ 2 ∧ s4 ≤ 2 ∧ s5 ≤ 2 ∧ s6 ≤ 3を返す関数，Dom(Sj ) は Sj に割当てられた接頭和と 表 せ る ．同 様 に α ⪯ (1, 1, 0, 0, 0, 0) の 条 件 は

si のドメイン {0, 1, . . . , i} を返す関数である．また，

s1 ≤ 1 ∧ s2 ≤ 2 ∧ s3 ≤ 2 ∧ s4 ≤ 2 ∧ s5 ≤ 2 ∧ s6 ≤ 2

max と min は，それぞれ与えられた値あるいは集合と表せる．Sol (ϕ) の要素である条件は，これら 2 つのの最大値と最小値を返す．

選言となり，接頭和を用いた選言標準形 (Disjunctive

Normal Form; DNF) で表せることがわかる．
Sol (ϕ) の要素である条件は，Sol (ϕ) の条件の否定

Algorithm 1 の 4 行目では接頭和 S1 ≥ d が充足可能となる値 a の集合を D として求めており，5 行目
では充足不能となる値の集合を D ′ として求めていだから，以下の命題を得る (証明は省略)．

る．論文 [16] では，各接頭和 si ∈ {0, 1, . . . , i} の値が

命題 2. Xn 上の任意の PB 制約 ϕ に対し，Xn 上の独立だとして D と D′ を計算しているが，ここではBC-CNF 式 ψ が存在し Sol (ϕ) = Sol (ψ) である．

si ≤ si+1 ≤ si + 1 を用い，ありえない値を D と D′

なお，例 1 の PB 制約 5x1 +3x2 +3x3 +3x4 +3x5 +から省いている．これにより，多くの無駄な BC 節

x6 ≥ 9 の場合，後述する余分な BC リテラルの削除のの生成を避けることが可能になった．例えば，上記の処理を行うと BC-CNF 式 (s1 ≥ 1∨s5 ≥ 3)∧(s6 ≥ 3)

接頭和表現は以下の例 2 に示すように 3 個の BC 節が得られる．

に符号化され，大幅な BC 節数の削減を実現できている．

3. 2 接頭和表現の BC-CNF 式への符号化
接頭和表現中の各 si を整数変数と見なし，論文 [16]例 2. 例 1 に示した接頭和表現 2s1 + 2s5 + s6 ≥ 9 に適用した場合，以下の 3 個の BC 節に符号化される．

C1 : (s1 ≥ 1) ∨ (s5 ≥ 3)の順序符号化アルゴリズムを用いれば，接頭和表現を

C2 : (s5 ≥ 2)

BC-CNF 式に符号化することが可能である．

C3 : (s5 ≥ 3) ∨ (s6 ≥ 3)

しかし，この場合，各 si のドメイン {0, 1, . . . , i}はそれぞれ独立していると見なされ，接頭和間の関係

si ≤ si+1 ≤ si + 1 が考慮されず，多数の無駄な BC節が生成される．例えば，例 1 に示した接頭和表現

2s1 + 2s5 + s6 ≥ 9 の場合，8 個の BC 節となり余分な BC 節が含まれている．
そこで，接頭和間の関係 si ≤ si+1 ≤ si + 1 を符号化アルゴリズムに組み込んだ改良を行った．
改良した順序符号化アルゴリズムを Algorithm 1に示す．このアルゴリズムの第 1 引数は PB 制約の 接 頭 和 表 現 B1 S1 + · · · + Bn Sn ≥ c，第 2 引
数は直前の接頭和のインデックス i0 ，第 3 引数は
そ の 接 頭 和 に 対 す る 値 d0 で あ る ．例 え ば ，接 頭
和 表 現 2s1 + 2s5 + s6 ≥ 9 を 符 号 化 す る 際 の 引

3. 3 BC-CNF 式の簡単化
前節では，論文 [16] の順序符号化アルゴリズムの改
良方法について述べ，大幅な BC 節数の削減が実現できることを示した．しかし，まだ無駄な BC リテラ
ルや BC 節が存在する．
本節では，より一般的に BC 節から不要な BC リ
テラルを除去する方法，および BC-CNF 式から不要な BC 節を除去する方法について述べる．
定義 4. Xn 上の BC リテラル si ≥ a, sj ≥ b 間の含意関係を以下のように定義する．

si ≥ a ⇒ sj ≥ b ⇐⇒(i ≤ j ∧ a ≥ b) ∨ (i ≥ j ∧ i − a ≤ j − b)

数 は ，Encode(2s1 + 2s5 + s6 ≥ 9, 0, 0) で あ り，BC リテラルについて以下が成り立つ (証明は省略)．

(B1 , B2 , B3 ) = (2, 2, 1), (S1 , S2 , S3 ) = (s1 , s5 , s6 ) で∑ある．すなわち，接頭和表現
bi si ≥ c 中で bi = 0

命題 3. Xn 上の BC リテラル l, l′ について以下が成の部分は省かれており，Sj = si の時の接頭和のイン
デックス i は，index(Sj ) で与える．アルゴリズム中で，sup と inf はそれぞれ引数の式の最大値と最小値

り立つ．

l ⇒ l′ ⇐⇒ Sol (l) ⊆ Sol (l′ )この命題を用いることで不要な BC リテラルの除去を実現できる．すなわち，BC 節中の異なる BC リ

Algorithm 1 Encode(B1 S1 + · · · + Bn Sn ≥ c, i0 , d0 )1: if n = 1 then2:ψ ← {{(S1 ≥ ⌈c/B1 ⌉)}}
3: else∑n∑n
4:D ← {d ∈ Dom(S1 ) | d0 ≤ d ≤ index(S1 ) − i0 + d0 , c − sup(i=2 Bi (Si − index(S1 )) +i=2 Bi d ) ≤∑n∑n
B1 d < c − inf( i=2 Bi (Si − min(Dom(S1 ))) + i=2 Bi d )}∑n∑
5:D′ ← {d ∈ Dom(S1 ) | B1 d < c − sup( ni=2 Bi d )}i=2 Bi (Si − index(S1 )) +6:
ψ ← {{(S1 ≥ d + 1)} ∪ θ | d ∈ D, θ ∈ Encode(B2 S2 + · · · + Bn Sn ≥ c − B1 d, index(S1 ), d)}7:
if D′ ̸= ∅ then8:
ψ ← {{(S1 ≥ max(max(D′ ) + 1, d0 )}} ∪ ψ
9:end if
10: end if
11: return ψ

テラル l, l′ について l ⇒ l′ が成り立つ時，その BCできる．すなわち，BC-CNF 式中の異なる BC 節 C,

節から BC リテラル l を除去して良い．

C ′ について C ⇒ C ′ が成り立つ時，その BC-CNF

例 3. 例 2 の BC-CNF 式において，s5 ≥ 3 ⇒ s6 ≥ 3

式から BC 節 C ′ を除去して良い．

より C3 中の BC リテラル s5 ≥ 3 を除去できる．

例 4. 例 3 の BC-CNF 式において，C3 ⇒ C2 より

定義 5. Xn 上の BC 節 C, C ′ 間の含意関係を以下のBC 節 C2 を除去でき，以下を得る．
C1 :(s1 ≥ 1) ∨ (s5 ≥ 3)

ように定義する．

C ⇒ C ′ ⇐⇒ ∀l ∈ C ∃l′ ∈ C ′ (l ⇒ l′ )以下の補題と命題が成り立つ．

C3 :(s6 ≥ 3)

後述の 4. 2 節で示すように，上記の簡単化を繰り返すことで，同値な PB 制約からは同一の BC-CNF

補題 1. Xn 上の BC リテラル l, l1 , l2 について，式が得られる．そこで，不要な BC リテラルをすべ

Sol (l) ⊆ Sol (l1 ∨ l2 ) ならば，Sol (l) ⊆ Sol (l1 ) またて除去した BC 節を既約な BC 節と呼び，さらに不は Sol (l) ⊆ Sol (l2 ) が成り立つ．

要な BC 節をすべて除去した BC-CNF 式を既約な

Proof. Sol (l) が空の場合は明らか．空でなければ最BC-CNF 式と呼ぶ．

小元 α を持つ．α は Sol (l1 ) または Sol (l2 ) に含まれるから，Sol (l) ⊆ Sol (l1 ) または Sol (l) ⊆ Sol (l2 ) が成り立つ．

3. 4 BC-CNF 式の SAT 符号化
BC 制約を SAT に符号化する良い手法の 1 つとして知られているシーケンシャルカウンタ法 [15] を用い

命題 4. Xn 上の BC 節 C, C ′ について以下が成り立つ．

れば，BC-CNF 式を容易に SAT 符号化できる．
∑ni=1 bi si ≥ c を PB 制約の接頭和表現とする．

C ⇒ C ′ ⇐⇒ Sol (C) ⊆ Sol (C ′ )si ≥ a を意味するブール変数 si,a を導入し，シーケン

Proof. (=⇒) 明らか．(⇐=) ∃l ∈ C ∀l′ ∈ C ′ (l ̸⇒ l′ )シャルカウンタ法により以下のような節を生成する．

と仮定し矛盾を導く．仮定を満たす BC リテラル
を l ∈ C とする．Sol (C) ⊆ Sol (C ′ ) より Sol (l) ⊆Sol (C ′ ) であり，補題 1 より，ある l′ ∈ C ′ についてSol (l) ⊆ Sol (l′ ) である．したがって，命題 3 よりl ⇒ l′ だが，これは仮定に矛盾する．
この命題を用いることで不要な BC 節の除去を実現

si−1,a−1 ∨ ¬si,a(1 ≤ a ≤ n, 1 ≤ i ≤ n)si−1,a ∨ xi ∨ ¬si,a(1 ≤ a ≤ n, 1 ≤ i ≤ n)

ただし，リテラル si,a (i < a) および，si ≥ 0 を含む節は削除する．
∑この時， ni=1 bi si ≥ c を符号化した BC-CNF 式において，各 BC リテラル si ≥ a を命題変数 si,a で置き換えれば良い．
例 5. 例 4 の BC-CNF 式を SAT 符号化した結果は，

x1 + x2 + · · · + x6 ≥ 3 に対しシーケンシャルカウン

すなわち C 中のある BC リテラル sj,a は，α で未定

タ法で SAT 符号化した節に加え，以下の節で与えら義であるが，α′ で 0 になる．したがって，α のもとれる．

で，sj,a = 1 が単位伝播され，さらにシーケンシャル

C1 :s1,1 ∨ s5,3

カウンタ部分に対する単位伝播で xi = 1 が得られる．

C3 :

s6,3

例 6. PB 制約 3x1 + 2x2 + 2x3 + x4 + x5 ≥ 5 を

また，シーケンシャルカウンタ法では，SAT ソル

例に取る．部分値割当て x2 = x3 = 0 の状況から，

バーの単位伝播により一般化アーク整合性維持が可

x1 = x4 = x5 = 1 が SAT ソルバーの単位伝播で導能であることが知られている [15]．

出されなければならない．提案手法で得られている

CNF 式は以下の通りである．

4 提案手法の特長

C1 : x1 ∨ ¬s1,1

C2 : s1,1 ∨ x2 ∨ ¬s2,1

本節では以下に示す提案手法の 3 つの特長についC3 : s1,1 ∨ ¬s2,2

C4 : x2 ∨ ¬s2,2

C5 : s2,1 ∨ x3 ∨ ¬s3,1

C6 : s2,1 ∨ ¬s3,2て説明する．

• SAT ソルバーの単位伝播により一般化アーク整C7 : s2,2 ∨ x3 ∨ ¬s3,2

C8 : s2,2 ∨ ¬s3,3

C9 : x3 ∨ ¬s3,3

C10 : s3,1 ∨ x4 ∨ ¬s4,1• 同じ解を持つ同値な PB 制約であれば，係数やC11 : s3,1 ∨ ¬s4,2

C12 : s3,2 ∨ x4 ∨ ¬s4,2

右辺の値が異なっていても，同一の中間表現およ

C13 : s3,2 ∨ ¬s4,3

C14 : s3,3 ∨ x4 ∨ ¬s4,3

び SAT 問題に符号化可能合性の維持が可能

C15 : s4,1 ∨ x5 ∨ ¬s5,1

C16 : s4,1 ∨ ¬s5,2• 異なった係数の種類が比較的少ない PB 制約に

C17 : s4,2 ∨ x5 ∨ ¬s5,2

C18 : s4,2 ∨ ¬s5,3

対しては，中間表現が簡潔になり少ない節数でC19 : s4,3 ∨ x5 ∨ ¬s5,3

C20 : s3,2 ∨ s5,3

SAT 符号化可能

C21 : s1,1 ∨ s3,2

C22 : s1,1 ∨ s5,3さらに，提案手法の節数が指数関数的に増加するような場合についても考察を行う．

C1 から C19 はシーケンシャルカウンタの部分であり，C20 から C22 が BC-CNF 式に対応した部分である．x2 = x3 = 0 の時，C4 , C7 , C9 , C13 から，単位4. 1 単位伝播による一般化アーク整合性の維持

伝播により s2,2 = s3,2 = s3,3 = s4,3 = 0 が導かれ

提案手法は，シーケンシャルカウンタと同じく一般

る．さらに，BC-CNF 式に対応した節 C20 , C21 から化アーク整合性の維持が可能であり，したがって整合

s1,1 = s5,3 = 1，すなわち s1 ≥ 1 と s5 ≥ 3 が単位伝性検査も維持される．

播で得られる．最後に，再度シーケンシャルカウンタ

提案手法で変換された SAT 問題は，シーケンシャ
ルカウンタを表す部分と BC-CNF 式を表す部分に分かれている．リテラル列 Xn に対する部分的な値割当てを α とする．シーケンシャルカウンタ部分により，α により成立する BC リテラル si ≥ a に対応する変数 si,a は単位伝播で 1 に割当てられ，矛盾する BC
リテラル si ≥ a に対応する変数 si,a は 0 に割当てられる．したがって，α で元の PB 制約が矛盾する場
合，BC-CNF 式中のある BC 節が矛盾することが単位伝播で検出でき，整合性検査が維持される．また，

α で元の PB 制約は矛盾せず，α に xi = 0 を追加した α′ で矛盾する場合，BC-CNF 式中のある BC 節

C について，それは α では矛盾せず α′ で矛盾する．

部分での単位伝播により x1 = x4 = x5 = 1 となる．
このように提案手法では SAT ソルバーの単位伝播により一般化アーク整合性の維持が可能であり，符号化後の SAT 問題を SAT ソルバーで解く際に，効率的な枝刈りが実現され，無駄な探索を避けることができる．

4. 2 同値な PB 制約に対する符号化
以下では，同値な PB 制約から得られる既約な BC-

CNF 式は同一になることの証明を示す．まず，既約な BC 節の同等性について，以下の補題と命題が成り立つ．

補題 2. Xn 上の既約な BC 節 C = {l1 , . . . , lm } につの場合も同様である．したがって，各 αi は Sol (ψ) のいて，C 中の BC リテラル li は Sol (C) の極小元 αi

極大元になっており，i ̸= j ならば αi ̸= αj である．

と 1 対 1 に対応し，{αi } = min(Sol (li )) である．

Proof. 恒偽でない BC リテラル l はただ 1 つの極小元(最小元) を持つ．そこで，各 li ∈ C について Sol (li )の最小元を αi と置く．この時，i ̸= j ならば αi ̸⪯ αj
かつ αj ̸⪯ αi が成り立つ．なぜなら，αi ⪯ αj とす
ると Sol (lj ) ⊆ Sol (li ) であり，命題 3 より lj ⇒ li が∪逆に，α を Sol (ψ) の任意の極大元とする．Sol (ψ) =C∈ψ Sol (¬Ci )よ り，α が 極 大 元 に なって い る

Sol (¬Ci ) が存在する．
定理 1. Xn 上の既約な BC-CNF 式 ψ, ψ ′ について
以下が成り立つ．

ψ = ψ ′ ⇐⇒ Sol (ψ) = Sol (ψ ′ )成り立ち，C が既約であることに反する．αj ⪯ αi の場合も同様である．したがって，各 αi は Sol (C) のProof. (=⇒) 明らか．(⇐=) 補題 3 より，ψ の BC 節

極小元になっており，i ̸= j ならば αi ̸= αj である．

C と ψ ′ の BC 節 C ′ は 1 対 1 に対応し，Sol (¬C) =逆に，α を Sol (C) の任意の極小元とする．α はあSol (¬C ′ )，すなわち Sol (C) = Sol (C ′ ) である．さる BC リテラル li の最小解になっている．
命題 5. Xn 上の既約な BC 節 C, C ′ について以下がらに，命題 5 より C = C ′ である．
以上により，同値な PB 制約に対する既約な BC-

CNF 式は常に同一になることが示せた．

成り立つ．
′

′

C = C ⇐⇒ Sol (C) = Sol (C )Proof. (=⇒) 明 ら か ．(⇐=) C と C ′ の 極 小 解 を{α1 , . . . , αm } と す る ．補 題 2 よ り，C は {αi } =min(Sol (li )) を満たす BC リテラル li の集合であり，C ′ もまたそうだから，C = C ′ である．
既約な BC-CNF 式の同等性について，以下の補題と定理が成り立つ．
補題 3. ψ = {C1 , . . . , Cm } を Xn 上の既約な BC-

CNF 式とする．ψ の BC 節 Ci は ψ の解の補集合

2 つの PB 制約が同値であるかどうかの判定問題
は co-NP 完全なので，co-NP̸=P を仮定すると，既約な BC-CNF 式を求める多項式時間の手続きは存在
しない．

4. 3 PB 制約の項数に対して係数の種類が少ない
ときの符号化節数
提案手法には，PB 制約の項数に対して係数の種類が少ないときに，PB 制約を効果的に SAT 符号化できる，別の言い方をすると，PB 制約の同じ係数の変の 極 大 元 αi ∈ max(Sol (ψ)) と 1 対 1 に 対 応 し ，数の数が増えても符号化節数が増えにくいという長所{αi } = max(Sol (¬Ci )) である．

がある．以下では，例を用いてこの長所を説明する．

Proof. 恒真でない BC リテラル l = (si ≥ a) について，¬l = (si ≤ a − 1) の解 Sol (¬l) はただ 1 つの極大元を持つ．したがって，恒真でない BC 節 C につ∩いて，Sol (¬C) = l∈C Sol (¬l) はただ 1 つの極大元(最大元) を持つ．
そこで，各 Ci ∈ ψ について Sol (¬Ci ) の最大元を αiと置く．すなわち，Sol (¬Ci ) = {α ∈ Xn | α ⪯ αi }で あ る ．こ の 時 ，i ̸= j な ら ば αi ̸⪯ αj か つ

αj ̸⪯ αi が成り立つ．なぜなら，αi ⪯ αj とするとSol (¬Ci ) ⊆ Sol (¬Cj ) であり，命題 4 より Cj ⇒ Ci
が成り立ち，ψ が既約であることに反する．αj ⪯ αi

3. 2 節で述べた PB 制約 5x1 + 3x2 + 3x3 + 3x4 +
3x5 +x6 ≥ 9，および，その接頭和表現 2s1 +2s5 +s6 ≥9 について考える．提案手法で符号化すると以下のBC-CNF 式が得られる．
C1 : (s1 ≥ 1) ∨ (s5 ≥ 3)
C2 :(s5 ≥ 2)C3 :(s5 ≥ 3) ∨ (s6 ≥ 3)

この 6 項の PB 制約に対し，係数が 3 である変数
を 4 つ増やした 10 項の PB 制約 5x1 + 3x2 + 3x3 +3x4 + 3x5 + 3x6 + 3x7 + 3x8 + 3x9 + x10 ≥ 9，および，その接頭和表現 2s1 + 2s9 + s10 ≥ 9 について考える．この PB 制約を BC-CNF 式に符号化すると，以下の BC-CNF 式が得られ，これは上述の 6 項の場
合の BC-CNF 式における接頭和 s5 , s6 が，s9 , s10 に置き換わったものとなっている．
C1 : (s1 ≥ 1) ∨ (s9 ≥ 3)

C2 :(s9 ≥ 2)C3 :(s9 ≥ 3) ∨ (s10 ≥ 3)

{1, 2, . . . , n} の部分集合でその和が ⌊n(n + 1)/4⌋ に√3一致する個数となり，その値は π6 2n n− 2 で近似される †3 ．したがって，指数オーダーの BC 節数が必要となる．

5 計算機実験
本節では, 提案手法と既存手法である BDD 法およこのように，提案手法では，接頭和表現により同び Sorter 法 [7] に対し，比較のために行った計算機実

じ係数の変数の値の和の範囲によって場合分けされ験とその結果について説明し，提案手法の有効性とそるから，PB 制約の項数が増えても，同じ係数であれの特長を評価する．なお Adder 法で生成される節数ば，接頭和表現でまとめて表すことができる．よってのオーダーは O(n) であるが，SAT ソルバーの単位

BC-CNF 式の BC 節数は増えない．

伝播では一般化アーク整合性も整合性検査も維持さ

この場合，SAT 符号化後の SAT 問題におけるシー

れないため，本論文では比較の対象としない．

ケンシャルカウンタを表す部分のみ節数が増える．こ最初に，異なった係数の種類が比較的少ない PB 制の例だと，最終的に提案手法で生成される SAT 問題

約について，ランダムに生成した 1100 問を用い，提の節数は，前者の PB 制約が 20 節，後者の PB 制約

案手法と既存手法で生成される節数について比較すが 40 節となる．

る．このような問題は提案手法が有効に働く場合であ

一方，BDD 法 [7] の場合を考えると，変数が取りり，既存手法との違いを明らかにする．

うる値の場合分けを行うから，上述の例で 6 項から

次 に ，2016 年 国 際 PB ソ ル バ ー 競 技 会 の10 項に増えた時に，前者の PB 制約が 28 節，後者のDEC-SMALLINT-LIN 部門の 1783 問を用い，求解性

PB 制約が 72 節となり，提案手法に比べ節数の増え

能 (時間制限内の解けた問題数) を比較する．また，方が大きくなる．

これらの問題を異なった係数の種類が比較的少ない問

また，後述の，2016 年国際 PB ソルバー競技会

DEC-SMALLINT-LIN 部門での問題 1783 問では，PB

題とそうでない問題に分類し，既存手法との違いについて評価する．

制約の項数に対する係数の種類の数の割合が最大でなお，提案手法の実装は，次の 4 つのプログラムか10%以下の問題が 856 問あり，項数に対して係数のら構成されている: i) PB 制約を接頭和にするプログ

種類が少ない PB 制約は多く存在する．そのような

ラム，ii) 接頭和を BC-CNF 式に符号化するプログ

PB 制約に対し，提案手法は，同じく単位伝播により

ラム，iii) BC-CNF 式を簡単化するプログラム，iv)

一般化アーク整合性を維持できる BDD 法と比べ，節BC-CNF 式を SAT 問題に符号化するプログラム．ま

数が小さな SAT 問題に符号化することができる．

た，プログラムはすべて Scala 言語を用いて記述されている．

4. 4 BC-CNF 式が指数関数的に増大する場合

比較には，論文 [7] で提案され，代表的な PB 制約

提案手法で PB 制約を SAT 符号化した場合，シーの SAT 符号化手法となっている以下の 2 つを用いた．

ケンシャルカウンタ x1 + · · · + xn ≥ k の部分から• BDD 法：二分決定木を用いた手法．

生成される節数は O(nk) で多項式的であるが [15]，• Sorter 法：ソーティング回路を用いた手法．

BC-CNF 式の部分は指数的に増大する場合が存在実験では，これらの SAT 符号化手法の実装として，する．

国際 PB ソルバー競技会における優勝ソルバーの一つである MiniSat+†4 を用いた．

例えば，PB 制約∑ni=1 (n − i + 1)xi

≥ ⌊n(n +1)/4⌋ + 1 の場合，BC-CNF 式中の BC 節数は，集合†3 https://oeis.org/A025591†4 https://github.com/niklasso/minisatp

60000
BDD
Sorter
提案手法

50000

節数

40000
30000
20000
10000
0

図2
表1

20

30

40

項数

50

60

70

係数種類の割合が 10%である PB 制約に対する提案手法と既存手法の SAT 節数の比較

DEC-SMALLINT-LIN 部門の問題 1783 問における提案手法と既存手法の解けた問題数と平均節数の比較

提案手法
係数種類の割合

問題数

BDD

Sorter

解けた

節数の

解けた

節数の

解けた

節数の

問題数

平均

問題数

平均

問題数

平均

10%以下

856

693

2421

685

3338

673

111680

その他

927

458

160692602

119741

570

188336

5. 1 ランダムに生成した 1100 問での比較• 項数：n ∈ {20, 25, · · · , 70}

本節では, 最初に，異なった係数の種類が比較的少• 係数：1 ≤ ai ≤ 5000∑
• 右辺：c = ⌈ n
i=1 ai /2⌉

ない PB 制約について，ランダムに生成した 1100 問を用い，提案手法と既存手法で生成される節数についこの条件のもとで，各項数に対し 100 個の PB 制て比較する．

約を生成し，計 1100 個の PB 制約を生成した．な

まず，係数種類の割合を以下のように定義する．
係数の種類の個数
係数種類の割合 =PB 制約の項数 n例えば，50 項の PB 制約で，異なった係数が 5 種類

お，2016 年の国際 PB ソルバー競技会で使われた

DEC-SMALLINT-LIN 部門の問題 1783 問の中，項数が現れている場合，係数種類の割合は 10%である．

図 2 は, 各項数に対する平均節数をプロットしたも70 以下で係数が 5000 以下の問題は 1287 問である．

提案手法は，異なった係数の種類が少なければ少なのである．提案手法が最も節数が小さくなっており，

いほど生成される節数が減少するが，ここでは係数種

また，提案手法の項数の増加に伴う節数の増加量も他類の割合が 10%の場合について評価する．なお，2016に比べ小さくなっている．これは，4. 3 節で述べたよ

年国際 PB ソルバー競技会の DEC-SMALLINT-LIN 部

うに，提案手法は，同じ係数の変数が増えても節数が門の 1783 問中，問題中に現れている全 PB 制約の係増えにくいという性質を持っている特長が行かされた

数種類の割合が 10%以下になっているものは 856 問からだと考えられる．

で，半数近くがそのような問題である．
係数種類の割合を 10%とした上で，以下の条件で∑PB 制約 ni=1 ai xi ≥ c をランダムに生成した．

5. 2 国際 PB ソルバー競技会のベンチマーク問

題での比較
本 節 で は ，2016 年 国 際 PB ソ ル バ ー 競 技 会 のDEC-SMALLINT-LIN 部門の 1783 問を用い，提案手

処理時間が増大したと考えられる．すべての組合せを調べないで BC 節の除去を実現する手法の考案は，今後の研究課題である．

法と既存手法の求解性能 (時間制限内の解けた問題
数) を比較する．比較する既存手法は，前節と同じく

6 結論

BDD 法と Sorter 法の 2 種類である．また，これら

本論文では, BC 制約を経由した PB 制約の新しいの問題を異なった係数の種類が比較的少ない問題とそSAT 符号化手法を提案した. 提案手法では, 与えられうでない問題に分類し，既存手法との違いについて評た PB 制約の接頭和表現を求め, 順序符号化を改良し価する．

たアルゴリズムを用いて BC-CNF 式に符号化し, 無実験では，まず各手法によって PB 問題を制限時間

駄な BC リテラルと BC 節を除去した後, シーケン

600 秒で符号化して SAT 問題を生成した．その後，シャルカウンタ法を用いて SAT 符号化を行っている.

SAT ソルバー MiniSat version 2.2 [5] を用いて生成提案手法は，次の 3 つの特長をもつ．

された SAT 問題を解き，制限時間 600 秒以内で解けた問題数を比較した．実験には CPU に Intel Xeon

• SAT ソルバーの単位伝播により一般化アーク整合性の維持が可能

3.00GHz, メモリ 16GB を搭載したマシンを用いた.

• 同じ解を持つ同値な PB 制約であれば，係数や表 1 に, 各手法で解けた問題数と節数の平均値を示

右辺の値が異なっていても，同一の中間表現およす．表内の 1 行目は，係数種類の割合が 10%以下のPB 制約だけが含まれている問題に対する値であり，2 行目はその他の問題に対する値である．

び SAT 問題に符号化可能• 異なった係数の種類が比較的少ない PB 制約に対しては，中間表現が簡潔になり少ない節数で係数種類の割合が 10%以下である PB 問題に対し

SAT 符号化可能．このような PB 制約は，国際て，提案手法が最も求解数が多く，平均節数も少なく

PB ソルバー競技会のベンチマーク問題にも頻出

なった．

している．

BDD 法と比較すると，求解数の差はわずかであ

計算機実験の結果，PB 制約の項数に対して係数るが多く，また節数は約 70%に減少している．また，の種類が 10%以下であるようなランダムに生成した

Sorter 法と比較した場合，その差はより大きい．特PB 制約に対しては，代表的な既存手法である BDDに，Sorter 法で生成される節数は提案手法の 46 倍以法，Sorter 法よりも少ない節数で符号化できること上になっている．したがって，異なった係数の種類がが分かった．また 2016 年の国際 PB ソルバー競技会

比較的少ない問題については，既存手法より優れた手で使われた 1783 問の問題に対しては，やはり PB 制法といえる．

約の項数に対して係数の種類の割合の最大が 10%以

しかし，その他の問題について見ると，節数の差は下であるような PB 問題に対して，他の既存手法よりそれほど大きくないが，制限時間 600 秒以内に解けたも多くの問題を解くことができ有効であることが分問題数では大きく差がついた．これは，SAT 符号化

かった．

自体が制限時間以内にできなかったことが 1 つの原因

今後の課題として，基数制約を直接扱うことができである．係数種類の割合が 10%以下のもので符号化る SAT ソルバーの利用や [4]，計算機実験の節で議論できなかった問題は 856 問中 10 問だったが，その他したように，高速な符号化・簡単化アルゴリズムを研の問題では 927 問中 158 問だった．詳細に調べた所，究することが挙げられる．

要した時間のほとんどは 3. 3 節で述べた BC-CNF 式の簡単化の処理が占めていた．現在の実装では，BC

参 考 文 献節の除去において，2 つの BC 節を選択するすべての[ 1 ] Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers.

組合せに対し，包摂の条件を調べている．このため，

In Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp.
399–404, 2009.
[ 2 ] Fahiem Bacchus. GAC via unit propagation. In
Proceedings of the 13th International Joint Conference on Principles and Practice of Constraint Programming (CP 2007), LNCS 4741, pp. 133–147,
2007.
[ 3 ] Olivier Bailleux and Yacine Boufkhad. Eﬃcient
CNF encoding of Boolean cardinality constraints.
In Proceedings of the 9th International Joint Conference on Principles and Practice of Constraint
Programming (CP 2003), LNCS 2833, pp. 108–122,
2003.
[ 4 ] Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean
Modeling and Computation, Vol. 7, No. 2-3, pp. 59–
64, 2010.
[ 5 ] Niklas Eén and Niklas Sörensson. An extensible
SAT-solver. In Proceedings of the 6th International
Conference on Theory and Applications of Satisfiability Testing (SAT 2003), LNCS 2919, pp. 502–
518, 2003.
[ 6 ] Niklas Eén and Niklas Sörensson. MiniSat: A
SAT solver with conflict-clause minimization. In
Proceedings of the 8th International Conference on
Theory and Applications of Satisfiability Testing(SAT 2005), LNCS 3569, pp. 502–518, 2005.
[ 7 ] Niklas Eén and Niklas Sörensson. Translating
pseudo-Boolean constraints into SAT. Journal on
Satisfiability, Boolean Modeling and Computation,
Vol. 2, No. 1-4, pp. 1–26, 2006.
[ 8 ] 井上克巳, 田村直之. SAT ソルバーの基礎. 人工知能学会誌, Vol. 25, No. 1, pp. 57–67, 2010.
[ 9 ] Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue. GlueMiniSat 2.2.8. In Proceedings of
SAT Competition 2014, pp. 35–36, 2014.
[10] 鍋島英知, 宋剛秀. 高速 SAT ソルバーの原理. 人工知能学会誌, Vol. 25, No. 1, pp. 68–76, 2010.

[11] Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa,
Miyuki Koshimura, and Hiroshi Fujita. Modulo
based CNF encoding of cardinality constraints andits 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.
[12] 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 Satisfiability
Testing (SAT 2015), pp. 9–16, 2015.
[13] Olivier Roussel and Vasco M. Manquinho.
Pseudo-Boolean and cardinality constraints. In
Armin Biere, Marijn Heule, Hans van Maaren, andToby Walsh, editors, Handbook of Satisfiability, Vol.
185 of Frontiers in Artificial Intelligence and Applications, pp. 695–733. IOS Press, 2009.
[14] Masahiko Sakai and Hidetomo Nabeshima. Construction 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.
[15] Carsten Sinz. Towards an optimal CNF encodingof Boolean cardinality constraints. In Proceedings ofthe 11th International Joint Conference on Principles and Practice of Constraint Programming (CP2005), LNCS 3709, pp. 827–831, 2005.
[16] Naoyuki Tamura, Mutsunori Banbara, andTakehide Soh. PBSugar: Compiling pseudo-boolean
constraints to SAT with order encoding. In Proceedings of the 25th IEEE International Conferenceon Tools with Artificial Intelligence (ICTAI 2013),
IEEE, pp. 1020–1027, November 2013.
[17] Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear CSP into SAT. Constraints, Vol. 14, No. 2, pp.
254–272, 2009.