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

解集合プログラミングに基づく組合せ遷移ソルバーの実装方式に関する考察
山田 悠也

湊 真一

番原 睦則

組合せ遷移問題とは，基となる組合せ問題とその 2 つの実行可能解が与えられたとき，一方の実行可能解から他方の実行可能解へ，遷移制約を満たしつつ，実行可能解のみを経由して到達できるかを判定する問題である．計算困難性について，基の組合せ問題が NP 完全であるとき，その遷移問題の多くは PSPACE 完全になることが知られている．本稿では，解集合プログラミング (ASP) を用いた組合せ遷移問題の解法として，有界組合せ遷移を提案し，そのソルバーの実装方法について述べる．有界組合せ遷移は，組合せ遷移問題に対して，制限された長さの (すなわち有界の) 遷移系列を論理プログラムとして記号的に表現し，その論理プログラムを ASP システムで実行することにより，到達可能性の検査を行う．有界組合せ遷移の有効性を評価するために，代表的な組合せ遷移問題の 1 つである
k 彩色遷移問題をベンチマークとして，提案ソルバーの性能評価を行った．

の切替えなど持続的システムへの実用的応用が期待

1 はじめにされている．しかしながら，一般の組合せ遷移問題を組合せ遷移問題 (Combinatorial Reconﬁguration

解く汎用ソルバーのアルゴリズム，ヒューリスティッ

Problems; CoRe [12] [14] [16]) とは，基となる組合せ

クスなどの実践的な研究開発はまだ始まったばかりで問題とその 2 つの実行可能解が与えられたとき，一ある．著者らの知る限り，実用的な汎用ソルバーはま方の実行可能解から他方の実行可能解へ，遷移制約をだ存在していない．

満たしつつ，実行可能解のみを経由して到達できるかどうかを判定する問題である．

解集合プログラミング (Answer Set Programming;

ASP [2] [9] [11] [13]) は，論理プログラミングから派生

計算困難性について，基の組合せ問題が NP 完全した宣言的プログラミングパラダイムである．ASPであるとき，その遷移問題の多くは PSPACE 完全に

言語は一階論理に基づく知識表現言語の一種である．

なることが知られている．代表的なものとしては，命ASP システムは安定モデル意味論 [9] に基づく解集

題論理の充足可能性判定問題 (SAT)，集合被覆問題，

合を計算するシステムである．近年，SAT の技術を

独立点集合，グラフ点彩色問題を基とする組合せ遷移応用した高速な ASP システムが開発され，プランニ問題などがある [5] [6] [10] [12]．

ング，有界モデル検査，システム生物学など様々な分組合せ遷移問題の研究は，理論計算機科学の分野を

野への実用的応用が急速に拡大している [7].

中心に，最近 10 年で急速に発展し，理論的な基盤が組合せ遷移問題に対して ASP を用いる利点とし整備されつつある．また，実社会においても，配電網ては，ASP 言語の高い表現力により，記号制約を簡潔に記述できる点，インクリメンタル ASP 解法によA Study on ASP-based Implementation of Combinatorial Reconﬁguration Solver
Yuya Yamada, Mutsunori Banbara, 名古屋大学 大学
院 情 報 学 研 究 科, Graduate School of Informatics,
Nagoya University.
Shin-ichi Minato, 京都大学 大学院情報学研究科, Graduate School of Informatics, Kyoto University.

り，学習節を再利用した効率的な解探索が可能である
点，探索ヒューリスティックスを簡単にカスタマイズできる点，などが挙げられる．
本稿では，解集合プログラミング (ASP) を用いた組合せ遷移問題の解法として，有界組合せ遷移を提案

し，そのソルバーの実装方法について述べる．有界組
合せ遷移は，SAT 技術を用いたモデル検査手法の 1

1

2

1

2

3

4

3

4

つである有界モデル検査 [1] [3] [4] を組合せ遷移に応用した解法といえる．
有界組合せ遷移は，組合せ遷移問題に対して，制限された長さの (すなわち有界の) 遷移系列を論理プログラムとして記号的に表現し，その論理プログラム

図1

色数 k = 3 のグラフ点彩色問題の入力例 (左) と実を ASP システムで実行することにより，到達可能性

行可能解 (右)の検査を行う．ASP システムが充足可能と判定した
場合，制限された長さの到達可能な遷移系列が存在

グラフ点彩色問題を基とする組合せ遷移問題は，することを意味する．逆に充足不能と判定した場合，

k 彩色遷移問題 (k-coloring Reconﬁguration Prob-

制限された長さでは到達不能であることを意味する.

lems) ともよばれ盛んに研究されている [5] [6]．k 彩

この場合，遷移系列の長さを増加させた論理プログラ

色遷移問題は，色数 k のグラフ点彩色問題と 2 つのムを構成し，再び ASP システムによる実行を繰り返

実行可能解が与えられたとき，一方の実行可能解からす．有界組合せ遷移は，到達可能な遷移系列を探すだ

他方の実行可能解へ，1 回の遷移において色が変化す

けで，到達不能の証明は行わない不完全な手続きである頂点はただ 1 つのみという遷移制約を満たしつつ，るが，検査すべき遷移系列の長さに上限が存在する場

実行可能解のみを経由して到達できるかを判定する

合には完全な手続きとなる．

