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

解集合プログラミングを用いたハミルトン閉路問題の解法に関する考察
平手 貴大

宋 剛秀

田村 直之

番原 睦則

本稿では，解集合プログラミング (ASP) を用いたハミルトン閉路問題，最短ハミルトン閉路問題，コスト制約付き
ハミルトン閉路問題の解法について述べる．ハミルトン閉路問題を解く ASP 符号化として，undirected，directed，
acyclicity の 3 つを考案した．undirected は，ハミルトン閉路問題を次数制約と連結制約で簡潔に表現した符号化である．directed は，与えられた無向グラフの各辺に対して，2 つの弧を対応させることで有向グラフ化して解く符号化である．acyclicity は，directed 符号化をベースに，連結制約に代わる部分閉路禁止制約を，ASP の組込み非閉路
制約で表現した符号化である．最短ハミルトン閉路問題とコスト制約付きハミルトン閉路問題については，考案した3 つの符号化に目的関数とコスト制約をそれぞれ追加することで自然に拡張できる．考案した符号化の有効性を評価するために，Flinders Hamiltonian Cycle Project で公開されているハミルトン閉路問題のインスタンス (全 1001
問) を用いて実験を行った．その結果，directed 符号化が，他の符号化と比較して，より多くの問題を高速に解くことができ，その優位性が確認できた．

の総和が所与の閾値以下 (または以上) であることを

1 はじめに制約条件として付加したコスト制約付きハミルトン

ハミルトン閉路問題 (Hamiltonian Cycle Problem;

閉路問題の解を高速に全列挙するアルゴリズムも提HCP) は，与えられたグラフの全頂点をちょうど一案されている [7]．本研究では，これらの (無向グラフ

度ずつ通る閉路が存在するかどうかを判定する問題

上の) ハミルトン閉路問題およびその関連問題を対象である [6]．ハミルトン閉路問題は代表的な NP 完全とする．

問題である．ハミルトン路問題 (Hamiltonian Path

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

Problem; HPP) は，ハミルトン閉路問題から始点とASP [1] [4] [8] [11]) は，論理プログラミングから派生し終点が一致するという閉路の条件を取り除いたもの

た宣言的問題解法のためのプログラミングパラダイである．これらの問題は，重要な工学的応用が数多くムである．ASP 言語は，一階論理に基づく知識表現存在するため，古くから盛んに研究されている．例え

言語の一種である．論理プログラムは ASP のルール

ば，数理最適化の分野で有名な巡回セールスマン問の有限集合である．ASP システムは論理プログラム

題は，グラフの辺に距離が付随しているとき，最短距から安定モデル意味論に基づく解集合を計算するシ離のハミルトン閉路を求める最短ハミルトン閉路問

ステムである．近年，SAT 技術を応用した高速 ASP

題と考えることができる．また，ごく最近では，距離システムが開発され，スケジューリング，プランニン
グ，システム生物学，システム検証など様々な分野へ

A Study on Solving Hamiltonian Cycle Problem with
Answer Set Programming
Takahiro Hirate, Mutsunori Banbara, 名 古 屋 大 学 大学院情報学研究科, Graduate School of Informatics,
Nagoya University.
Takehide Soh, Naoyuki Tamura, 神戸大学 情報基盤センター, Information Science and Technology Center,
Kobe University.

の実用的応用が急速に拡大している．ハミルトン閉路問題およびその関連問題に対して ASP を用いる利点としては，ASP 言語の高い表現力，高速な解列挙，
組込み非閉路制約，充足不能コアに基づく最適化，インクリメンタル ASP 解法などが挙げられる．
本論文では，解集合プログラミング (ASP) を用い図1

D. E. Knuth の教科書にある米国本土 48 州の隣接関係を表すグラフ

たハミルトン閉路問題，最短ハミルトン閉路問題，コ• ハミルトン閉路問題は，与えられたグラフの全

スト制約付きハミルトン閉路問題の解法について述

頂点をちょうど一度ずつ通る閉路が存在するかど

べる．ハミルトン閉路問題を解く ASP 符号化としうかを判定する問題である．

