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

解集合プログラミングに基づく組合せ遷移ソルバーとその性能評価
山田 悠也

番原 睦則

本稿では，組合せ遷移問題を解く汎用ソルバーの設計と実装について述べる．組合せ遷移問題とは，基となる組合
せ問題とその二つの実行可能解が与えられたとき，一方から他方へ隣接関係を満たしつつ，実行可能解のみを経由して到達可能かどうかを判定する問題である．解集合プログラミング (ASP) に基づく組合せ遷移ソルバー recongo
は，組合せ遷移問題のインスタンスと組合せ遷移問題を解くための ASP 符号化 (論理プログラム) を入力として，
高速 ASP システム clingo を用いて組合せ遷移問題の解を求めるシステムである．recongo は組合せ遷移問題の到達性判定に加え，最短経路長，最長経路長，遷移最適化など他のバリエーションにも対応している．提案ソルバー
recongo の性能評価として，国際競技会 CoRe Challenge 2022 の結果と考察を示す．なお，recongo は同競技会のSolver Track 全 6 部門のうち，Single-engine Solvers shortest 部門で優勝，その他 4 部門でも入賞している．

可能であればその遷移系列を解として出力する．組合

1 はじめにせ遷移ソルバーの研究開発はまだ始まったばかりであ組合せ遷移問題 (Combinatorial Reconﬁguration

り，その実装技術は確立されていない．2021 年 11 月

Problems; [15] [17] [18]) とは，基となる組合せ問題とから 2022 年 3 月にかけて，組合せ遷移問題に関する

その二つの実行可能解が与えられたとき，一方から他方へ，隣接関係を満たしつつ，実行可能解のみを経初めての国際プログラミング競技会 CoRe Challenge
2022 †1 が開催されるなど，今後は工学レベルでの研由して到達可能かどうかを判定する問題である．組究開発の活発化が予想される．

合せ遷移問題の研究は，最近 10 年で理論計算機科学

解集合プログラミング (Answer Set Programming;の分野を中心に急速に発展し，理論的な基盤が整備

ASP [2] [11] [14] [16]) は，非単調推論，否定を含む論されつつある．特に計算複雑性の研究が盛んであり，理プログラミング，制約充足 (特に SAT)，演繹デー

基の組合せ問題が NP 完全であるとき，その遷移問

タベースを起源にもつ宣言的プログラミングパラダイ

題の多くが PSPACE 完全となることがわかってきてムである．ASP 言語は一階論理に基づく知識表現言いる [15]．このような問題の代表例として，命題論理語の一種である．ASP システムは，安定モデル意味の充足可能性判定問題 (SAT) ，集合被覆問題，独立論 [11] に基づく解集合を計算するプログラムである．

集合問題，支配集合問題，グラフ彩色問題を基とする

近年，SAT ソルバーの技術を応用した高速な ASP シ

組合せ遷移問題があげられる [5] [6] [12] [13] [15]．

ステムが開発され，AI 分野を中心に，制約充足問題，

組合せ遷移ソルバー (Combinatorial Reconﬁgura-

有界モデル検査，プランニング，システム生物学など

tion Solvers) は，与えられた組合せ遷移問題が到達様々な分野への実用的応用が急速に拡大している [7].

可能か到達不能かを判定するプログラムである．到達

本稿では，ASP に基づく組合せ遷移ソルバーの設

An ASP-based Combinatorial Reconﬁguration Solver
and its Performance Evaluation
Yuya Yamada, Mutsunori Banbara, 名古屋大学 大学
院 情 報 学 研 究 科, Graduate School of Informatics,
Nagoya University.

計と実装について述べる．開発した組合せ遷移ソル
バー recongo は，組合せ遷移問題のインスタンスと†1 https://core-challenge.github.io/2022/

最後に，提案ソルバー recongo の性能評価として，組合せ遷移問題を解くための ASP 符号化 (論理プロ
グラム) を入力として，高速 ASP システム clingo †2

国際競技会 CoRe Challenge 2022 の結果と考察を示を用いて組合せ遷移問題の解を求めるシステムであす．なお，recongo は同競技会の Solver Track 全 6

る．recongo は，組合せ遷移問題の到達性判定にくわ部門のうち，Single-engine Solvers shortest 部門でえ，最短経路長，最長経路長，遷移最適化など他のバ優勝，その他 4 部門でも入賞している．

リエーションにも対応している．

以降，第 2 節では，組合せ遷移問題について例を

まず最初に，組合せ遷移問題の解法として有界組使って説明する．第 3 節では，ASP の言語構文を簡合せ遷移を提案する．有界組合せ遷移は，組合せ遷

単に説明する．第 4 節では，有界組合せ遷移のアイ移問題に対して，制限された長さ ℓ の (すなわち有界

デアを示す．第 5 節では，有界組合せ遷移アルゴリの) 遷移系列を求める問題を論理プログラム φℓ とし

ズムと recongo の実装について述べる．第 6 節では，て表現し，それを ASP システムを使って解くことに国際競技会 CoRe Challenge 2022 の結果と考察を示

より到達性の検査を行う方法である．ASP システム

す．最後に，第 7 節で本稿をまとめる．

が充足可能と判定した場合，制限された長さの到達可能な遷移系列が存在することを意味する. 逆に充足

2 組合せ遷移

不能と判定した場合，制限された長さでは到達不能