問題である．k 彩色遷移問題では，グラフの形や色数有界組合せ遷移の有効性を評価するために，代表に制限を加えることで多項式時間で解ける問題が存的な組合せ遷移問題の 1 つである k 彩色遷移問題を在するが，一般に k ≥ 4 において PSPACE 完全で

ベンチマークとして，提案ソルバーの性能評価を行っあることが知られている．

た．その結果，インクリメンタル ASP 解法を用いた

図 1 に，色数 k = 3 のグラフ点彩色問題の例とその実装方法がより多くの問題を高速に解くことができ

実行可能解を示す．図 2 は，到達可能な k = 4 彩色遷ることを確認した．

移問題の例である．この例は，スタート状態 (t = 0)
からゴール状態 (t = 3) へ，3 ステップの遷移で到達

2 組合せ遷移問題と k 彩色遷移問題

している．また，各状態 t はグラフ点彩色問題の制約組合せ遷移問題 (Combinatorial Reconﬁguration

を満たしており，1 回の遷移においてちょうど 1 個のProblems; CoRe [12] [14] [16]) は，基となる組合せ問

頂点の色が変化していることがわかる．

題の実行可能解が形成する解空間グラフを用いて定義される．解空間グラフの頂点は実行可能解を表し，3 解集合プログラミング

辺は遷移制約に関する実行可能解の間の隣接関係を解集合プログラミング (Answer Set Programming;

表す．つまり，組合せ問題が実行可能解が存在するか

ASP [2] [9] [11] [13]) は，演繹データベース，否定を含を判定するのに対し，組合せ遷移問題は，解空間グラ

む論理プログラミング，非単調推論，制約充足 (特に，

フにおいて 2 つの頂点間の到達可能性を判定するこSAT) を起源にもつ，宣言的プログラミングパラダイとが目的となる．

ムである．ASP の言語は，一般拡張選言プログラム

基となる組合せ問題の例として，色数 k のグラフに基づいている．本稿では説明の簡略化のため，その点彩色問題を考える．この問題は，与えられた有限無サブクラスである標準論理プログラムについて説明

向グラフについて，隣接する頂点が同色にならないよする．以降，標準論理プログラムを単に論理プログラ

うに各頂点を彩色するとき，グラフが k 色以下で彩ムとよぶ．

色可能かどうかを判定する問題である．

論理プログラムは，以下の形式をしたルールの有限

t=0
1

t=1
2

1

t=2
2

⇒

3

4

1

t=3
2

⇒

3

4

1

2

3

4

⇒

3

4

スタート状態

ゴール状態
図2

到達可能な k = 4 彩色遷移問題の例

集合である．

表1

論理プログラムとソースコードの対応

a0 ← a1 , . . . , am , ∼am+1 , . . . , ∼an

論理プログラム

←

,

;

∼

ここで，0 ≤ m ≤ n であり，各 ai はアトム，∼ はデ
フォルトの否定 †1 ，“,” は連言を表す．← の左側を

ソースコード

:-

,

;

not

ヘッド，右側をボディとよぶ．ルールの直観的な意味

グラムに基礎化したのち，基礎ソルバーを用いて解は，「a1 , . . . , am がすべて成り立ち，am+1 , . . . , an のそれぞれが成り立たないならば，a0 が成り立つ」で集合を計算する．本稿で使用する高速 ASP システム
clingo †2 は，基礎化のためのグラウンダー gringo とある．ボディが空のルール (すなわち a0 ←) をファク

基礎ソルバー clasp をシームレスに結合したものであトとよび，← を省略してよい．

る．以降で示す論理プログラムのソースコードはすべ

ヘッドが空のルールを一貫性制約とよぶ．

← a1 , . . . , am , ∼am+1 , . . . , ∼anて clingo 言語で書かれており，表記上の対応については表 1 の通りである．

直観的には，← a1 は，a1 ではないという禁止を表ASP を用いた基本的な問題解法は，最初に解きたし，← ∼a1 は，a1 でなければならないという強制をい問題を論理プログラムとして表現 (ASP 符号化) す表す．また，← a1 , ∼a2 は，a1 が成り立つならば，a2る．つぎに ASP システムを用いて論理プログラムのが成り立つことを意味する．

解集合を計算する．最後に解集合を解釈してもとの問

ASP 言語は，組合せ問題を解くための便利な拡張

題の解を得る，という 3 つのステップからなる．以構文を備えている．その代表的なものが選択子と個数

下，グラフ点彩色問題を例にとって，各ステップごと制約である．例えば，選択子 {a1 ; . . . ; an } をファクに説明する．

トとして書くと，アトム集合 {a1 , . . . , an } の任意のコード 1 に，図 1 のグラフを ASP のファクト形

部分集合が成り立つことを意味する．個数制約は選式で表したもの示す．アトム n/1 は頂点数，e/1 は辺

択子の両端に選択可能な個数の上下限を付けたもの

数，node/1 は頂点，edge/2 は辺を表している．ピリである．例えば，lb {a1 ; . . . ; an } ub ← Body と書く

オド (“.”) はルールの終わりを表す終端記号である．

と，Body が成り立つならば，a1 , . . . , an のうち，lb
個以上 ub 個以下が成り立つことを意味する．