て，undirected，directed，acyclicity の 3 つを考案し• 最短ハミルトン閉路問題は，グラフの辺に距離た．undirected は，ハミルトン閉路問題を次数制約が付随しているとき，最短距離のハミルトン閉路と連結制約で簡潔に表現した符号化である．directedを求める最適化問題である．

は，与えられた無向グラフの各辺 u − v に対して，2• コスト制約付きハミルトン閉路問題は，ハミル

つの弧 u → v と v → u を対応させることで有向グ

トン閉路問題に，距離の総和が所与の閾値以下ラフ化して解く符号化である．acyclicity は，directed(または以上) であることを制約条件として付加符号化をベースに，連結制約に代わる部分閉路禁止制した問題である [7]．

約を，ASP の組込み非閉路制約 [2] で表現した符号

これらの問題から，始点と終点が一致するという閉路化である．最短ハミルトン閉路問題とコスト制約付きの条件を取り除いた問題を，それぞれ，ハミルトン路

ハミルトン閉路問題については，考案した 3 つの符問題，最短ハミルトン路問題，コスト制約付きハミル号化に目的関数とコスト制約をそれぞれ追加するこトン路問題と呼ぶ．

とで自然に拡張できる．

図 1 は，D. E .Knuth の The Art of Computer

考案した符号化の有効性を評価するために，Flinders

Programming [10] に記載されている米国本土 48 州

Hamiltonian Cycle Project (FHCP) で公開されていの隣接関係を表すグラフである．この隣接グラフの頂る HCP インスタンス (全 1001 問) [5] を用いて実験

点数は 48，辺の数は 105 である．各辺に付与されてを行った．この問題集は FHCP Challenge と呼ばれいる数字は，州都の間の距離 (マイル) を表している．

る国際競技会で使用された頂点数が 66 個から 9,528

西海岸ワシントン州 (WA) から東海岸メーン州 (ME)個の HCP インスタンスから構成されている．実験のまでのハミルトン路は 6,876,928 通りあり，最短ハミ結果，directed 符号化が 875 問と最も多くの問題を解

ルトン路は 11,698 マイルである．コスト制約付きハき，他の符号化と比較してその優位性が確認できた．

ミルトン路問題は，WA から ME までの距離の総和がある閾値以下であるハミルトン路を求める問題と2 ハミルトン閉路問題とその関連問題

考えることができる．本稿では，コスト制約付きハグラフの全頂点を一度ずつ通る路はハミルトン路

ミルトン路問題の解を全列挙する問題を対象とする．

(Hamiltonian Path) と呼ばれ，閉路はハミルトン閉

例えば，コスト制約を最短距離の 10%増 (12,868 マ

路 (Hamiltonian Cycle) と呼ばれる．以下に，本稿でイル) 以内とした場合，解の総数は 16,180 個である．

対象とする問題群について述べる．

23 解集合プログラミング

1

1

3

5

解集合プログラミング (ASP; [1] [4] [8] [11]) の言語
は，一般拡張選言プログラムに基づいている．本稿で3

2は説明の簡略化のため，そのサブクラスである標準論

2

3

理プログラム (以降，論理プログラムと呼ぶ) につい

2て説明する．以降，論理プログラムのソースコードは
すべて ASP システム clingo †1 の言語構文に従う．

1
4

図2

6

重み付き無向グラフの例

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

a0 :- a1 , . . . ,am ,not am+1 , . . . ,not an .

% nodenode(1). node(2). node(3). node(4). node(5). node(6).

ここで，0 ≤ m ≤ n であり，各 ai はアトム，notはデフォルトの否定 †2 ，カンマ (“,”) は連言を表す．

% edgeピリオド (“.”) はルールの終わりを表す終端記号であ% distanceる．“:-” の左側をヘッド，右側をボディと呼ぶ．ルー

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

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

cost(3,5,1). cost(4,6,1). cost(5,6,2).

ルの直観的な意味は，「a1 , . . . , am がすべて成り立ち，

am+1 , . . . , an のそれぞれが成り立たないならば，a0

コード 1