本節では，組合せ遷移問題の概要について述べたあであることを意味する．この場合，遷移系列の長さ ℓと，代表的な組合せ遷移問題の一つである独立集合遷を増加させた論理プログラムを構成し，再び ASP シ移問題について，例を用いて説明する．また，国際競ステムによる実行を繰り返す．

技会 CoRe Challenge 2022 の概要についても触れる.

つぎに，有界組合せ遷移のアルゴリズムとして，基本アルゴリズムと改良アルゴリズムの二つを示す．基2. 1 組合せ遷移問題

本アルゴリズムは，ステップ長 ℓ を増やしながら φℓ組合せ遷移問題 (Combinatorial Reconﬁguration

を繰り返し構成して解く素朴なアルゴリズムである．

Problems; [15] [17] [18]) とは，基となる組合せ問題と改良アルゴリズムは，インクリメンタルに φℓ を構成

その二つの実行可能解が与えられたとき，一方から他しながら解くように工夫されている．そのため，φℓ方へ，隣接関係を満たしつつ，実行可能解のみを経由の構成にかかるコストを抑えつつ，獲得した学習節

して到達可能かどうかを判定する問題である．入力とを再利用した効率のよい到達性の検査が可能となる．

して与えられる二つの実行可能解の片方をスタート

つづいて，組合せ遷移ソルバー recongo の実装コー

状態，他方をゴール状態とよぶ．組合せ遷移問題は，ドを示す．このコードは，改良アルゴリズムを clingo

基となる組合せ問題の実行可能解が形成する解空間の Python API を用いて僅か 30 行程度で簡潔に実グラフ上の問題として定義される．解空間グラフにお装したものである．また，recongo のプログラム例とける頂点は実行可能解を表し，辺は隣接関係を満たす

して，代表的な組合せ遷移問題の一つである独立集合

二つの実行可能解の組を表す．基となる組合せ問題が遷移問題 [15] の ASP 符号化を示す．

実行可能解の存在性を判定するのに対し，組合せ遷移

ASP に基づくアプローチにはいくつかの利点がある．ASP の高い表現力により，様々な組合せ遷移問題

問題は解空間グラフの構造や性質を分析することを主眼とする．

を簡潔に記述できる．マルチショット ASP 解法によ組合せ遷移問題にはさまざまなバリエーションが存り，遷移問題の到達可能性を効率的に検査できる [8]．

在する．入力となる実行可能解の数によって以下のよ

探索ヒューリスティックスを簡単にカスタマイズできうに分類される．入力として二つの実行可能解が与える [10]．効率的な解列挙が可能である [9]．

られるものとしては，解空間グラフ上の 2 頂点間の経路の有無を判定する到達性判定，最短経路を求め†2 https://potassco.org/clingo/

る最短経路長，ループのない最長経路を求める最長経

1

2

1

2

3

4

5

3

4

5

6

7

8

6

7

8

図 1: サイズ k = 3 の独立集合問題例: 入力例 (左) と実行可能解 (右)

t=0
1

t=1
2

3

4

5

6

7

8

1

⇒

t=2
2

3

4

5

6

7

8

1

⇒

t=3
2

3

4

5

6

7

8

1

⇒

スタート状態

2

3

4

5

6

7

8

ゴール状態
図 2: 独立集合遷移問題の例

路長がある．入力として一つの実行可能解が与えられが可能である．ただし，トークンが配置された頂点のる遷移最適化は，ある頂点から隣接関係を満たしつつ集合は，つねに独立集合問題の制約を満たさなけれ遷移できる頂点のなかで，目的関数を最大あるいは最ばならない．最終的に，トークンの配置された頂点小にするものを求める．入力となる実行可能解がないの集合がゴール状態の独立集合と一致すれば到達可ものとしては，解空間グラフが連結かどうかを判定す能となる．独立集合遷移問題の隣接関係については，

る連結性判定と，任意の二つの実行可能解の最短経路

1 回の遷移でちょうど一つのトークンが移動するトーのうちの最大長を求める直径がある．

クンジャンピング (Token Jumping; TJ) と，1 回の遷移でちょうど一つのトークンが隣接頂点へ移動す

2. 2 独立集合遷移問題

るトークンスライディング (Token Sliding; TS) の 2

無向グラフ G = (V, E) が与えられたとき，サイズ k の独立集合 (Independent Set) V′′⊆ V とは，′種類が広く研究されている．
独立集合問題の入力例とその実行可能解を図 1 に| V |= k であり，任意の 2 頂点 v1 , v2 ∈ V について示す．この実行可能解では，黄色で示された頂点 1,(v1 , v2 ) ∈/ E となるような V の部分集合 V ′ である．

6, 8 が独立集合に含まれる．図 2 は，独立集合遷移

独立集合問題 (Independent Set Problem) は，与え問題の例である．この例では，スタート状態 (t = 0)

られたグラフ G と自然数 k に対して，G がサイズ k

からゴール状態 (t = 3) へ，3 ステップの遷移で到達の独立集合をもつかどうかを判定する問題である．独している．各ステップ t では独立集合問題の制約を満立集合遷移問題 (Independent Set Reconﬁguration

たしている．また各遷移では，1 回の遷移でちょうど

Problem; [15]) は，独立集合問題を基とする組合せ遷

一つのトークンが移動しており，隣接関係 TJ を満た移問題である．

していることがわかる．一方で，ゴール状態に注目す

独立集合遷移問題は，トークン (Token) を移動させる問題と考えることもできる．スタート状態の独立集合に含まれるすべての頂点にトークンを配置する．
トークンは隣接関係を満たすように移動させること