グラフ点彩色問題を解く論理プログラムを，コード 2 に示す．コード中の c は色数を表す定数であり，ASP システムは，与えられた論理プログラムか

実際の値は実行時に clingo のオプションとして与えらら，安定モデル意味論 [9] に基づく解集合を計算す

れる．1 行目のアトム col/1 は色を表し，col(1..c).

るソフトウェアである．ASP システムの多くは，変は col(1)., col(2)., . . . , col(c). と書くことに等数を含む論理プログラムを変数を含まない論理プロ

しい．2 行目のルールは，頂点 X が色 C で塗られることを意味するアトム color(X,C) を導入し，個数制約†1 “失敗による否定” ともよばれる．述語論理で定義される否定 (¬) とは意味が異なる．

†2 https://potassco.org/

n(4).
node(1).

1 node(1).

e(4).
node(2).

node(3).

node(4).

edge(1,2). edge(2,3). edge(2,4). edge(3,4).

node(2).

node(3).

node(4).

2 edge(1,2). edge(2,3). edge(2,4). edge(3,4).
3 col(1).

col(2).

col(3).

4 1 { color(1,1) ; color(1,2) ; color(1,3) } 1.

コード 1

図 1 のグラフの ASP ファクト表現(graph.lp)

5 1 { color(2,1) ; color(2,2) ; color(2,3) } 1.
6 1 { color(3,1) ; color(3,2) ; color(3,3) } 1.
7 1 { color(4,1) ; color(4,2) ; color(4,3) } 1.
8 :- not {color(1,1) ; color(2,1) } 1.
9 :- not {color(1,2) ; color(2,2) } 1.
10 :- not {color(1,3) ; color(2,3) } 1.

1 col(1..c).

11 :- not {color(2,1) ; color(3,1) } 1.

2 1 { color(X,C): col(C) } 1 :- node(X).

12 :- not {color(2,2) ; color(3,2) } 1.

3 :- not { color(X,C); color(Y,C) } 1, edge(X,Y), col(C).

13 :- not {color(2,3) ; color(3,3) } 1.
14 :- not {color(2,1) ; color(4,1) } 1.

コード 2

色数 c のグラフ点彩色問題を解く論理プログラ

15 :- not {color(2,2) ; color(4,2) } 1.
16 :- not {color(2,3) ; color(4,3) } 1.

ム (color.lp)

17 :- not {color(3,1) ; color(4,1) } 1.
18 :- not {color(3,2) ; color(4,2) } 1.
19 :- not {color(3,3) ; color(4,3) } 1.

% clingo -c c=3 graph.lp color.lp

コード 4clingo version 5.4.0

基礎化された論理プログラム

Reading from graph.lp ...
Solving...
Answer: 1

をコード 4 に示す．4–7 行目がコード 2 の 2 行目に，color(1,1) color(2,3) color(3,1) color(4,2)...

8–19 行目がコード 2 の 3 行目に対応している．

SATISFIABLE

Models

: 1+

Calls

: 1

CPU Time: 0.002s

4 ASP を用いた組合せ遷移問題の解法
ASP 技術を用いた組合せ遷移問題の解法として，
有界組合せ遷移 (Bounded Combinatorial Reconﬁg-

コード 3clingo の実行例

uration) を提案し，そのソルバーの実装方法について述べる．

を用いて「各頂点は 1 つの色で塗られる」という制約を表している．3 行目のルールは，一貫性制約と個

4. 1 有界組合せ遷移

数制約を使って「辺で結ばれた頂点 X と Y が同じ色 C

有界組合せ遷移では，組合せ遷移問題に対して，制で塗られることはない」という制約を表している．

限された長さの遷移系列を論理プログラムとして記

ASP システムは，コード 1 のファクトとコード 2号的に表現し，その論理プログラムを ASP システの論理プログラムから解集合を計算する．コード 3

ムで実行することにより，到達可能性の検査を行う．

に clingo の 実 行 例 を 示 す．色 1 を 赤 ，色 2 を 青 ，

ASP システムが充足可能と判定した場合，制限され色 3 を黄とすると，得られた解集合 { color(1,1),た長さの到達可能な遷移系列が存在することを意味

color(2,3), color(3,1), color(4,2)} は，図 1 のする．逆に充足不能と判定した場合，制限された長さ右側の彩色を表す．

では到達不能であることを意味する．この場合，遷論理プログラムの基礎化について，もう少し詳しく

移系列の長さを増加させた論理プログラムを構成し，説明する．clingo は，グラウンダー gringo を用いて再び ASP システムによる実行を繰り返す．有界組合

コード 1 のファクトとコード 2 の論理プログラムをせ遷移は，到達可能な遷移系列を探すだけで，到達不基礎化した後，clasp を用いて基礎化された論理プロ

能の証明は行わない不完全な手続きであるが，検査すグラムの解集合を計算する．基礎化されたルール集合

べき遷移系列の長さに上限が存在する場合には，完全な手続きとなる．例えば，基の組合せ問題の直径 (任意の 2 つの実行可能解の最短経路のうちの最大長) を上限とすればよい †3 ．
組合せ遷移問題が与えられたとき，基の組合せ問

1 n(4).

e(4).

2 node(1).

node(2).

node(3).

node(4).

3 edge(1,2).

edge(2,3).

edge(2,4).

edge(3,4).