グラフ (図 2) の ASP ファクト表現が成り立つ」である．
ボディが空のルール (すなわち a0 :-.) をファク

潔に記述できる#edge 宣言が追加されている [2]．例

トと呼び，“:-” を省略してもよい．また，以下のよ

えば，#edge(X,Y): arc(X,Y). は，arc(X,Y) を満

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

たす有向辺 X → Y を辺集合としてもつグラフが，閉:- a1 , . . . ,am ,not am+1 , . . . ,not an .

路をもたないことを保証する．

例えば，:- not a1 ,a2 . は，
「a2 が成り立つならば，a1 が成り立つ」を意味する．

4 ハミルトン閉路問題の ASP 符号化

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

図 3 に，ASP を用いたハミルトン閉路問題の解法

張構文として，選択子と個数制約が用意されている．

を示す．これは，与えられた問題インスタンスを ASP

例えば，選択子{a1 ; . . . ;an } をファクトとして書く

ファクト形式に変換し，ハミルトン閉路問題を解くと，「アトム集合 {a1 , . . . , an } の任意の部分集合が成論理プログラム (ASP 符号化) と結合した後，ASPり立つ」を意味する．個数制約は選択子の両端に選システムを用いて解を計算する一般的な解法である．

択可能な個数の上下限を付けたものである．例えば，

本節では，ハミルトン閉路問題のインスタンスを記:- not lb {a1 ; . . . ;an } ub,b. と書くと，「b が成り立

述するための ASP ファクト形式を説明した後，ハつならば，a1 , . . . , an のうち，lb 個以上 ub 個以下がミルトン閉路問題を解くための 3 つの ASP 符号化成り立つ」を意味する．

undirected, directed, acyclicity について述べる．