ると，どのトークンも隣接関係 TS のもとでは移動できないため，図 2 の例は到達不能となる．

2. 3 CoRe Challenge 2022
CoRe Challenge 2022 は，2021 年 11 月から 2022

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

年 3 月にかけて開催された，組合せ遷移問題に関する

論理プログラム

⇐

,

;

∼

初めての国際プログラミング競技会である．この競技

ソースコード

:-

,

;

not

会は，隣接関係 TJ の独立集合遷移問題を解く Solver

Track と，独立集合遷移問題を生成する Graph Track

ダイムである．ASP の言語は，一般拡張選言プログの二つのトラックから構成されている．本稿は Solver

ラムに基づいている．本稿では説明の簡略化のため，

Track を対象とする．

そのサブクラスである標準論理プログラムについて

Solver Track は次の 3 部門にわけられる．

説明する．以降，標準論理プログラムを，単に論理プ• existent 部門

ログラムとよぶ．

組合せ遷移問題の到達性判定に関する部門である．独立集合遷移問題の到達性 (到達可能あるいは到達不能) を判定し，解けた問題数を競う．

• shortest 部門

論理プログラムは，以下の形式をしたルールの有限集合である．

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

組合せ遷移問題の最短経路長に関する部門であ

ここで，0 ≤ m ≤ n であり，各 ai はアトム，∼ はデ
フォルトの否定 †3 ，“,” は連言を表す．⇐ の左側をる．独立集合遷移問題のできるだけ短い遷移系列

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

を求め，その短さを競う．

は，「a1 , . . . , am がすべて成り立ち，am+1 , . . . , an の

• longest 部門

それぞれが成り立たないならば，a0 が成り立つ」で組合せ遷移問題の最長経路長に関する部門であある．ボディが空のルール (すなわち a0 ⇐) をファクる．独立集合遷移問題のできるだけ長い遷移系列

トとよび，⇐ を省略してよい．

を求め，その長さを競う．

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

longest 部門では，遷移系列に同じ状態が複数回出現⇐ a1 , . . . , am , ∼am+1 , . . . , ∼an

してはならないという制約が追加される．これは遷移

直観的には，⇐ a1 は，a1 ではないという禁止を表

系列にループが存在しないことと等しい．

し，⇐ ∼a1 は，a1 でなければならないという強制を

ベンチマーク問題は，7 種類の問題ファミリで構成された全 369 問である．問題の規模としては，グラフ表す．また，⇐ a1 , a2 は，a1 と a2 が，両方同時には成り立たないことを意味する．

の頂点数が 1 桁であるような小規模の問題から，グASP 言語は，組合せ問題を解くための便利な拡張

ラフの頂点数が 40,000 個にもなる大規模なものまで構文を備えている．その代表的なものが選択子と個数含まれる．

制約である．例えば，選択子 {a1 ; . . . ; an } をファク

各部門は，Single-engine Solvers と Overall Solvers

トとして書くと，アトム集合 {a1 , . . . , an } の任意のの二つの指標で評価される．前者は，逐次ソルバーの部分集合が成り立つことを意味する．個数制約は，選みが対象となる．後者は，逐次ソルバーに加え，ポー択子の両端に選択可能な個数の上下限を付けたもの

トフォリオ型ソルバーも含めたすべてのソルバーが対である．例えば，lb {a1 ; . . . ; an } ub ⇐ Body と書く

象となる．

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

3 解集合プログラミング

ASP システムは，与えられた論理プログラムか

解集合プログラミング (Answer Set Programming;ら，安定モデル意味論 [11] に基づく解集合を計算す

ASP [2] [11] [14] [16]) は，演繹データベース，否定をるソフトウェアである．ASP システムの多くは，変含む論理プログラミング，非単調推論，制約充足 (とくに SAT) を起源にもつ，宣言的プログラミングパラ†3 “失敗による否定” ともよばれる．述語論理で定義される否定 (¬) とは意味が異なる．

k(3).

% clingo isp_fact.lp isp.lp

node(1).

node(2).

node(3).

node(4).

node(5).

node(6).

node(7).

node(8).

edge(1,3). edge(2,5). edge(3,4). edge(3,6).
edge(4,5). edge(5,8). edge(6,7). edge(7,8).

コード 1: 図 1 の独立集合問題の ASP ファクト表現

clingo version 5.4.0
Reading from isp_fact.lp ...
Solving...
Answer: 1
in(1) in(6) in(8)SATISFIABLE(isp_fact.lp)
コード 3: clingo の実行例

1 K { in(X): node(X) } K :- k(K).
2 :- in(X), in(Y), edge(X,Y).
1 k(3).

コード 2: 独立集合問題を解くための論理プログラム(isp.lp)

2 node(1).

node(2).

node(3).

node(4).

3 node(5).

node(6).

node(7).

node(8).

4 edge(1,3). edge(2,5). edge(3,4). edge(3,6).
5 edge(4,5). edge(5,8). edge(6,7). edge(7,8).
6 3 {in(1);in(2);in(3);in(4);in(5);in(6);in(7);in(8)} 3.

数を含む論理プログラムを変数を含まない論理プロ
グラムに基礎化したのち，基礎ソルバーを用いて解集

7 :- in(1), in(3).
8 :- in(2), in(5).
9 :- in(3), in(4).

合を計算する．本研究で利用する高速 ASP システム

10 :- in(3), in(6).

clingo は，基礎化のためのグラウンダー gringo と基