4 start(1,4). start(2,2). start(3,3). start(4,1).
5 goal(1,3).

goal(2,4).

goal(3,2).

goal(4,1).

題の変数集合 x = {x1 , x2 , . . . , xn }，各遷移ステップt ≥ 0 に対して，ステップ t での各変数の値を表す変数

コード 5

集合 xt = {xt1 , xt2 , . . . , xtn } を導入する．ここで，スk = 4 彩色遷移問題のファクト表現(graph_reconfig.lp)

タート状態の制約を表す論理式を S(x)，基の組合せ問
題の制約を表す論理式を C(x)，遷移制約を表す論理式′

不能の証明は行えない不完全な手続きであるが，検査を T (x, x )，ゴール状態の制約を表す論理式を G(x)

すべきステップ長 ℓ に上限が存在する場合には完全とする．スタート状態から ℓ ステップ遷移した後の各変∧∧数の値 xℓ は，S(x0 )∧ ℓt=0 C(xt )∧ ℓt=1 T (xt−1 , xt )な手続きとなり，到達不能も判定できる．この手続きを満たす．そこで，ゴール状態の制約を満たすかどうことにする．

か判定するため，G(xℓ ) を付け加えた論理式 φℓ を構成する．

を，単純に実装したプログラムを基本ソルバーとよぶ

k 彩色遷移問題を例にとって，基本ソルバーを用いた問題解法を説明する．図 2 の k = 4 彩色遷移問題のASP ファクト表現をコード 5 に示す．コード 1 のグ
φℓ = S(x0 )
ℓ
ℓ
∧
∧
∧
C(xt ) ∧T (xt−1 , xt )
t=0

t=1

∧ G(xℓ )ラフ点彩色問題のファクト表現と比較して，スタート状態を表す start/2 とゴール状態を表す goal/2 が追加されている．ここで，色 1 は赤，色 2 は青，色

3 は黄，色 4 は緑とする．例えば，start(1,4). は，与えられたステップ長 ℓ に対し φℓ が充足可能であれスタート状態 (t = 0) において頂点 1 が色 4 (緑) でば，到達可能な遷移系列が得られる．

塗られることを表す．
コード 6 に，k=c 彩色遷移問題を解く論理プログラ

4. 2 有界組合せ遷移の基本ソルバー

ムとして changed 符号化を示す．コード中の c は色

ASP システムを用いて有界組合せ遷移を行う手続

数，length はステップ長を表す．1 行目のアトム t/1

きは以下のようになる．

はステップ数を表す．アトム color(X,C,T) は，ス

1. ステップ長 ℓ を ℓ = 0 とする．

テップ T において，頂点 X が色 C で塗られることを意

2. φℓ を論理プログラムとして記述し，ファクト形

味する．3 行目はスタート状態の制約を表す．5–7 行

式の CoRe 問題インスタンスとともに，ASP シ

目は基のグラフ点彩色問題の制約を表す．9–11 行目はステムに入力として与える．

遷移制約を表す．9 行目の補助アトム changed(X,T)

3. ASP システムの出力結果が充足可能であればは，ステップ T-1 と T の間で頂点 X の色が変化した

終了する．充足不能であれば ℓ の値を 1 増加さことを意味する．11 行目のルールは，個数制約を用せ，2 に戻り手続きを繰り返す．ただし，ℓ が基いて「各ステップ T において色が変化する頂点はたの問題の直径を超えたところで繰り返しを停止

だ 1 つのみ」という制約を表している．

できる．

コ ー ド 7 に ，遷 移 制 約 の 表 現 方 法 が 異 な る

この手続きは，与えられた組合せ遷移問題に対して，

unchanged 符号化を示す．changed 符号化との違い

到達可能な最短の遷移系列を探索する．一般に，到達は，9–10 行目のルールだけである．9 行目の補助ア†3 理論的には，問題の直径を超えるまで手続きを繰り返せばよいが，実用的な問題ではしばしば直径が大きす
ぎ，現実的には適用できない場合もある．

トム unchanged(X,T) は，ステップ T-1 と T の間で
頂点 X の色が変化しないことを意味する．10 行目のルールは，個数制約を用いて「各ステップ T において

1 col(1..c).

t(0..length).

% clingo graph_reconfig.lp changed.lp -c c=4 -c length=0

2 % startclingo version 5.4.0

3 :- not color(X,C,0), start(X,C).

Reading from graph_reconfig.lp ...

4 % constraints

Solving...

5 1 { color(X,C,T): col(C) } 1 :- node(X), t(T).

UNSATISFIABLE

6 :- not { color(X,C,T); color(Y,C,T) } 1,7edge(X,Y), col(C), t(T).

Models: 0

8 % transition

Calls

: 1

9 changed(X,T) :- color(X,C1,T), color(X,C2,T-1),

CPU Time: 0.003s

10

C1 != C2, T >= 1.

11 :- not 1{ changed(X,T) } 1, t(T), T >= 1.

% clingo graph_reconfig.lp changed.lp -c c=4 -c length=1

12 % goalclingo version 5.4.0

13 :- not color(X,C,length), goal(X,C).

Reading from graph_reconfig.lp ...
Solving...

コード 6

k =c 彩色遷移問題を解く changed符号化(changed.lp)．定数 length はステップ長を表す．

1 col(1..c).

Models

: 0