また，組合せ最適化問題を解くために，最小化関数(#minimize) と最大化関数 (#maximize) 等も用意さ

4. 1 ASP ファクト形式

れている．さらに，最近では，グラフ問題を解くため

最短ハミルトン閉路問題を例にとって，入力となの便利な拡張構文として，有向グラフの非閉路性を簡る重み付き無向グラフ (図 2) の ASP ファクト形式†1 https://potassco.org/clingo/†2 失敗による否定とも呼ばれる．述語論理の否定 (¬)とは意味が異なる．

をコード 1 に示す．アトム node/1 は頂点，edge/2
は辺，cost/3 は距離を表す．例えば，edge(1,2) は，
辺 1 – 2 を表し，cost(1,2,3) は，この辺の重みがHCP 問題
インスタンス-

変換器-

ASP ファクト

-ASP システム-

HCP 問題の解ASP 符号化(論理プログラム)

図3

1
2
3
4
5
6
7

ASP を用いたハミルトン閉路問題 (HCP) の解法{ in(X,Y) } :- edge(X,Y).
:- not 2 { in(X,_) ; in(_,X) } 2, node(X).
reached(s).
reached(Y) :- reached(X), in(X,Y).
reached(Y) :- reached(X), in(Y,X).
:- not reached(X), node(X).
コード 2

undirected 符号化

番号を表し，実際の値は実行時に与えられる．

• 1 行目のルールは，各辺 edge(X,Y) に対して，
その辺がハミルトン閉路に含まれるかどうかを意味するアトム in(X,Y) を選択子を使って導入している．

• 次数制約は 2 行目のルールで表される．このルー
ルは，各頂点 node(X) に対して，その次数が 2 に等しくなることを個数制約を使って表している．

1
2
3
4
5
6
7
8
9

{ in(X,Y) ; in(Y,X) } 1 :- edge(X,Y).
:- not 1 { in(X,_) } 1, node(X).
:- not 1 { in(_,X) } 1, node(X).
reached(s).
reached(Y) :- reached(X), in(X,Y).
:- not reached(X), node(X).
:- not X < Y, in(s,X), in(Y,s).

• 連結制約は 4–7 行目のルールで表される．ある頂点 X が始点 s から到達可能であることを意味する
補助アトム reached(X) を導入する．4 行目のファ
クトは，始点 s が到達可能あることを表している．

5 行目のルールは，各辺 X – Y に対して，その辺がハミルトン閉路に含まれ (in(X,Y))，かつ，頂点 X が始点から到達可能であれば (reached(X))，

Y も到達可能であることを表している．6 行目は
コード 3

directed 符号化

5 行目と同様であるが，辺を逆向きに辿った場合を表している．7 行目のルールは，すべての頂点

3，すなわち，頂点 1 と頂点 2 の距離が 3 であることが始点から到達可能でなければならないことをを示している．

一貫性制約を使って表している．
このように，undirected 符号化は，ハミルトン閉路問

4. 2 undirected 符号化

題の次数制約と連結制約を，ASP のルール 6 個で簡グラフ G = (V, E) にハミルトン閉路が存在する必潔に表現している．特に，4–7 行目のように連結制約

要十分条件は，以下の 2 つの制約を満たす部分グラを簡潔に記述できる点は，ASP の大きな特長の一つ′′

フ G = (V, E ) が存在することである．

である．

′

• G の各頂点の次数が 2 (次数制約)• G′ が連結である (連結制約)
ハミルトン路の場合，次数制約は「始点と終点の次数が 1，他の頂点の次数が 2」となる．

4. 3 directed 符号化
directed 符号化は，undirected 符号化をベースに，与えられた無向グラフの各辺 u − v に対して，2 つのundirected 符号化は，ハミルトン閉路問題の次数

弧 u → v と v → u を対応させることで有向グラフ化

制約と連結制約を，ASP の一貫性制約と個数制約して解く符号化である．コード 3 に，directed 符号化を使って表した基本的な符号化である．コード 2 にを示す．

undirected 符号化を示す．コード中の s は始点の頂点• 1 行目では，無向グラフの有向グラフ化を行う．

1
2
3
4
5
6
7

{ in(X,Y) ; in(Y,X) } 1 :- edge(X,Y).
:- not 1 { in(X,_) } 1, node(X).
:- not 1 { in(_,X) } 1, node(X).

#minimize { C,X,Y: in(X,Y), cost(X,Y,C) }.
コード 5

目的関数

#edge (X,Y): in(X,Y), X != s, Y != s.
:- not X < Y, in(s,X), in(Y,s).
コード 4

cost(Y,X,C) :- cost(X,Y,C).
コード 6

acyclicity 符号化与えられた無向グラフの各辺 edge(X,Y) に対

補助ルール:- not #sum { C,X,Y: in(X,Y), cost(X,Y,C) } c.

して，in(X,Y) と in(Y,X) を導入し，二つの弧

X→Y と Y→X のうち高々1 個がハミルトン閉路に

コード 7

コスト制約

含まれることを個数制約を使って表している．

• 次数制約は 2–3 行目のルールで表される．2 行

号化については，無向グラフの各辺 edge(X,Y) に対目のルールは，各頂点 node(X) の出次数が 1 にして，2 つの弧 in(X,Y) と in(Y,X) を導入している．

等しいことを表している．同様に，3 行目のルー

そのため，#minimize 宣言に加えて，コード 6 の補

ルは入次数が 1 に等しいことを表す．

助ルールを追加する必要がある．

• 連結制約は，directed 符号化と同様に，補助ア
トム reached/1 を使って表される (5–7 行目)．

4. 6 コスト制約付きハミルトン閉路問題• 有向グラフ化した場合，無向グラフ上の各ハミコスト制約付きハミルトン閉路問題は，ハミルトンルトン閉路に対して，右回りと左回りの 2 つの閉路問題に，距離の総和が所与の閾値以下であるこ

対称なハミルトン閉路が存在する．9 行目のルーとを制約条件として付加した問題である．この問題

ルは，この対称解を除去する制約である．

の ASP 符号化は，ハミルトン閉路問題の undirected,

directed, acyclicity 符号化に，コード 7 のルールを追
4. 4 acyclicity 符号化

加することで実現できる．コード中の c は閾値を表

acyclicity 符号化は，directed 符号化をベースに，連し，実際の値は実行時に与えられる．また，最短ハ

結制約を部分閉路を禁止する制約に置き換えたものでミルトン閉路問題の場合と同じ理由で，directed とある．コード 4 に，acyclicity 符号化を示す．directed

acyclicity 符号化については，アトム cost/3 に関す符号化との違いは，5 行目だけである．

る補助ルール (コード 6) も追加する必要がある．

• 5 行目のルールは，始点 s を含まない弧 in(X,Y)の集合をもつ有向グラフが閉路を含まないこと

5 実行実験

を，clingo の#edge 宣言を使って簡潔に表して考案した 3 つの符号化の性能を評価するために実いる．

行実験を行った．実験に使用したベンチマーク問題は以下の通りである．

4. 5 最短ハミルトン閉路問題• ハミルトン閉路問題 (1,001 問)

最短ハミルトン閉路問題の ASP 符号化は，これまFlinders Hamiltonian Cycle Project (FHCP) でで説明した各符号化に，目的関数を追加することで実公開されている HCP インスタンス (全 1,001 問)現できる．undirected 符号化の場合は，コード 5 のを使用した [5]．この問題集は FHCP Challenge

ルールを追加すればよい．この#minimize 宣言は，ハと呼ばれる国際競技会で使用された頂点数が 66

ミルトン閉路に含まれる各辺 X – Y の距離 C の総和を個から 9,528 個の HCP インスタンスで構成され最小化することを意味する．directed と acyclicity 符ている．すべてのインスタンスはハミルトン閉路

の優位性が確認できる．
図 4 に，カクタスプロットを示す．縦軸は問題を解くのに要した CPU 時間 (秒)，横軸は解けた問題数を表す．グラフが右によるほど多くの問題を解けたことを示し，下によるほどより速く解けたことを示す．
図 4 より，directed 符号化が，他の 2 つの符号化と比較して，より多くの問題を高速に解いていることが確認できる．
今回の実験では，ASP システム clingo のオプショ
ンは trendy を使用し，1 問あたりの時間制限は 30 分
図4ハミルトン閉路問題: カクタスプロットとした．また，directed と acyclicity 符号化について
は，個数制約の上限 (コード 3 と 4 の 1 行目) を省略が存在する SAT インスタンスである．

したものを使用した．

• 最短ハミルトン路問題 (7 問)
図 1 に示した米国本土 48 州の隣接グラフに基づ

5. 2 最短ハミルトン路問題

く問題インスタンス (1 問) と，2N + 1 次の正方

表 2 に，最短ハミルトン路問題について，各符号化

グリッドグラフに基づく問題インスタンス (6 問，で得られた目的関数の値を示す．ASP システム clingo

3 ≤ N ≤ 8) を使用した．グリッドグラフの辺ののオプションは trendy を使用し，1 問あたりの時間

重みはランダムに生成した．

制限は 3 時間とした．各問題ごとに，最も良かった値• コスト制約付きハミルトン路問題 (全列挙)をボールド体で示している．*マークは，最適値を表

図 1 に示した米国本土 48 州の隣接グラフに基している．最適値と最良値の数は，undirected 符号化づく問題インスタンスを使用した．コード 7 にが 5 問，directed 符号化が 3 問，acyclicity 符号化が 3示したコスト制約の閾値 c として，最短距離問であり，undirected 符号化が 2 問ではあるが，他の(11,698 マイル) の N 倍となる 10 個の値，N =符号化より精度の高い解を生成した．grid6 と US48

1.00, 1.01, 1.02, 1.05, 1.1, 1.2, 1.3, 1.4, 1.5, 1.6 をについては，3 つの符号化すべてで最適値を得ること使用した．

ができた．最適値を得るのに要した CPU 時間は，最ASP システムには，clingo のバージョン 5.5.0 を使用し，実験環境は Mac OS (Intel Core i7 3.2GHzも速かった undirected 符号化で，grid6 は 1.451 秒，

US48 は 6.68 秒であった．

64GB メモリ) である．
5. 3 コスト制約付きハミルトン路問題
5. 1 ハミルトン閉路問題

表 3 に，図 1 に示した米国本土 48 州の隣接グラ

表 1 に，ハミルトン閉路問題の解けた問題数を示

フに基づくコスト制約付きハミルトン路問題についす．左から，HCP インスタンスの頂点数の範囲，問て，各符号化が解の全列挙に要した CPU 時間 (秒)

題数，各符号化で解けた問題数を示している．各範を示す．ASP システム clingo のオプションは crafty

囲において，最もよい結果をボールド体で示していを使用し，1 問あたりの時間制限を 3 時間とした．

る．解けた問題数は，undirected 符号化が 715 問，

表の 1 列目はコスト制約の閾値と最短距離からの倍

directed 符号化が 875 問，acyclicity 符号化が 473 問

率，2 列目は解の総数を表している．各閾値ごとに，であり，directed 符号化がもっとも多くの問題を解い最も良かった値をボールド体で示している．表より，た．directed 符号化は，どの頂点数の範囲においてもacyclicity 符号化が，他の符号化と比較して，より多他の符号化と同じかより多くの問題を解いており，そくの問題を高速に解いていることがわかる．また，平頂点数
0 ≤ |V | < 1000
1000 ≤ |V | < 2000
2000 ≤ |V | < 3000
3000 ≤ |V | < 4000
4000 ≤ |V | < 5000
5000 ≤ |V | < 6000
6000 ≤ |V | < 7000
7000 ≤ |V | < 8000
8000 ≤ |V | < 9000
9000 ≤ |V | < 10000
合計
表1

問題名
grid6
grid8
grid10
grid12
grid14grid16US48
最適値または最良値の数
表2

undirected
156
120
125
104
92
63
39
12
2
2
715

directed
171
158
162
148
104
68
43
14
5
2
875

acyclicity
155
124
73
42
28
23
21
5
1
1
473

ハミルトン閉路問題: 解けた問題数

頂点数
49
81
121
169
225
289
48

辺数
84
144
220
312
420
544
105

undirected*68,656
113,250
172,703
231,278
317,617421,249*11,698
5

directed*68,656
113,335
174,861
236,211316,347
421,696*11,6983acyclicity*68,656
113,186
172,759
233,657
318,419
422,963*11,6983

最短ハミルトン路問題: 得られた目的関数の値

閾値 (倍率)11698(1.00)
11814(1.01)
11931(1.02)
12282(1.05)
12867(1.10)
14037(1.20)
15207(1.30)
16377(1.40)
17547(1.50)
18716(1.60)
平均 CPU 時間
表3

問題数
171
165
177
185
128
80
55
28
10
2
1001

解の総数
1
8
28
388
16,180939,209
4,525,541
6,702,964
6,876,526
6,876,928

undirected
2.979
5.587
3.243
10.003
16.54848.26288.17299.15495.39098.93746.8275

directed
7.531
15.32218.60019.81828.55540.71755.27647.64745.26549.13832.7869

acyclicity
4.586
5.250
3.578
6.296
9.764
26.83742.03740.64038.41140.74821.8147

コスト制約付きハミルトン路問題: 解の全列挙に要した CPU 時間 (秒)均 CPU 時間も最も短い．

考案した 3 つの符号化の有効性を評価するために，

Flinders Hamiltonian Cycle Project (FHCP) で公

6 おわりに開されているハミルトン閉路問題の問題集 (全 1001

本稿では，解集合プログラミング (ASP) を用いた問) を用いた実験を行った．その結果，directed 符号

ハミルトン閉路問題，最短ハミルトン閉路問題，コス化が，875 問と最も多くの問題を解き，他の符号化とト制約付きハミルトン閉路問題の解法について述べ

比較してその優位性が確認できた．

た．ハミルトン閉路問題を解く ASP 符号化として，本研究で使用したハミルトン閉路問題の問題集は，

undirected，directed，acyclicity の 3 つを考案し，ハ2015 年から 2016 年にかけて行われた FHCP Chal-

ミルトン閉路問題および関連問題の制約を，ASP の

lenge と呼ばれる国際競技会 [5] で使用されたもので

ルール 10 個程度で簡潔に表現できることを確認した．

ある．この競技会では，整数計画ソルバー CPLEX

を使用した手法 [3] が 985 問を解き優勝した．2 位となった SAT ソルバーを使用した手法は 614 問を解いた [9]．3 位から 5 位の解けた問題数はそれぞれ，

488 問，464 問，385 問であった．よって，875 問を解いた directed 符号化は，ASP のルール 10 個程度の簡潔なプログラムであるにもかかわらず，実質 2 位の成績に相当する．
今後の課題としては，ハミルトン閉路問題の緩和
問題と CEGAR (Counterexample Guided Abstrac-

tion Reﬁnement) を用いた解法 [13] [16] を応用した提案手法の高速化，巡回セールスマン問題への拡張などが挙げられる．
ハミルトン閉路問題は代表的な NP 完全問題であり，また重要な工学的応用が数多く存在するため，その解法については古くから盛んに研究されている．本
研究と関連の深いものとしては，SAT ソルバーを用いた解法 [12] [14] [13]，整数計画ソルバーを用いた解法 [15] がある．これらや FHCP Challenge の上位ソ
ルバー [3] [9] との比較も重要な今後の課題である．
参 考 文 献[ 1 ] Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving, Cambridge
University Press, 2003.
[ 2 ] Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B., and Schaub, T.: Answer set programming modulo acyclicity, Fundamenta Informaticae,
Vol. 147, No. 1(2016), pp. 63–91.
[ 3 ] Cohen, N. and Coudert, D.: Le déﬁ des 1001
graphes, Interstices, (2017).
[ 4 ] 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.
[ 5 ] Haythorpe, M.: FHCP challenge set: The ﬁrst
set of structurally diﬃcult instances of the hamiltonian cycle problem, Bulletin of the Institute of
Combinatorics and its Applications, Vol. 83(2018),
pp. 98–107.
[ 6 ] 平田富夫: アルゴリズム設計とデータ構造, サイエ
ンス社, 2015.
[ 7 ] 湊真一, 番原睦則, 堀山貴史, 川原純, 瀧川一学, 山
口勇太郎: コスト制約つき組合せ問題に対する ZDD を用いた高速な解列挙手法, 信学技報, Vol. 120, No. 276,
電子情報通信学会, 2020, pp. 8–15.
[ 8 ] 井上克巳, 坂間千秋: 論理プログラミングから解集合
プログラミングへ, コンピュータソフトウェア, Vol. 25,

No. 3(2008), pp. 20–32.
[ 9 ] Johnson, A.: Stedman and Erin Triples encoded
as a SAT Problem, 2018.
[10] Knuth, D. E.: The Art of Computer Programming: Bitwise Tricks & Techniques; Binary Decision Diagrams, Vol. 4, Fascicle 1, Addison-Wesley
Professional, 2009.
[11] 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.
[12] Prestwich, S. D.: SAT problems with chains ofdependent variables, Discret. Appl. Math., Vol. 130,
No. 2(2003), pp. 329–350.
[13] Soh, T., Berre, D. L., Roussel, S., Banbara, M.,
and Tamura, N.: Incremental SAT-based Methodwith Native Boolean Cardinality Handling for the
Hamiltonian Cycle Problem, Proceedings of the 14th
European Conference on Logics in Artiﬁcial Intelligence (JELIA 2014), LNAI 8761, Springer, 2014,
pp. 684–693.
[14] Velev, M. N. and Gao, P.: Eﬃcient SAT Techniques for Relative Encoding of Permutations with
Constraints, Proceedings of the 22nd Australasian
Joint Conference on Artiﬁcial Intelligence, LNCS,
Vol. 5866, Springer, 2009, pp. 517–527.
[15] 沼田一道: 汎用 MIP ソルバによる巡回セールスマン問題の求解 : 多項式オーダ本数の部分巡回路除去制
約, オペレーションズ・リサーチ : 経営の科学, Vol. 56,
No. 8(2011), pp. 452–455.
[16] 宋 剛 秀, 鍋 島 英 知, 番 原 睦 則, 田 村 直 之, 井 上 克
巳: CEGAR と反例の共有を用いた SAT 型 CSP ソ
ルバーの並列化方法の考察, 人工知能基本問題研究会,
Vol. 112(2020), pp. 6–11.