11 :- in(4), in(5).

礎ソルバー clasp を，シームレスに結合したものである．以降で示す論理プログラムのソースコードはすべて clingo 言語で書かれており，表記上の対応につい12 :- in(5), in(8).
13 :- in(6), in(7).
14 :- in(7), in(8).

コード 4: コード 1 と 2 を基礎化した論理プログラムては表 1 の通りである．

ASP を用いた基本的な問題解法は，最初に解きたい問題を論理プログラムとして表現 (ASP 符号化) す

制約を表す．

る．つぎに ASP システムを用いて論理プログラムのコード 3 に，コード 1 とコード 2 を入力として与解集合を計算する．最後に解集合を解釈してもとの問えた場合の ASP システム clingo の実行例を示す．得

題の解を得る，という 3 段階からなる．以下，独立集

られた解集合 { in(1), in(6), in(8)} は，図 1 の右合問題を例にとって，各ステップごとに説明する．

側の実行可能解と対応している．

コード 1 に，サイズ k = 3 の独立集合問題の例

論理プログラムの基礎化について，もう少し詳しく(図 1) を ASP のファクト形式で表したものを示す．

説明する．clingo は，グラウンダー gringo を用いてアトム k/1 は独立集合のサイズ k を，node/1 は頂

コード 1 のファクトとコード 2 の論理プログラムを点を，edge/2 は辺を表している．ピリオド (“.”) は基礎化した後，clasp を用いて基礎化された論理プロ

ルールの終わりを表す終端記号である．

グラムの解集合を計算する．基礎化されたルールの集

コード 2 に，独立集合問題を解く論理プログラム

合をコード 4 に示す．6 行目がコード 2 の 1 行目に対を示す．アトム in/1 は，頂点 X が独立集合に含まれ応し，7–14 行目がコード 2 の 2 行目に対応している．

ることを表す．1 行目のルールは，ASP の個数制約を用いて「独立集合に含まれる頂点の数はちょうど K

4 有界組合せ遷移個となる」という制約を表している．2 行目のルール

有界組合せ遷移 (Bounded Combinatorial Recon-

は，ASP の一貫性制約を用いて「隣接する頂点 X とﬁguration) は，与えられた組合せ遷移問題に対して，

Y は，同時に独立集合に含まれることはない」という制限された長さの (すなわち有界の) 遷移系列を求める問題を論理式として記号的に表現し，その論理式をASP システム等の汎用ソルバーを使って解くことにInput: logic program φℓより，到達性の検査を行う方法である．

Parameter: maximum step length ℓmax

ソルバーが充足可能と判定した場合，制限された長Output: true if reachable and otherwise false

さの到達可能な遷移系列が存在することを意味する．

1: ℓ ← 0

逆に充足不能と判定した場合，制限された長さでは到

2: result ← none

達不能であることを意味する．この場合，遷移系列の

3: while ℓ ≤ ℓmax ∧ result ̸= satisﬁable do

長さを増加させた論理式を構成し，再びソルバーによる実行を繰り返す．有界組合せ遷移は，到達可能な遷移系列を探すだけで，到達不能の証明は行わない不完
全な手続きであるが，検査すべき遷移系列の長さに上限が存在する場合には，完全な手続きとなる．例えば，基の組合せ問題の直径を上限とすればよい †4 ．
組合せ遷移問題が与えられたとき，基の組合せ問題

4:s ← create a ASP system5:s.ground(φℓ )6:result ← s.solve()

7:

s.close()

8:

ℓ←ℓ+1

9: end while
10: return result = satisﬁableの変数集合 x = {x1 , x2 , . . . , xn }，各ステップ t ≥ 0に対して，ステップ t での各変数の値を表す変数集合xt

図 3: 基本アルゴリズム (到達性判定)= {xt1 , xt2 , . . . , xtn } を導入する．ここで，スタート状態を表す論理式を S(x)，基の組合せ問題の制(CSP) ソルバーなどが挙げられる．

約を表す論理式を C(x)，隣接関係を表す論理式をT (x, x′ )，ゴール状態を表す論理式を G(x) とする．

5 ASP に基づく組合せ遷移ソルバー

スタート状態から ℓ ステップ遷移した後の各変数の値∧∧
xℓ は，S(x0 ) ∧ ℓt=0 C(xt ) ∧ ℓt=1 T (xt−1 , xt ) を満

本節では，ASP に基づく組合せ遷移ソルバーの設計と実装について述べる．まず，第 4 節の有界組合

たす．そこで，ゴール状態と一致するかどうか判定す

せ遷移を実現するアルゴリズムを 2 種類提案する．

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

バックエンドのソルバーとしては，ASP システムの利用を前提とする．便宜上，アルゴリズム中の φℓ ,φℓ = S(x0 )
ℓ
ℓ
∧
∧
∧
C(xt ) ∧T (xt−1 , xt )
t=0

t=1

∧ G(xℓ )S(x), C(x), T (x, x′ ), G(x) は，第 4 節で述べた論
理式を論理プログラム (ASP のルール集合) として表現したものとする．つぎに，ASP システム clingo のPython API を用いた組合せ遷移ソルバーの recongo

与えられたステップ長 ℓ に対し φℓ が充足可能であれの実装について述べる．最後に，recongo のプログラば，到達可能な遷移系列が得られる．

ム例として，独立集合遷移問題の ASP 符号化を示す．

