回答セットプログラミング( ASP ) は、困難な (主にNP 困難)検索問題を対象とした宣言型プログラミングの一種です。これは、論理プログラミングの安定モデル(回答セット) セマンティクスに基づいています。ASP では、検索問題は安定モデルの計算に簡略化され、回答セット ソルバー(安定モデルを生成するプログラム) を使用して検索が実行されます。多くの回答セット ソルバーの設計で採用されている計算プロセスは、 DPLL アルゴリズムの拡張であり、原則として常に終了します (無限ループにつながる可能性があるPrologクエリ評価とは異なります)。
より一般的な意味では、ASPには、知識表現と推論への回答セットのすべての応用[1] [2]と、これらの応用で生じる問題を解決するためのPrologスタイルのクエリ評価の使用が含まれます。
歴史
解答セットプログラミングの初期の例としては、1997 年に Dimopoulos、Nebel、Köhler が提案した計画手法が挙げられます。 [3] [4]彼らのアプローチは、計画と安定したモデルの関係に基づいています。[5] 1998 年に Soininen と Niemelä [6] は、現在解答セットプログラミングとして知られている手法を製品構成 の問題に適用しました。[4] 1999 年に、「解答セットプログラミング」という用語は、2 つの論文集のタイトルとして、The Logic Programming Paradigm という書籍に初めて登場しました。 [4]これらの論文の最初の論文では、検索に解答セットソルバーを使用することを新しいプログラミングパラダイムとして特定しました。[7]同年、Niemelä は「安定したモデルセマンティクスを持つロジックプログラム」も新しいパラダイムとして提案しました。[8]
回答セット プログラミング言語 AnsProlog
Lparse は、もともと解答集合ソルバー smodels の基礎ツール (フロントエンド)として作成されたプログラムの名前です。Lparse が受け入れる言語は現在、AnsProlog [9]と呼ばれています。これはAnswer Set Programming in Logicの略です。[10]現在、assat、clasp、cmodels、gNt、nomore++、pbmodels など、他の多くの解答集合ソルバーでも同じように使用されています。(dlv は例外です。dlv 用に書かれた ASP プログラムの構文は多少異なります。)
AnsPrologプログラムは以下の形式の規則から構成される。
<ヘッド> :- <ボディ> .
が空の場合、シンボル:-("if") は省略されます。このようなルールは、ファクト<body>と呼ばれます。最も単純な種類の Lparse ルールは、制約のあるルールです。
この言語に含まれるもう一つの便利な構成要素は選択です。例えば、選択ルール
{ p 、q 、r }。
は、安定モデルに含める原子を任意に選択する、と述べている。この選択規則を含み、他の規則を含まないLparseプログラムには、8つの安定モデル(の任意のサブセット)があります。安定モデルの定義は、選択規則を含むプログラムに一般化されました。[11]選択規則は、安定モデル意味論の下では命題式 の省略形としても扱うことができます。[12] たとえば、上記の選択規則は、3つの「排中律」式の連言の省略形として見ることができます。
Lparseの言語では、次のような「制約付き」選択ルールを書くこともできます。
1 { p 、q 、r } 2.
この規則は、少なくとも1つの原子を選択するが、2つを超えてはならないとしています。安定モデル意味論におけるこの規則の意味は、命題式によって表されます。
カーディナリティ境界はルール本体でも使用できます。次に例を示します。
:- 2 { p 、q 、r }。
この制約をLparseプログラムに追加すると、少なくとも2つの原子を含む安定モデルが除去されます。この規則の意味は、命題式で表すことができます。
変数(Prologのように大文字で表記)は、Lparseでは同じパターンに従うルールの集合を省略したり、同じルール内のアトムの集合を省略したりするために使われます。例えば、Lparseプログラム
p ( a ). p ( b ). p ( c ).
q ( X ) :- p ( X ), X ! = a .
と同じ意味を持つ
p ( a ) 。p ( b ) 。p ( c ) 。q
( b ) 。q ( c ) 。
プログラム
p ( a ). p ( b ). p ( c ).
{ q ( X ):- p ( X )} 2.
は、
p ( a ). p ( b ). p ( c ).
{ q ( a ), q ( b ), q ( c )} 2.
範囲は次の形式になります。
(開始..終了)
ここで、startとendは定数の算術式です。範囲は主に数値ドメインを互換性のある方法で定義するために使用される表記上のショートカットです。たとえば、
(1..3 )です。
のショートカットです
a ( 1 ). a ( 2 ). a ( 3 ).
範囲は、同じセマンティクスを持つルール本体でも使用できます。
条件リテラルの形式は次のとおりです。
p ( X ) : q ( X )
の拡張qが である場合{q(a1), q(a2), ..., q(aN)}、上記の条件は、条件の代わりに と書くことと意味的に同等です{p(a1), p(a2), ..., p(aN)}。たとえば、
q ( 1..2 ).
a :- 1 { p ( X ) : q ( X )}.
は、
q ( 1 ). q ( 2 ).
a :- 1 { p ( 1 ), p ( 2 )}.
安定したモデルの生成
ファイルに保存されているLparseプログラムの安定モデルを見つけるには、次の${filename}コマンドを使用します。
% lparse ${ファイル名} | smodels
オプション0は、smodelsにプログラムの安定モデルをすべて見つけるように指示します。たとえば、ファイルにtest次のルールが含まれている
場合
1 { p 、q 、r } 2.
s :- pではない 。
コマンドは出力を生成する
% lparse test | smodels 0回答: 1安定モデル: qp回答: 2安定モデル: p回答: 3安定モデル: rp回答: 4安定モデル: qs回答: 5安定モデル: rs回答: 6安定モデル: rqs
ASPプログラムの例
グラフの色付け
グラフの-色付けは、隣接する頂点のすべてのペアに対してとなる関数です。ASP を使用して、指定されたグラフの - 色付けを見つけます (または、それが存在しないことを確認します)。
これは、次の Lparse プログラムを使用して実現できます。
c ( 1. . n )。
1 { color ( X , I ) : c ( I )} 1 :- v ( X ).
:- color ( X 、I )、 color ( Y 、I )、 e ( X 、Y )、 c ( I )。
1 行目では、数字を色として定義しています。2 行目の選択ルールに従って、各頂点に一意の色を割り当てる必要があります。3 行目の制約により、頂点と頂点を接続するエッジがある場合 、頂点と頂点に同じ色を割り当てることが禁止されます。
このファイルを の定義と組み合わせると、例えば
v ( 1..100 )。 % 1 , ...,100 は頂点
e ( 1 , 55 )。 % 1 から 55 までの辺が存在します
。
コマンドラインで の数値を指定して smodels を実行すると、 smodels の出力内の形式のアトムはの -色付けを表します。
この例のプログラムは、単純な ASP プログラムでよく見られる「生成とテスト」の構成を示しています。選択ルールは、「潜在的なソリューション」のセット、つまり、指定された検索問題に対するソリューションのセットの単純なスーパーセットを記述します。その後に制約が続き、受け入れられない潜在的なソリューションをすべて排除します。ただし、smodels やその他の回答セット ソルバーによって使用される検索プロセスは、試行錯誤に基づくものではありません。
大きな派閥
グラフ内のクリークは、隣接する頂点のペアの集合です。次の Lparse プログラムは、指定された有向グラフ内のサイズのクリークを見つけるか、クリークが存在しないことを判定します。
n { in ( X ) : v ( X ) }。
:- ( X )、( Y )において、X ! = Yであり、e ( X , Y )ではない。
これは、生成とテストの構成の別の例です。行 1 の選択ルールは、頂点で構成されるすべてのセットを「生成」します。行 2 の制約は、クリークではないセットを「除去」します。
ハミルトンサイクル
有向グラフのハミルトン閉路は、グラフの各頂点を 1 回だけ通過する閉路です。次の Lparse プログラムを使用すると、与えられた有向グラフにハミルトン閉路が存在するかどうかを調べることができます。0 は頂点の 1 つであると仮定します。
{ in ( X , Y )} :- e ( X , Y )。
:- 2 { in ( X , Y ) : e ( X , Y ) }, v ( X ).
:- 2 { ( X 、Y )において: e ( X 、Y ) }、v ( Y )。
r ( X ) :- ( 0 , X )において、 v ( X )。
r ( Y ) :- r ( X )、 ( X , Y )において、 e ( X , Y )。
:- r ( X )、v ( X )ではありません 。
1 行目の選択ルールは、エッジ セットのすべてのサブセットを「生成」します。3 つの制約は、ハミルトン サイクルではないサブセットを「除去」します。最後の制約は、補助述語(「0 から到達可能」) を使用して、この条件を満たさない頂点を禁止します。この述語は、6 行目と 7 行目で再帰的に定義されます。
このプログラムは、より一般的な「生成、定義、テスト」の構成の例です。このプログラムには、すべての「悪い」潜在的な解決策を排除するのに役立つ補助述語の定義が含まれています。
依存関係の解析
自然言語処理では、依存関係に基づく解析はASP問題として定式化できます。[13] 次のコードは、ラテン語の文「Puella pulchra in villa linguam latinam discit」(かわいい女の子が別荘でラテン語を学んでいる)を解析します。構文木は、文の単語間の依存関係を表すアーク述語によって表現されます。計算された構造は、線形順序付けされたルート付き木です。
% ********** 入力文 **********
単語( 1 , puella )。 単語( 2 、 プルクラ)。 単語( 3 , in )。 ワード( 4 、 ヴィラ)。 単語( 5 、 リングアム)。 単語( 6 、 ラテン語)。 ワード( 7 、 discit )。
% ********** レキシコン **********
1 { ノード( X , attr ( pulcher , a , fem , nom , sg ));
node ( X , attr ( pulcher , a , fem , abl , sg )) } 1 :- word ( X , pulchra )。
node ( X , attr ( latinus , a , fem , acc , sg )) :- word ( X , latinam )。
1 { ノード( X 、 attr ( puella 、 n 、 fem 、 nom 、 sg ));
ノード( X 、 attr ( puella 、 n 、 fem 、 abl 、 sg )) } 1 :- word ( X 、 puella )。
1 { ノード( X 、 attr (ヴィラ、 n 、 fem 、 nom 、 sg ));
ノード( X 、 attr (ヴィラ、 n 、 fem 、 abl 、 sg )) } 1 :- 単語( X、 villa )。
node ( X 、 attr ( linguam 、 n 、 fem 、 acc 、 sg )) :- word ( X 、 linguam )。
node ( X 、 attr ( discere 、 v 、 pres 、 3 、 sg )) :- word ( X 、 discit )。
node ( X 、 attr ( in 、 p )) :- word ( X 、 in )。
% ********** 構文規則 **********
0 { arc ( X 、 Y 、 subj ) } 1 :- node ( X 、 attr ( _ 、 v 、 _ 、 3 、 sg )), node ( Y 、 attr ( _ 、 n 、 _ 、 nom 、 sg )).
0 { arc ( X , Y , dobj ) } 1 :- node ( X , attr ( _ , v , _ , 3 , sg )), node ( Y , attr ( _ , n , _ , acc , sg )).
0 { arc ( X , Y , attr ) } 1 :- node ( X , attr ( _ , n , 性別, 大文字と 小文字, 数値)), node ( Y , attr ( _ , a , 性別, 大文字と 小文字 )、 Number )).
0 { arc ( X 、 Y 、 prep ) } 1 :- node ( X 、 attr ( _ 、 p )), node ( Y 、 attr ( _ 、 n 、 _ 、 abl 、 _ )), X < Y 。
0 { arc ( X 、 Y 、 adv ) } 1 :- node ( X 、 attr ( _ 、 v 、 _ 、 _ 、 _ )), node ( Y 、 attr ( _ 、 p )), not leaf ( Y )。
% ********** グラフの treeness を保証する **********
1 { root ( X ) : node ( X 、 _ ) } 1.
:- arc ( X 、 Z 、 _ )), arc ( Y 、 Z 、 _ ), X ! = Y 。
:- arc ( X , Y , L1 )、 arc ( X 、 Y 、 L2 )、 L1 ! = L2 。
path ( X 、 Y ) :- arc ( X 、 Y 、 _ )。
path ( X 、 Z ) :- arc ( X 、 Y 、 _ )、 path ( Y 、 Z )。
:- path ( X 、 X )。
:- root ( X )、 node ( Y, _ )、 X ! = Yであり、 path ( X 、Y ) ではありません。leaf ( X ) :- node ( X 、_ ) であり、arc ( X 、_ 、_ )ではありません。
言語標準化とASP競争
ASP標準化ワーキンググループは、ASP-Core-2と呼ばれる標準言語仕様を作成しました。 [14]最近のASPシステムはこれに向かって収束しています。ASP-Core-2は、回答セットプログラミングコンペティションの参照言語であり、このコンペティションでは、ASPソルバーがいくつかの参照問題に対して定期的にベンチマークされます。
実装の比較
smodels などの初期のシステムでは、バックトラッキングを使用してソリューションを探していました。ブール SAT ソルバーの理論と実践が進化するにつれて、ASSAT や Cmodels などの多くの ASP ソルバーが SAT ソルバー上に構築されました。これらは ASP 式を SAT 命題に変換し、SAT ソルバーを適用して、ソリューションを ASP 形式に戻しました。Clasp などの最近のシステムでは、ブール論理形式に完全に変換せずに、SAT にヒントを得た競合駆動型アルゴリズムを使用するハイブリッド アプローチを使用しています。これらのアプローチにより、以前のバックトラッキング アルゴリズムに比べてパフォーマンスが大幅に向上し、多くの場合、桁違いに向上します。
Potassco プロジェクトは、clasp、グラウンディング システム ( gringo )、増分システム ( iclingo )、制約ソルバー ( clingcon )、アクション言語から ASP コンパイラー ( coala )、分散メッセージ パッシング インターフェイス実装 ( claspar ) など、以下の多くのシステムを統括する役割を果たします。
ほとんどのシステムは変数をサポートしていますが、それは間接的にしかサポートしておらず、Lparseやgringoなどのグラウンディングシステムをフロントエンドとして使用して強制的にグラウンディングしています。グラウンディングの必要性は、節の組み合わせ爆発を引き起こす可能性があります。そのため、オンザフライグラウンディングを実行するシステムが有利になる可能性があります。[15]
Galliwaspシステム[16]やs(CASP) [17]などの回答セットプログラミングのクエリ駆動型の実装では、解決とコインダクションの組み合わせを使用することでグラウンディングを完全に回避します。
参照
参考文献
- ^ Baral, Chitta (2003).知識表現、推論、宣言的問題解決。ケンブリッジ大学出版局。ISBN 978-0-521-81802-5。
- ^ Gelfond, Michael (2008)。「Answer sets」。van Harmelen, Frank、Lifschitz, Vladimir、Porter, Bruce (編)。Handbook of Knowledge Representation。Elsevier。pp . 285–316。ISBN 978-0-08-055702-1。PDFとして2016年3月3日にWayback Machineにアーカイブされました
- ^ Dimopoulos, Y.; Nebel, B .; Köhler, J. (1997). 「非単調論理プログラムにおける計画問題の符号化」。Steel, Sam; Alami, Rachid (編)。AI 計画の最近の進歩: 第 4 回ヨーロッパ計画会議、ECP'97、トゥールーズ、フランス、1997 年 9 月 24 ~ 26 日、議事録。コンピュータ サイエンスの講義ノート: 人工知能の講義ノート。第 1348 巻。Springer。273 ~ 285 ページ。ISBN 978-3-540-63912-1。追記
- ^ abc Lifschitz, Vladimir (2008 年 7 月 13 日). 「回答セットプログラミングとは何か?」(PDF) .第 23 回人工知能全国会議議事録. 3 . AAAI プレス: 1594–1597.
- ^ Subrahmanian, VS; Zaniolo, C. (1995). 「安定したモデルと AI 計画ドメインの関係」。Sterling, Leon (編)。論理プログラミング: 第 12 回国際論理プログラミング会議の議事録。MIT プレス。pp. 233–247。ISBN 978-0-262-69177-2。追記
- ^ Soininen, T.; Niemelä, I. (1998)、「選択肢付きルールを使用した構成知識の形式化(追記)」、ヘルシンキ工科大学情報処理科学研究所
- ^ Marek, V.; Truszczyński, M. (1999 年 5 月 20 日)。「安定したモデルと代替ロジック プログラミング パラダイム」。Apt , Krzysztof R. (編)。ロジック プログラミング パラダイム: 25 年の展望( PDF)。Springer。pp. 169–181。arXiv : cs/ 9809032。ISBN 978-3-540-65463-6。
- ^ Niemelä, I. (1999 年 11 月). 「制約プログラミングパラダイムとしての安定したモデルセマンティクスを備えた論理プログラム」(Postscript、gzip 形式) . Annals of Mathematics and Artificial Intelligence . 25 (3/4): 241–273. doi :10.1023/A:1018930122475. S2CID 14465318.
- ^ Crick, Tom (2009). スーパー最適化: 回答セットプログラミングを使用した証明可能な最適コード生成(PDF) (Ph.D.). バース大学。Docket 20352。2016-03-04のオリジナル(PDF)からアーカイブ。2011-05-27に取得。
- ^ ロジェリオ・ダヴィラ。 「AnsProlog、概要」(PowerPoint)。
- ^ Niemelä, I.; Simons, P.; Soinenen, T. (2000)。「重み制約ルールの安定モデル意味論」。Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald (編)。論理プログラミングと非単調推論: 第 5 回国際会議、LPNMR '99、米国テキサス州エルパソ、1999 年 12 月 2 ~ 4 日議事録。コンピュータ サイエンスの講義ノート: 人工知能の講義ノート。第 1730 巻。Springer。pp. 317 ~331。ISBN 978-3-540-66749-0。追記
- ^ Ferraris, P.; Lifschitz, V. (2005 年 1 月). 「ネストされた式としての重み制約」.論理プログラミングの理論と実践. 5 (1–2): 45–74. arXiv : cs/0312045 . doi :10.1017/S1471068403001923. S2CID 5051610.追記
- ^ 「依存関係の解析」。2015年4月15日時点のオリジナルよりアーカイブ。2015年4月15日閲覧。
- ^ 「ASP-Core-2 入力言語仕様」(PDF) 。2018年5 月 14 日閲覧。
- ^ Lefèvre, Claire; Béatrix, Christopher; Stéphan, Igor; Garcia, Laurent (2017 年 5 月). 「ASPeRiX、回答セット コンピューティングのための 1 次順方向連鎖アプローチ」.論理プログラミングの理論と実践. 17 (3): 266–310. arXiv : 1503.07717 . doi :10.1017/S1471068416000569. ISSN 1471-0684. S2CID 2371655.
- ^ Marple, Kyle.; Gupta, Gopal. (2012). 「Galliwasp: 目標指向の回答セット ソルバー」。Albert, Elvira (編)。ロジック ベースのプログラム合成と変換、第 22 回国際シンポジウム、LOPSTR 2012、ベルギー、ルーベン、2012 年 9 月 18 ~ 20 日、改訂版選定論文。Springer。pp. 122 ~ 136。
- ^ Arias, J.; Carro, M.; Salazar, E.; Marple, K.; Gupta, G. (2018). 「グラウンディングなしの制約回答セットプログラミング」。論理プログラミング の理論と実践。18 (3–4): 337–354。arXiv : 1804.11162。doi : 10.1017 / S1471068418000285。S2CID 13754645。
- ^ ab 「DLV System の会社ページ」。DLVSYSTEM srl。2011年11 月 16 日閲覧。
外部リンク
- ASP-Core-2 2.03c 入力言語仕様
- 第1回ASPシステムコンペティション
- 第2回ASPコンペティション
- 第3回ASPコンペティション
- 第4回ASPコンペティション
- カモノハシ
- Debian / Ubuntu用にパッケージ化されたさまざまな解答セットソルバー
- クラスプ回答セットソルバー