Calls

: 1

CPU Time: 0.003st(0..length).
% clingo graph_reconfig.lp changed.lp -c c=4 -c length=2

2 % start
3 :- not color(X,C,0), start(X,C).
4 % constraints
5 1 { color(X,C,T): col(C) } 1 :- node(X), t(T).
6 :- not { color(X,C,T); color(Y,C,T) } 1,
7

UNSATISFIABLE

clingo version 5.4.0
Reading from graph_reconfig.lp ...
Solving...
UNSATISFIABLE

edge(X, Y), col(C), t(T).
Models

8 % transition
9 unchanged(X,T) :- color(X,C,T), color(X,C,T-1), T >= 1.
10 :- not N-1 { unchanged(X,T) } N-1 , n(N), t(T), T >= 1.

: 0

Calls

: 1

CPU Time: 0.005s

11 % goal
12 :- not color(X,C,length), goal(X,C).

% clingo graph_reconfig.lp changed.lp -c c=4 -c length=3
clingo version 5.4.0
Reading from graph_reconfig.lp ...

コード 7

k =c 彩色遷移問題を解く unchanged符号化

Solving...

(unchanged.lp)．定数 length はステップ長を表す．

Answer: 1
color(1,4,0) color(2,2,0) color(3,3,0) color(4,1,0)
color(1,3,1) color(2,2,1) color(3,3,1) color(4,1,1)

色が変化しない頂点は N-1 個」という制約を表してcolor(1,3,2) color(2,4,2) color(3,3,2) color(4,1,2)いる．この unchanged 符号化の特徴は，changed 符

color(1,3,3) color(2,4,3) color(3,2,3) color(4,1,3)...
SATISFIABLE

号化と比較して，基礎化後のルール数が少なく抑えられる点である．
基本ソルバーは，CoRe 問題インスタンスのファク

Models

: 1+

Calls

: 1

CPU Time: 0.005s

ト表現と，CoRe 問題を解く符号化を入力として，到達可能性を検査する．コード 8 に，k 彩色遷移問題

コード 8clingo の実行例

に対する基本ソルバーの動作を示す．この例より，ステップ長 length を 0 から 3 まで変化させ，clingo を

4. 3 ソルバーの改良

合計 4 回実行することにより，最短の遷移系列が得

有界組合せ遷移は，ステップ長 ℓ を増やしながら，られることがわかる．length=3 で得られた解集合は，複数の φℓ を繰り返し解く必要がある．しかし，各 φℓ

図 2 に示した遷移系列に対応している．

に含まれる制約の大部分は同じであるため，実際に提案ソルバー
組合せ遷移問題のインスタンス-- ASP ファクト - ASP システム - 組合せ遷移問題
の解

変換器

6
論理プログラム

図3

インクリメンタル ASP 解法を用いた改良ソルバーの構成図

φℓ−1 と φℓ の差をみてみると，
φℓ−1 ⊕ φℓ = {C(x ), T (xℓ?

core.lpℓ−1

9. ASP システムの出力結果が充足可能であれば終
ℓ

ℓ−1

ℓ

), G(x )}了する．充足不能であれば ℓ の値を増加させ，4であり，多くの制約は共通していることがわかる．そに戻り手続きを繰り返す．ただし，ℓ が基の問題のため，各 φℓ に対して毎回 ASP システムを実行すの直径を超えたところで繰り返しを停止できる．