有界組合せ遷移は，SAT 技術を用いたモデル検査手法の一つである有界モデル検査 [1] [3] [4] を，組合

5. 1 有界組合せ遷移アルゴリズム

せ遷移に応用した解法といえる．有界組合せ遷移の有界組合せ遷移に基づき組合せ遷移問題の到達性

バックエンドで使用するソルバーとしては，本研究を判定するアルゴリズムとして，基本アルゴリズムとで採用した ASP システム以外にも，SAT ソルバー，

改良アルゴリズムの二つを考案した．

背景理論付き SAT (SMT) ソルバー，制約充足問題

基本アルゴリズムを図 3 に示す．基本アルゴリズ
ムの流れは以下の通りである．

†4 理論的には，問題の直径を超えるまで手続きを繰り返せばよいが，現実的には，しばしば直径が大きすぎて適用できない場合もある．

(1) ステップ長 ℓ と ASP システムの実行結果を格納する result を，ℓ ← 0 と result ← none に初Input: logic program S(x), C(x), T (x, x′ ), G(x)して，毎回 ASP システムを生成 (図 3 の 4 行目) する基本アルゴリズムは，探索中に得られた学習節を再Parameter: maximum step length ℓmax

利用できないため，同一の探索空間を何度も調べるこ

Output: true if reachable and otherwise falseとになり求解効率が低下する．また，毎回 φℓ 全体を

1: ℓ ← 0

基礎化 (図 3 の 5 行目) するコストも無視できない．
この問題を解決するために，マルチショット ASP

2: result ← none
3: s ← create a ASP system

解法 [8] を利用した改良アルゴリズムを提案する．こ4: while ℓ ≤ ℓの解法を利用することにより，ルールを動的に追加・

max∧ result ̸= satisﬁable do

5:s.ground(C(xℓ ) ∪ T (xℓ−1 , xℓ ) ∪ G(xℓ ))6:

if ℓ > 0 then

削除した一連の論理プログラムを，同様の探索失敗を防ぐために獲得した学習節を再利用しながら，連続的に解くことが可能となる．

s.remove(G(xℓ−1 ))7:

改良アルゴリズムを図 4 に示す．改良アルゴリズ

else

8:

ムの流れは以下の通りである．

09:s.ground(S(x ))10:

end if

11:

result ← s.solve()

納する result を，ℓ ← 0 と result ← none に初

12:

ℓ←ℓ+1

期化する (1–2 行目)．

(1) ステップ長 ℓ と ASP システムの実行結果を格

13: end while(2) ASP システムを生成し，s と置く (3 行目)．

14: s.close()(3) ℓ ≤ ℓmax ，かつ，result が充足可能 (satisﬁable) でないかぎり以下を繰り返す．

15: return result = satisﬁable(a) 論 理 プ ロ グ ラ ム C(xℓ ), T (xℓ−1 , xℓ ),G(xℓ ) を基礎化する (5 行目)．

図 4: 改良アルゴリズム (到達性判定)(b) ℓ > 0 のとき，論理プログラム G(xℓ−1 )期化する (1–2 行目)．

に対応する制約を削除する．そうでないと(2) ℓ ≤ ℓmax ，かつ，result が充足可能 (satisﬁable) でないかぎり以下を繰り返す．

き，S(x0 ) を基礎化する (6–10 行目)．

(c) ASP システムを実行し，結果を result に(a) ASP システムを生成し，s と置く (4 行目)．

保存する (11 行目)．

(b) 論理プログラム φℓ を基礎化する (5 行目)．

(d) ℓ ← ℓ + 1 とする (12 行目)．

(c) ASP システムを実行し，結果を result に(4) ASP システムを終了する (14 行目)．

保存する (6 行目)．

(5) result が充足可能の場合は true を返す．そう(d) ASP システムを終了する (7 行目)．

でない場合は false を返す (15 行目)．

(e) ℓ ← ℓ + 1 とする (8 行目)．

改良アルゴリズムは，ステップ長 ℓ を増やしながら，(3) result が充足可能の場合は true を返す．そう

インクリメンタルに φℓ を構成し解探索を行う．具体的には，φℓ は，φℓ−1 に C(xℓ ), T (xℓ−1 , xℓ ), G(xℓ )でない場合は false を返す (10 行目)．
基本アルゴリズムは，ステップ長 ℓ を増やしながら複を追加し，G(xℓ−1 ) を削除することで，インクリメ数の φℓ を繰り返し構成して解く素朴なアルゴリズム

ンタルに構成できる．そのため，基礎化のコストを抑である．実装が単純という反面，以下のような短所がえつつ，獲得した学習節を再利用した効率のよい到達ある．そもそも，φℓ−1 と φℓ に含まれるルールの大部可能性の検査が可能となる．

ℓ

分は同じである．実際に φℓ−1 と φℓ の差は，C(x ),
ℓ−1

ℓ

ℓ−1

ℓ

上で示した二つのアルゴリズムは，組合せ遷移問題), G(x ) となり，これら以外のの到達性判定を行うものである．これらのアルゴリズ

ルールはすべて共通している．そのため，各 φℓ に対ムは，探索戦略としてステップ ℓ に関する線形探索をT (x, x ), G(x採用しているため，最短経路長にもそのまま利用でき

1 k(3).

る．また，最長経路長や遷移最適化にも容易に拡張可

2 node(1).

node(2).

node(3).

node(4).

能である．

3 node(5).

node(6).

node(7).

node(8).

4 edge(1,3). edge(2,5). edge(3,4). edge(3,6).
5 edge(4,5). edge(5,8). edge(6,7). edge(7,8).

5. 2 組合せ遷移ソルバー recongo の実装
組合せ遷移ソルバー recongo は，ASP に基づく組合せ遷移問題の汎用ソルバーである．recongo は，与えられた組合せ遷移問題のインスタンス (ASP のファ
クト形式) と組合せ遷移問題を解くための ASP 符号6
7 start(3). start(5). start(7).
8 goal(1).

goal(2).

goal(4).

コード 5: 図 2 の独立集合遷移問題の ASP ファクト
表現 (isrp_fact.lp)化を入力とし，高速 ASP システム clingo を用いて解を求める (図 5 参照)．

1 #program base.

図 6 に，Python 言語で書かれた recongo ソルバーの実装を示す．このコードは，図 4 に示した改良ア
ルゴリズムを clingo の Python API を用いて実装したものであり，大部分が対応している．例えば，変数
max

core_max は，図 4 における ℓを表す．7 行目で2 :- not in(X,0), start(X).
3
4 #program step(t).
5 K { in(X,t): node(X) } K :- k(K).
6 :- in(X,t), in(Y,t), edge(X,Y).
7
8 moved_from(X,t) :- in(X,t-1), not in(X,t), t > 0.

定義される step と ret は，ℓ と result に対応する．

9 :- not 1 { moved_from(X,t) } 1, t > 0.

また，11–12 行目は，図 4 中の 5 行目に対応してい10

る．13–17 行目は，図 4 中の 6–10 行目に対応している．recongo では，制約を取り除くのではなく，外部からアトムの真偽値を切り替えることで制約を無効化している．具体的には，30 行目の#external 宣言で

11 #program check(t).
12 :- not in(X,t), goal(X), query(t).

コード 6: 独立集合遷移問題を解くための論理プログ
ラム (isrp.lp)

指定したアトム query/1 に対して，14 行目で偽を割り当てることで，query/1 を含む一貫性制約が必ず

トム start(3) は，スタート状態で頂点 3 が独立集成り立たなくなるようにしている．18 行目でステッ合に含まれることを意味している．

プ数 t で追加されるルールの基礎化を行い，20 行目の prg.solve() で到達可能性を検査している．

独立集合遷移問題の ASP 符号化をコード 6 に示す．
この符号化は，改良アルゴリズムを用いることを前recongo は，ステップ長 ℓ を 0 から 1 ずつ増やしな提に設計されている．そのため，#program 宣言子をがら繰り返し問題を解く．したがって，遷移系列を見用いて，base，step(t)，check(t) の 3 パートにわつけた場合，その遷移系列は与えられたインスタンス

けて記述されている．step(t) と check(t) の引数 tに対して必ず最短なものとなる．

はステップを表す定数パラメータである．

• はじめに base パートには，ステップ t=0 で満
5. 3 プログラム例

たすべき制約を記述する．ここでは 2 行目のルー

recongo のプログラム例として，独立集合遷移問題

ルで，スタート状態とステップ 0 での独立集合の ASP 符号化を示す．コード 6 に，図 2 の独立集に含まれる頂点が一致することを強制している．

合遷移問題を ASP のファクト形式で表したものを示• つぎに step(t) パートには，各ステップ t におす．基となる独立集合問題のサイズを表すアトム k/1，

いて満たすべき制約を記述する．ここでは，第 3頂点を表す node/1，辺を表す edge/2 に加えて，ス節のコード 2 で示した独立集合問題の ASP 符号

タート状態を表す start/1 (7 行目) とゴール状態を化の各アトムにステップを表す項 t を引数とし表す goal/1 (8 行目) が追加されている．例えば，アて追加したルールを記述している (5–6 行目)．

recongo
組合せ遷移問題のインスタンス-

変換器- ASP ファクト -6
論理プログラム- 組合せ遷移問題

clingoの解?

有界組合せ遷移アルゴリズム図 5: 組合せ遷移ソルバー recongo

1 #script (python)
2 import clingo
3
4 def main(prg):
5
core_max = prg.get_const("core_max")
6
7
step, ret = 0, None8while (step <= core_max.number and (step == 0 or not ret.satisfiable)):9parts = []1011parts.append(("step", [clingo.Number(step)]))12
parts.append(("check", [clingo.Number(step)]))13
if step > 0:
14
prg.release_external(clingo.Function("query", [clingo.Number(step-1)]))15
prg.cleanup()
16
else:
17
parts.append(("base", []))
18
prg.ground(parts)
19
prg.assign_external(clingo.Function("query", [clingo.Number(step)]), True)
20
ret, step = prg.solve(), step+1
21
22
print(’c step: %s’ % str(step-1))
23
if (step != 0 and ret.satisfiable):24
print(’s REACHABLE’)
25
else:
26
print(’s UNREACHABLE’)
27
28 #end.
29 #program check(t).
30 #external query(t).

図 6: clingo の Python API を用いた，recongo の実装 (core.lp)• さらに，8–9 行目には，隣接関係を表すルール

態とステップ t の対応を記述する．ステップ長がを記述している．moved_from(X,t) は，ステッℓ−1 から ℓ に変化したとき，query(ℓ−1) の値割

プ t-1 からステップ t への遷移において，頂点当てを動的に操作することにより，check(ℓ − 1)

X のトークンが移動したことを意味する．9 行目のルールを無効化する．

のルールで，各ステップ t において，移動した

以上のように，独立集合遷移問題の制約は，ステップ

トークンの数がちょうど一つであることを保証し

t をパラメータとした僅か 6 個のルールからなる論理ている．

プログラムで簡潔に表される．

• 最後に，check(t) パートでは，プログラムの終コード 7 に，コード 5 とコード 6 を入力として与了条件を記述する．ここでは，12 行目でゴール状えた場合の recongo の実行例を示す．得られた解集合

会の Web ページと同様に “@提出者” の形式で記載% clingo core.lp isrp_fact.lp isrp.lp
clingo version 5.4.0
Reading from core.lp ...
Solving...

している．各スコアについて，existent 部門では到達可能性を判定できた問題数 (到達可能/到達不能) を，

shortest 部門では最短の遷移系列を求めることがでSolving...
Solving...

きた問題数を，longest 部門では最長の遷移系列を求Solving...

めることができた問題数を示している．recongo は，Answer: 1
in(3,0) in(5,0) in(7,0) in(2,1) in(3,1) in(7,1) in(1,2) in(2,2)
in(7,2) in(1,3) in(2,3) in(4,3)
SATISFIABLE

existent 部門で 2 位，shortest 部門で 1 位，longest
部門で 2 位となった．全体的に，プランニングや有界モデル検査の技術を利用したソルバーが上位を占め

c step: 3ている．

s REACHABLE

コード 7: recongo の実行例

existent 部門の問題ファミリごとのスコアを表 3 に示す．recongo は，最短経路長が非常に短い問題の多い color04 に属する問題をすべて解いている．一方{in(3,0). . . in(4,3)} は，図 2 のステップ長 3 の遷で，到達不能な問題が多い grid や，最短経路長が数移系列と対応している．

百を超える問題を多く含む power, sp, square では，ほとんどの問題を解けなかった．

6 CoRe Challenge 2022 の結果と考察

shortest 部門の問題ファミリごとのスコアを表 4 に

本節では，第 2 節で述べた組合せ遷移問題に関する示す．問題数については，到達不能と判定できた問題

国際プログラミング競技会 (CoRe Challenge 2022)の結果 †5 をもとに，開発した recongo ソルバーの性能は評価に含まれないため，ポートフォリオ型ソルバー

評価を行う．recongo ソルバーは，独立集合遷移問題

た問題の数を表記している．recongo は，existent 部を解く性能を競う Solver Track の全 3 部門 (existent,

門と同様，color04 のすべての問題に対して，最短経を含むすべてのソルバーで到達不能と判定できなかっshortest, longest 部門) に参加した．各部門の結果は，路長を求めることに成功している．一方で，power や

逐次ソルバーのみが対象の Single-engine Solvers とsquare については，上位 3 ソルバーすべてがスコア

逐次ソルバーに加えポートフォリオ型ソルバーも対象を獲得できていない．

となる Overall Solvers の二つのタイプにわけられ，
計 6 部門 (3 部門 ×2 タイプ) で評価される．

longest 部門の問題ファミリごとのスコアを表 5 に示す．問題数は表 4 と同じである．recongo は，queen

結果. recongo ソルバーは，Single-engine Solversの属する問題について良い性能を示した．これは，re-shortest 部門で第 1 位を獲得した．また，全体としてcongo が longest 部門に対応できたことで，shortest

は，Solver Track 全 6 部門中 5 部門で入賞した．なお，

で解いた問題のほぼすべてで，遷移系列長を更新でき

競技会の参加ソルバー数は，逐次ソルバーが 6，ポー

たことが要因と考えられる．他のソルバーを見てみる

トフォリオ型ソルバーが 2 の合計 8 ソルバーであっと，PARIS single は n = 8, 10 の小規模なクイーン

た．以下，逐次ソルバーを対象とする Single-engine

グラフについては 3 桁の遷移系列を求めている一方

Solvers の結果について詳しく述べる．

で，残りの問題は shortest 部門で遷移系列を求めてSingle-engine Solvers 全 3 部門の入賞ソルバーをいたにも関わらず，一つも遷移系列を求められていな

表 2 に示す．各部門の 1 位から 3 位までのソルバー

い．また recongo は，color04 については他の 2 部門について，ソルバー名，実装技術，スコアを記載してと比べて性能を落としている．これは，ステップ長をいる．ソルバー名が未公開のものについては，競技1 ずつ増やしていくため，より長い遷移系列を求める
必要がある本部門を苦手としたと考えられる．

†5 https://core-challenge.github.io/2022result/考察. 上で述べた CoRe Challenge 2022 の各部門

表 2: Single-engine Solvers: 全 3 部門の入賞ソルバー
部門

existent

1位

2位

3位

ソルバー名

PARIS single

recongo@toda5603

実装技術

プランニングASP貪欲法/有界モデル検査

スコア

299 (275/24)

244 (238/6)

207 (207/0)

recongo@tigrisg

PARIS single

ASP

総当り/SARSA

プランニングソルバー名

shortest

実装技術
スコア

longest

238

232

213

ソルバー名

PARIS single

recongoReconfAIGERation

実装技術

プランニングASP

SAT/有界モデル検査

144

115

54

スコア

表 3: Single-engine Solvers existent 部門: 問題ファミリごとのスコア問題ファミリ

問題数

PARIS single

recongo@toda5603

color04

202

202

202

194

grid

49

25

7

2

handcraft

6

6

6

4

power

17

4

0

0

queen

48

48

26

6

sp

30

8

3

1

square

17

6

0

0

合計

369

299

244

207

表 4: Single-engine Solvers shortest 部門: 問題ファミリごとのスコア問題ファミリcolor04

問題数recongo@tigrisg

PARIS single

202

202

192

177

grid

4

2

2

0

handcraft

5

5

5

3

power

17

0

0

0

queen

48

26

25

25

sp

30

3

8

8

square

17

0

0

0

合計

323

238

232

213

の結果から，ステップ長に関する探索戦略が recongoとができ，shortest 部門のよい結果につながった．しの性能に大きく影響したと考えられる．現行の re-

かし，その一方で，最短経路長が数百を超えるような

congo は，ステップ長を 1 ずつ増やす線形探索を採用

問題を多く含む power, sp, square では，多くの問題している．そのため，最短経路長が短い問題の多いで遷移系列を求めることができなかった．この問題をcolor04 ではすべての問題でその最短系列を求めるこ

解決する方法としては，二分探索や指数探索を用いた

表 5: Single-engine Solvers longest 部門: 問題ファミリごとのスコア問題ファミリ

問題数

PARIS single

recongoReconfAIGERation

202

120

92

36

grid

4

1

2

0

handcraft

5

3

4

2

power

17

1

0

1

queen

48

8

15

7

sp

30

4

2

5

square

17

7

0

3

合計

323

144

115

54

color04

探索戦略が考えられる．これらの戦略は，単純な線形

経路長，遷移最適化など他のバリエーションにも対応

探索と比較して，充足不能の判定回数を減らすことがしている．

できるため，遷移系列の長い問題に対する求解性能の向上が期待できる．

プログラムの記述性. recongo は，ASP の高い表
現力を生かし，様々な組合せ遷移問題を簡潔に記述できる．代表的な組合せ遷移問題である独立集合遷移問

7 おわりに題の ASP 符号化を示し，僅か 6 個のルールで簡潔に

本稿では，解集合プログラミング (ASP) に基づく記述できることを確認した．

組合せ遷移ソルバーの設計と実装について述べた．ま

性能評価. 国際組合せ遷移競技会 CoRe Challenge

た，提案ソルバー recongo の性能評価として，国際2022 の結果をもとに，recongo の性能評価を示した．

競技会 CoRe Challenge 2022 の結果とその考察につrecongo は Solver Track 全 6 部門のうち，Single-

いて述べた．本稿の貢献と提案ソルバー recongo のengine Solvers shortest 部門で優勝，その他 4 部門

特長について以下にまとめる．

で入賞した．

ソルバーの設計. 組合せ遷移問題の解法として有界

今後の課題として，ステップ長 ℓ に関する探索戦略

組合せ遷移を提案した．有界組合せ遷移は，有界モデの改良が挙げられる．現行版 clingo は線形探索を採ル検査のアイデアを組合せ遷移に応用した解法であ用しているが，二分探索や指数探索を用いることで，り，本研究で利用した ASP システムのほかに，SAT充足不能の判定回数を減らすことができる．その結果

ソルバー，SMT ソルバー，CSP ソルバーなども適として，遷移系列の長い問題に対する求解性能の向上

用可能な汎用的なアプローチである．

が期待できる．また，複数の隣接関係をもつ組合せ遷

アルゴリズム. 有界組合せ遷移アルゴリズムとして，基本アルゴリズムと改良アルゴリズムの二つを考移問題に対する重み付き遷移最適化も，重要な今後の課題の一つである．

案した．特に，改良アルゴリズムは，マルチショット

ASP 解法を利用することで，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, Pro-

した効率的な到達性の検査ができる点が特長である．
ソルバーの実装. 組合せ遷移ソルバー recongo は，
改良アルゴリズムを clingo の Python API を用いて僅か 30 行程度で簡潔に実装されている点が特長である．本稿では触れなかったが，拡張版 recongo は組合せ遷移問題の到達性判定に加え，最短経路長，最長

ceedings 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 Computer 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 ] Gebser, M., Kaufmann, B., Neumann, A., andSchaub, T.: Conﬂict-Driven Answer Set Enumeration, Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2007), LNCS, Vol. 4483,
Springer, 2007, pp. 136–148.
[10] Gebser, M., Kaufmann, B., Romero, J., Otero,R., Schaub, T., and Wanko, P.: Domain-Speciﬁc
Heuristics in Answer Set Programming, Proceedingsof the Twenty-Seventh AAAI Conference on Artiﬁcial Intelligence (AAAI 2013), desJardins, M. and
Littman, M. L.(eds.), AAAI Press, 2013.
[11] 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.
[12] 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.
[13] Haddadan, A., Ito, T., Mouawad, A. E.,
Nishimura, N., Ono, H., Suzuki, A., and Tebbal,
Y.: The complexity of dominating set reconﬁguration, Theoretical Computer Science, Vol. 651(2016),
pp. 37–49.
[14] 井上克巳, 坂間千秋: 論理プログラミングから解集合
プログラミングへ, コンピュータソフトウェア, Vol. 25,
No. 3(2008), pp. 20–32.
[15] 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.
[16] Niemelä, I.:
Logic Programs with Stable
Model Semantics as a Constraint Programming
Paradigm, Ann. Mathematics and Artiﬁcial Intelligence, Vol. 25, No. 3–4(1999), pp. 241–273.
[17] Nishimura, N.: Introduction to Reconﬁguration,
Algorithms, Vol. 11, No. 4(2018), pp. 52.
[18] 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.