, x ), G(xる基本ソルバーは，同一の探索空間を何度も調べるこ

10. ASP システムを終了する．

とになり求解効率が低下する．また，毎回 φℓ 全体を到達不能の証明については，4. 2 節で述べた基本ソル基礎化するオーバーヘッドも無視できない．

バーの手続きと同じである．

この問題を解決するために，有界モデル検査やプラ図 4 に，clingo の Python インターフェースを用いンニングの実装で使われるインクリメンタル ASP 解て上記の手続きを実装した改良ソルバーを示す．変数法を用いる [8]．この解法は，ルールを追加・削除しcore_max はステップ長 ℓ の上限値を表す．core_stop

た一連の論理プログラムを，同様の探索失敗を防ぐたはプログラムの停止条件を表す変数であり，基本的にめに獲得した学習節を再利用しながら，連続的に解くは SAT を指定する．11 行目で定義されている step

ための手法である．

は ℓ に対応する．16–18 行目は手続き 4 に対応してインクリメンタル ASP 解法を用いた改良ソルバー

いる．19–20 行目は手続き 5 に対応している．21 行

は，ステップ長 ℓ を増やしながら，段階的に φℓ を構

目は手続き 6 に対応している．22 行目は手続き 7 に成し，獲得した学習節を再利用した効率のよい到達可

対応している．23 行目でステップ数 ℓ で追加される能性の検査を可能とする．改良ソルバーの構成を図 3ルールの基礎化を行い，25 行目の prg.solve() で到に示す．

達可能性を検査している．

改良ソルバーにおける有界組合せ遷移を行う手続
き (図 3 の core.lp) は以下のようになる．

改良ソルバーの入力となる論理プログラムは，base,step(t), check(t) の 3 つのパートから構成される．

1. ASP システムを起動する．

base パートには，スタート状態の制約 S を記述す2. ファクト形式の CoRe 問題インスタンスと，Sる．step(t) パートには，各ステップ 0 ≤ t ≤ ℓ にを表すサブプログラム，C と T を表すサブプロ

おいて満たすべき基の組合せ問題の制約 C および遷グラム，G を表すサブプログラムから構成され

移制約 T を記述する．check(t) パートには，ゴールる論理プログラムを与える．

状態の制約 G を記述する．コード 9 とコード 10 に，

3. ステップ長 ℓ を ℓ = 0 とする．

k=c 彩色遷移問題を解く 2 種類の論理プログラムを

4. ℓ > 0 であれば，G(xℓ−1) を表すルールを削除

0

5. ℓ = 0 であれば，S(x ) を表すルールを追加
6. C(x ) と T (xをコード 11 に示す．得られた解集合は，図 2 の遷移系列に対応している．

する．
ℓ

示す．これらは，それぞれコード 6 とコード 7 の論理プログラムに対応している．改良ソルバーの実行例

する．

ℓ−1

ℓ

, x ) を表すルールを追加する．

ℓ

7. G(x ) を表すルールを追加する．
8. ASP システムを用いて到達可能性を検査する．

1 #script (python)
2 import clingo
3
4 def get(val, default):
5
return val if val != None else default
6
7 def main(prg):
8
core_stop = get(prg.get_const("core_stop"), clingo.String("SAT"))9core_max= prg.get_const("core_max")
10
11
step, ret = 0, None
12
while ((core_max is None or step <= core_max.number) and13(step == 0 or (core_stop.string == "SAT" and not ret.satisfiable) or
14(core_stop.string == "UNSAT" and not ret.unsatisfiable))):15
parts = []16
if step > 0:
17
prg.release_external(clingo.Function("query", [step-1]))18
prg.cleanup()
19
else:
20
parts.append(("base", []))
21
parts.append(("step", [step]))
22
parts.append(("check", [step]))
23
prg.ground(parts)
prg.assign_external(clingo.Function("query", [step]), True)
24
25
ret, step = prg.solve(), step+1
26
27
print(’c step: %s’ % str(step-1))
28
if (step != 0 and29(core_stop.string != "SAT" or ret.satisfiable) and30(core_stop.string != "UNSAT" or ret.unsatisfiable)):31
print(’s REACHABLE’)
32
else:
33
print(’s UNREACHABLE’)
34
35 #end.
36 #program check(t).
37 #external query(t).

図4clingo の Python API を用いた改良ソルバーの実装 (core.lp)

127 個のうち，彩色数が判明している 44 個 [15]5 実行実験

をベンチマーク問題の候補とした．

提案した有界組合せ遷移の有効性を評価するため• 44 個のグラフに対して，彩色数での実行可能解に，k 彩色遷移問題をベンチマークとして開発したソの総数を計算できるか調査した．総数が得られた

ルバーの性能評価を行った．ベンチマーク問題には，

9 個のグラフを表 2 に示す．

独自に作成した k 彩色遷移問題 (90 問) を使用した．
作成方法は以下の通りである．

• Graph Coloring and its Generalization †4 で公開されているグラフ点彩色問題のインスタンス• 総数が得られた 9 個のグラフについて，実行可能解をランダムに 2 つ選びベンチマーク問題を各 10 問ずつ作成した (計 90 問)．

k 彩色遷移問題を解く論理プログラムには，changed
符号化，unchanged 符号化，changed_inc 符号化，

†4 https://mat.tepper.cmu.edu/COLOR04/

unchanged_inc 符号化の 4 つを使用した．ステップ

% clingo graph_reconfig.lp changed_inc.lp core.lp -c c=4

1 #program base.

clingo version 5.4.0

2 col(1..c).
3 color(X,C,0) :- start(X,C).

Reading from graph_reconfig.lp ...
Solving...

4

Solving...

5 #program step(t).
6 1 { color(X,C,t): col(C) } 1 :- node(X).
7 :- not { color(X,C,t); color(Y,C,t) } 1, edge(X,Y), col(C).

Solving...
Solving...
Answer: 1

8
9 changed(X,t) :- color(X,C1,t), color(X,C2,t-1),
10

C1 != C2, t >= 1.

11 :- not 1 { changed(X,t) } 1, t >= 1.

color(1,4,0) color(2,2,0) color(3,3,0) color(4,1,0)
color(1,3,1) color(2,2,1) color(3,3,1) color(4,1,1)
color(1,3,2) color(2,4,2) color(3,3,2) color(4,1,2)
color(1,3,3) color(2,4,3) color(3,2,3) color(4,1,3)...

12

SATISFIABLE

13 #program check(t).
14 :- not color(X,C,t), goal(X,C), query(t).

c step: 3
s REACHABLE

コード 9

k=c 彩色遷移問題を解く changed_inc 符号化(changed_inc.lp)

Models

: 1+

Calls

: 4

CPU Time: 0.029s

コード 11

提案ソルバーの実行例

1 #program base.
2 col(1..c).
3 :- not color(X, C, 0), start(X, C).

表2

独自に生成した k 彩色遷移問題のベンチマーク問題

4
5 #program step(t).

グラフ名

6 1 { color(X,C,t): col(C) } 1 :- node(X).
7 :- not { color(X,C,t); color(Y,C,t) } 1, edge(X,Y), col(C).
89 unchanged(X,t) :- color(X,C,t), color(X,C,t-1), t >= 1.
10 :- not N-1 { unchanged(X,t) } N-1 , n(N), t >= 1.
1112 #program check(t).
13 :- not color(X,C,t), goal(X,C), query(t).

コード 101-FullIns_3
le450_5ale450_5cle450_5d
myciel3
myciel4queen5_5
queen6_6
queen7_7

頂点数

辺数

彩色数

30
450
450
450
11
23
25
36
49

100
5,714
9,803
9,757
20
71
160
290
476

4
5
5
5
4
5
5
7
7

解の総数
50,693,280
3,840
120
960
12,4802,845,658,400
240
100,800
20,160k=c 彩色遷移問題を解く unchanged_inc 符
号化 (unchanged_inc.lp)

が 21 問，unchanged 符号化が 21 問，changed_inc
符号化が 67 問，unchanged_inc 符号化が 71 問であ長の上限値には，解の総数から 1 ひいた値を使用した †5 ．ASP システムには，clingo のバージョン 5.4.0

る．unchanged_inc が最も多くの問題を解き，平均(jumpy) を使用した．計算環境は Mac OS 3.2GHz 6

す．図 5 の縦軸は CPU 時間，横軸は解けた問題数をCPU 時間も最も短い．図 5 にカクタスプロットを示

コア Intel Core i7，64GB メモリである．1 問あたり表す．図より，unchanged_inc 符号化が，他の符号の制限時間は 1 時間とした．

化と比較して，より多くの問題をより高速に解いてい表 3 に実験結果を示す．左から順に問題名，到達可ることが確認できる．以上のことから，インクリメン

能/到達不能の別，ステップ長，各符号化の CPU 時

タル ASP 解法を用いた改良ソルバーの優位性が確認間を表している．解けた問題の数は，changed 符号化できた．

†5 ただし，グラフ myciel4 から作成した問題について
は，clingo が対応している数よりも解の総数が大きかったため，ステップ長の上限値を 231 − 1 とした．

表3

実験結果: CPU 時間

問題名

到達可能/到達不能

ステップ長

1-FullIns 3 col4 1
le450 5a col5 1
le450 5a col5 2
le450 5a col5 3
le450 5a col5 4le450 5a col5 5le450 5a col5 6le450 5a col5 7le450 5a col5 8le450 5a col5 9le450 5a col5 10le450 5c col5 1
le450 5c col5 2
le450 5c col5 3
le450 5c col5 4le450 5c col5 5le450 5c col5 6le450 5c col5 7le450 5c col5 8le450 5c col5 9le450 5c col5 10le450 5d col5 1
le450 5d col5 2
le450 5d col5 3
le450 5d col5 4le450 5d col5 5le450 5d col5 6le450 5d col5 7le450 5d col5 8le450 5d col5 9le450 5d col5 10
myciel3 col4 1
myciel3 col4 3
myciel3 col4 4myciel3 col4 7
myciel3 col4 8
myciel4 col5 2
myciel4 col5 3
myciel4 col5 4
myciel4 col5 6
myciel4 col5 10queen5 5 col5 1queen5 5 col5 2queen5 5 col5 3queen5 5 col5 4queen5 5 col5 5queen5 5 col5 6queen5 5 col5 7queen5 5 col5 8queen5 5 col5 9queen5 5 col5 10queen6 6 col7 1
queen6 6 col7 2queen6 6 col7 3queen6 6 col7 4queen6 6 col7 5queen6 6 col7 6queen6 6 col7 7queen6 6 col7 8queen6 6 col7 9queen6 6 col7 10queen7 7 col7 1
queen7 7 col7 2queen7 7 col7 3queen7 7 col7 4queen7 7 col7 5queen7 7 col7 6queen7 7 col7 7queen7 7 col7 8queen7 7 col7 9queen7 7 col7 10

REACHABLE
11
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
3,839
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
119
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
UNREACHABLE
959
REACHABLE
11
REACHABLE
11
REACHABLE
13
REACHABLE
8REACHABLE
9REACHABLE
16
REACHABLE
14
REACHABLE
7REACHABLE
10REACHABLE
17
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
239
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
100,799
UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159UNREACHABLE
20,159平均 CPU 時間
解けた問題数changedunchanged
基本ソルバー
1.374
1.071
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
0.179
0.148
0.206
0.164
0.486
0.445
0.090
0.072
0.119
0.094
42.48248.72117.09821.211
0.256
0.193
1.525
1.391
212.682
73.646439.863302.994
437.481301.194441.161
303.136443.299304.547441.616302.366446.811301.201
441.071303.449442.539303.821443.353302.952
446.027305.350
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
TO
223.796151.341
21
21

changed_inc
unchanged_inc
改良ソルバー
1.291
0.756
3.761
2.991
2.943
11.6734.662
22.048TO
7.776
TO26.7233.618
3.220
1318.024
8.698
3.367
18.226
2.943
2.847
2.968
3.196
2.189
2.165
150.018
2.148
150.2832.701
152.434
2.102
2.209
2.114
2.219
2.141
151.252
2.150
2.878
2.176
2.827
2.146
2.246
2.166
2.680
5.653
4.097
2.621
3.421
2.600
155.850
6.960
3.294
2.618
199.336
25.2733.308
12.001
2.695
15.2243.351
13.121333.183
7.974
0.065
0.065
0.082
0.080
0.303
0.583
0.042
0.036
0.048
0.044
20.308134.0565.286
80.848
0.086
0.072
1.052
1.558
29.999200.068
0.073
0.082
0.074
0.057
0.073
0.589
0.061
0.057
0.074
0.067
0.061
0.149
0.074
0.056
0.073
0.137
0.074
0.066
0.073
0.058
5.375
5.488
5.337
5.292
5.345
4.390
5.714
4.358
4.274
5.178
5.403
5.129
5.219
4.418
4.300
4.389
5.365
5.407
TO
4.412
2804.714
949.947
1.342
907.100
1.586
1.499
TO
2.768
1.622
6.052
1.803
1626.628
1.343
1.590
1.481
3.652
1224.680
3.760
1.557
1.349
101.758
59.09567
71

組合せ遷移の有効性を評価するために，代表的な組

6 おわりに合せ遷移問題の 1 つである k 彩色遷移問題をベンチ

本稿では，解集合プログラミング (ASP) を用いたマークとして，提案ソルバーの性能評価を行った．そ組合せ遷移問題の解法として，有界組合せ遷移を提の結果，インクリメンタル ASP 解法を用いた改良ソ案し，そのソルバーの実装方法について述べた．有界

ルバーがより多くの問題を高速に解くことができる

3000
changedchanged_inc
unchanged
unchanged_inc
2500

CPU Time (sec)

2000

1500

1000

500

0
0

10

20

30

40

50

60

70

80

Solved Instances

図5

カクタスプロットことを確認した．
組合せ遷移問題を解く汎用ソルバーの研究開発はまだ始まったばかりである．今後の課題として，改良
ソルバーの高速化があげられる．高速化の手法として
は，アルゴリズムの刷新や探索ヒューリスティックスの改良を考えている．集合被覆問題や独立点集合を基とする組合せ遷移問題，15 パズルなどの問題記述例の蓄積も重要な課題の一つである．また，k 彩色遷移問題の ASP 符号化の改良も考えている．
参 考 文 献[ 1 ] 番原睦則, 田村直之: SAT によるシステム検証, 人
工知能学会誌, Vol. 25, No. 1(2010), pp. 122–129.
[ 2 ] Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving, Cambridge
University Press, 2003.
[ 3 ] Biere, A.: Bounded Model Checking, Handbookof Satisﬁability, IOS Press, 2009, pp. 457–481.
[ 4 ] Biere, A., Cimatti, A., Clarke, E. M., and Zhu,
Y.: Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on
Tools and Algorithms for Construction and Analysis of Systems (TACAS 1999), LNCS 1579, 1999,
pp. 193–207.
[ 5 ] Bonsma, P. S. and Cereceda, L.: Finding Paths
between graph colourings: PSPACE-completenessand superpolynomial distances, Theoretical Com-

puter Science, Vol. 410, No. 50(2009), pp. 5215–
5226.
[ 6 ] Cereceda, L., van den Heuvel, J., and Johnson,
M.: Finding paths between 3-colorings, Journal ofGraph Theory, Vol. 67, No. 1(2011), pp. 69–82.
[ 7 ] Erdem, E., Gelfond, M., and Leone, N.: Applications of ASP, AI Magazine, Vol. 37, No. 3(2016),
pp. 53–68.
[ 8 ] Gebser, M., Kaminski, R., Kaufmann, B., andSchaub, T.: Multi-shot ASP solving with clingo,
Theory and Practice of Logic Programming, Vol. 19,
No. 1(2019), pp. 27–82.
[ 9 ] Gelfond, M. and Lifschitz, V.: The Stable Model
Semantics for Logic Programming, Proceedings ofthe Fifth International Conference and Symposiumon Logic Programming, MIT Press, 1988, pp. 1070–
1080.
[10] Gopalan, P., Kolaitis, P. G., Maneva, E. N., andPapadimitriou, C. H.: The Connectivity of Boolean
Satisﬁability: Computational and Structural Dichotomies, SIAM Journal on Computing, Vol. 38,
No. 6(2009), pp. 2330–2355.
[11] 井上克巳, 坂間千秋: 論理プログラミングから解集合
プログラミングへ, コンピュータソフトウェア, Vol. 25,
No. 3(2008), pp. 20–32.
[12] Ito, T., Demaine, E. D., Harvey, N. J. A., Papadimitriou, C. H., Sideri, M., Uehara, R., and Uno,Y.: On the complexity of reconﬁguration problems,
Theoretical Computer Science, Vol. 412, No. 1214(2011), pp. 1054–1065.
[13] Niemelä, I.:
Logic Programs with Stable
Model Semantics as a Constraint Programming
Paradigm, Ann. Mathematics and Artiﬁcial Intel-

ligence, Vol. 25, No. 3–4(1999), pp. 241–273.
[14] Nishimura, N.: Introduction to Reconﬁguration,
Algorithms, Vol. 11, No. 4(2018), pp. 52.
[15] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.

[16] van den Heuvel, J.: The complexity of change,
Surveys in Combinatorics 2013, Blackburn, S. R.,
Gerke, S., and Wildon, M.(eds.), London Mathematical Society Lecture Note Series, Vol. 409, Cambridge University Press, 2013, pp. 127–160.