解集合プログラミング(Answer Set Programming) 論理プログラミングの歴史とASP概要

解集合プログラミング(Answer Set Programming) 論理プログラミングの歴史とASP概要

人工知能技術の中で複雑な知識情報を構築するための論理プログラミングの参考論文である人工知能学会誌(2010.5)論理に基づく推論研究の動向の中から「解集合プログラミング」より。

1970年代初頭に開発された論理型プログラミング言語Prologは、述語論理に基づく宣言的記述と定理証明に基づく計算手続きを併せ持つ新しい人工知能言語として注目され、1980年代にはエキスパートシステム、自然言語処理、演算データベースなどに幅広く有用されている。

Prologはチューリング完全で高い計算能力を持つ一方で、そのベースとなるホーン節論理プログラムは構文上の制約や推論能力の不足により、現実の知識表現や問題解決への適用は限定的であることも明らかになっている。

こうした問題を解決するために、論理プログラミングの表現能力を拡張し、推論機能を強化するための試みが1980年代後半から数多く提案されている。その結果1990年代後半から、論理プログラミングと制約プログラミングの概念を融合した解集合プログラミング(answer set programming)の概念が確立され、現在では論理プログラミングの中心的な言語の一つになっている。

ASPの特徴と意義をまとめると次の3つが挙げられる。

一つは(a)宣言的プログラミングの実現で、ASPは知識表現言語に必要とされる宣言性(declarativeness)を具備している。論理プログラミングの概念が導入された当初は、論理と制御の分離が最大の特徴といわれたが、prologではプログラムの各型に依存した実行手順や制御子(カット)などの導入により、論理プログラミングの宣言性が犠牲にされた。これに対してASPはその宣言性を保ちつつ、ASPソルバ上で拡張言語が実装されている点がPrologとは異なる。

二つ目は(b)制約プログラミングとの融合で、ASPは従来の論理プログラミングの発展という見方もできる一方で、制約プログラミングの一種と捉えることもでき、制約充足問題の計算言語としても有用になる。論理プログラミングに制約の概念を組み込んだ枠組みとしては、制約論理プログラミング(constraint logic programming;CLP)がある。ASPはCLPとは言語発展の経緯、構文論、意味論がいずれも異なるものの、思想的には両者は接近しており、二つの枠組みを統合する試みもなされている。

三つ目は(c)プログラミング理論の発展と開発環境の整備で、ASPは論理に基づく厳格な数学的意味論を持ち、プログラムの性質や計算量に関する論理的研究が進んでいる。一方ASPソルバによるプログラミング環境も整備されており、ASPの処理系はフリーウェアとしてwebを通じて世界のユーザーに公開されている。(Clasp Answer Set Solver、DLV、DLV-Complex、Smodels、clingo, Potassco, 等)

ASPの最新の動向としてはプログラム中にさまざまな制約を記述する言語拡張が行われたり、セマンティックwebにおけるオントロジーを記述するためにASPと記述論理(description logic)を融合した言語や、ASPと確率推論を融合する研究、ASPによるマルチエージェントシステムの理論なども研究されている。

まずASPが構築されてきた要因を知るため歴史的背景について述べる。

初期の論理プログラミング(logic programming)は、一階述語論理の部分クラスであるホーン節論理(Horn logic)に手続き的解釈を与えたものとして作られた。ホーン節とは以下の形式をした含意式となる。

\[\mathbf{A}\leftarrow\mathbf{A}_1,\dots,\mathbf{A}_m\quad(1)\]

(A,A1,…,Amはアトム)で、←の左側を節(1)の帰結部あるいはヘッド、右側を条件部あるいはボディと呼ぶ。ボディにおけるカンマ( 、)は連言を表す。特にヘッドが空でない確定節から構成される集合を確定論理プログラム(definite logic program)と呼ぶ。確定論理プログラムの宣言的意味論は、プログラムの最小モデル(least model)により与えられる。

van Emdenは確定論理プログラムの最小モデルが、プログラム上で定義される連続関数の最小不動点(least fixpoint)として操作的に計算可能であることを示した。また確定論理プログラムの手続き的意味論として導入されたSLD導出(resolution)は、ヘッドが空のホーン節を証明すべきゴールとみなしてプログラムに対して反論(refutation)計算を行う。確定論理プログラムの宣言的意味と手続き的意味が一致することは、最小モデルに含まれる基礎アトムの集合とSLD導出により証明される基礎アトムの集合が一致する事実により保証される。

確定論理プログラムの最小モデルに含まれる基礎アトムは、プログラムから演繹される真の事実を表す。これに対して、プログラムから演繹されない基礎アトムを偽と解釈する立場を閉世界仮説(closed world assumption:DWA)と呼ぶ。一方SLD導出による証明が有限ステップで失敗するような基礎アトムを偽と解釈する方法を失敗による否定(negation as failure;NAF)と呼ぶ。

NAFのもとで手続き的に定義される否定事実の集合は、プログラムに対して完備化(completion)と呼ばれる変換手続きを施した論理式集合から演繹的に導かれる否定事実の集合と一致する。ある基礎アトムがNAFの下で偽と解釈される場合はCWAの下でも偽と解釈されるが、その逆は一般には言えない。

CWAやNAFはプログラム中で真であることが証明できない不完全な情報を偽と解釈することで、プログラムを完全化し否定情報の推論を可能とする。一方こうしたデフォルト推論(default reasoning)は、述語論理における論理的推論とは異なる非単調推論(nonmonotonic reasoning)であるため、論理プログラミングと述語論理の間に推論規則の上で乖離が生まれる。

確定論理プログラムから否定の推論を行う論理が整うと、こうして得られる否定情報をプログラム中に知識として記述し推論の過程で利用したい。実際、prologにも節のボディにアトムの否定を条件として記述するための組み込み述語が用意されていたし、演繹データベースで二つの関係RとSの間の差を計算する場合には

\[difference_{R,S}(x_1,\dots,x_n)\leftarrow R(x_1,\dots,x_n),not\ S(x_1,…,x_n)\]

のようにボディに否定条件を記述する必要がある。一方、CWAやNAFで得られる否定はデフォルト推論の結果得られるデフォルトの否定(default negation)であり、述語論理で定義される否定とは意味が異なる。

従ってデフォルトの否定をプログラム中に陽に記述する場合、プログラムは述語論理のもとで定義される節集合とは異なるものになる。ここで、記述式の上でも論理プログラミングと述語論理の間に乖離が生じることとなる。そこで、プログラムの記述文の条件部にデフォルトの否定が出現する式

\[A\leftarrow A_1,\dots,A_m,\ notA_{m+1},\dots,notA_n\quad(2)\]

(A,A₁,…,A_nはアトム)をルールと呼び、節と区別する。ここでnotはNAFオペレータと呼ばれ、(2)の形式のルールから構成される集合を標準論理プログラム(normal logic program)と呼ぶ。プログラムの構文の拡張により、デフォルトの否定を含むプログラムの意味論を考える必要があるが、すべての基礎アトムからなる集合をAtとすると、解釈I⊆Atの下で基礎アトムAが死んでない場合、またその時に限りIの下でのnotAは真であると定義するのが自然となる。

そこで(2)の形式の基礎ルール(変数を含まないルール)に対して、解釈Iが「{A₁,…,A_m}⊆Iかつ{A_m+1,..,A_n}∩I=∅ならばA∈I」(*)という条件を満たす場合にはIはこのルールを充足すると定義する。条件(*)は「{A₁,…,A_m}⊈Iまたは{A_m+1,..,A_n}∩I=∅またはA∈I」(+)と等価である。

この結果標準論理プログラムPのモデルはPを基礎化(ground instantiation)したプログラムに含まれるすべてのルールを充足する解釈であると定義される。

確定論理プログラムの宣言的意味は最小モデルにより定義されたが、標準論理プログラムでは一般に最小モデルが存在しない、例えばプログラム

\[p\leftarrow not\ q\]

は二つの極小モデル(minimal model){p}と{q}を持つが、いずれも最小モデルではない。そこで標準論理プログラムの宣言的意味を最小モデルの代わりに極小モデルを使って定義し、一般に複数存在する極小モデルのうち、プログラムの記述文の意味を反映するものはどれかということを考える。上の例ではpはqが証明されないという条件の下で導かれている。一方、qを導くルールはプログラムには存在しない。あるアトムを導く根拠となるルールがプログラムの中に存在する時、そのアトムは支持されている(supported)という。

プログラムの意味を反映する極小モデルに含まれるすべてのアトムは、プログラムで支持されていることが必要条件になる。支持されたアトムから構成されるモデルを計算するためには、ヘッドに含まれるアトムがボディに存在するデフォルトの否定に含まれるアトムよりも上位の層にあると考え、解釈における各アトムの真偽の評価は下位の層に属するものから順番に行えれば良い。

上の例ではまずqが証明されないので偽と解釈され、その前提の下でpが真となる。この結果、二つの極小モデルのうち{p}のみが支持されたアトムから構成され、このプログラムの意味を反映したものと考えられる。この{p}を完全モデル(perfect model)と呼ぶ。

一般にはプログラム中の述語を階層に分解し、プログラムの中の任意のルール(2)について、ヘッドAに含まれる述語がデフォルトの否定中に現れるアトムA_m+1,…,A_nに含まれる述語よりも上位に含まれるような分割が可能であるようなプログラムを層状プログラム(stratified program)と呼ぶ。

層状プログラムは常に唯一の完全モデルを持ち、プログラムがデフォルトの固定を含まない場合は完全モデルは最小モデルに一致する。層状プログラムは各述語が自身のデフォルトの否定を再起的に呼び出さないようなプログラムであり、完備化が矛盾しない特徴を持つ。

標準論理プログラムにおける証明手続としてはSLD導出にNAFを組み込んだSLDNF導出がある。またプログラムの完備化が矛盾しない条件の下で、層状プログラムの構文の制約を緩和する提案もなされ、述語階層をアトムの階層に拡張した局所層状プログラム(locally stratified program)やデフォルトの否定の偶数回の再帰呼び出しを許容する呼び出し無矛盾プログラム(call-consistent program)などがある。

層状プログラムはデフォルトの否定の記述を可能にし、宣言的意味および手続的意味が明確に定義されたプログラムのクラスとなる。一方で我々が日常もっている知識や情報の中には、必ずしも相乗の否定で表現できないものもある。例えば、目覚めのためのコーヒーがなければ紅茶を飲み、紅茶が鳴けばコーヒーを飲むという状況を以下のようなプログラムPで記述したとする。

\[wake\leftarrow coffee\\wake\leftarrow tea\\tea\leftarrow not\ coffe\\coffee\leftarrow not\ tea\]

このプログラムはteaとcoffeeがそれぞれ自身のデフォルトの否定を再帰的に呼び出しているため層状プログラムではない。このような層状でないプログラムの宣言的意味を定義するために導入されたのが、安定モデル意味論(stable model semantics)となる。

今、解釈Iが与えられた時、基礎化された標準論理プログラムPに含まれる任意の基礎ルール(2)に対して(a){Am+1,…,An}∩I≠∅であるようなルールは前述の定義(+)からIにより充足されるのでPから消去し、(b)次に残ったルールに含まれるデフォルトの否定にについては{Am+1,…,An}∩I=∅tが成り立つことから、not A_m+1,…,not A_nはIにより満たされるのでこれらの否定条件をルールから消去する。

この結果得られたプログラムをP’で表すと、P’はデフォルトの否定を含まないホーン節からなる論理プログラムと同一視できる。ここで、IがP’の最小モデルと一致する時、IをPの安定モデルと呼ぶ。安定モデルの直感的な意味は、ある解釈Iに対してプログラムPからデフォルトの否定条件が満たされるようなルールの集合P’を構成し、ここでP’から導かれる事実の集合がIに一致する時、IはPの安定モデルであると考える。

上述の例ではI₁={wake,tea}としたとき、\(P{I_1}\)は

\[wake\leftarrow coffee\\wake\leftarrow tea\\tea\leftarrow\]

となる。ここでI₁は\(P{I_1}\)の最小モデルになっているので、I₁はPの安定モデルである。同様にI₂={wake,coffee}もPの安定モデルとなる。安定モデルは極小モデルであるがその逆は言えない。また層状プログラムにおいては安定モデルは完全モデルと一致する。

安定モデルは完全モデルを自然に拡張し、宣言的意味が定義されるプログラムのクラスを拡張した。一方、層状でない標準論理プログラムは複数の安定モデルをもつことがあり、また一つも持たないこともある。この事実は論理プログラムの意味論に非決定性を導入するばかりではなく、SLD導出依頼使われてきたゴール駆動型の計算手続きに限界をもたらした。

例えば以下のプログラム

\[p\leftarrow not\ q\\r\leftarrow not\ r\]

においてゴール←pはSLDNF導出に成功するが、このプログラムは安定モデルを持たない。すなわち、ゴールが成功してもそのゴールに含まれるアトムが真となる安定モデルの存在が保証されないため健全性がいえない。確定論理プログラムや層状プログラムでは、ゴール←Gがプログラムの一部のルールを使って反論されれば、Gはプログラム全体の帰結であることが保証されるが、標準論理プログラムにおける安定モデル意味論の下ではこの局所性の原理(locality principle)が成り立たない。

標準論理プログラムの意味論として、完全戻るを拡張した別のアプローチとして整礎モデル意味論(well-founded model emantics)がある。整礎モデル意味論は3値論理のもとで定義され、すべての標準論理プログラムは唯一の整礎モデルを持つことが保証される。また安定モデル意味論と異なり局所性の減速を保持するため、従来方式のゴール駆動型証明手続が有効であるというメリットもある。

一方、安定モデル意味論の元では真または偽と解釈される基礎アトムが整礎モデルの元では未定義(unknown)とされることがある。例えば、前述のコーヒーと紅茶のプログラムではどちらを飲んでも目覚めることが安定モデルの元では言えるが、整礎モデル意味論の下では、本来審議が決まるはずの基礎アトムがunknown値を取ることがあるため、安定モデルに比べて慎重(skeptial)であるといわれる(逆に安定モデルは安易(credulous)であるといわれる)。このように安定モデル意味論、整礎モデル意味論ともに一長一短があり、それらをベースに提案された意味論は、その多くが構文的に特殊なプログラムに直感的な意味を与えるため悪戯に理論を複雑にしたものとなり、今日ではほとんど使われていない。

確定論理プログラムにおける記述文は、帰結部が単一のアトムからなる確定節でなければならないが、この事実は一般に不確定な情報を記述する上での制約となる。そこでルールのヘッド部にアトムの選言を含むような非ホーン節からなる選言論理プログラム(disjunctive logic program)の枠組みが導入された。選言プログラムは以下の形式の節

\[A_1∨\dots∨A_l\leftarrow A_{l+1},\dots,A_m\quad(3)\]

(A₁,..,A_mはアトム)からなる集合となる。このとき確定論理プログラムは節(3)においてl=1であるような節のみから構成される特殊な場合であると考えられる。選言論理プログラムは一般に最小モデルは持たないため、プログラムがもつ複数の極小モデルによって宣言的意味が定義される。例えば

\[p∨q\leftarrow\]

という選言節からなるプログラムは二つの極小モデル{p}と{q}を持つ。これらの極小モデルは同等であり、プログラムの二つの可能な解釈を表現している。一方、選言論理プログラムにCWAを適用すると、CWAから得られる否定情報とプログラムが矛盾することがある。前述のプログラムではpとqはいずれもプログラムから証明されないためCWAにより¬pと¬qが推論されるが、ひれらの否定事実はプログラムの選言節と矛盾する。

こうした問題を解決するためMinkerらはCWAを拡張した一般閉世界仮説(generalized CWA:GCWA)を導入したGCWAは基礎アトムAが真となるような極小モデルが存在しない場合に限り、Aを偽と解釈するものとなる。前述の例ではpまたはqを含む極小モデルが存在するため、GCWAのもとでこれらの否定は推論されない。一方GCWAによる否定推論の問題として、例えば以下のプログラム

\[land\ animal\ ∨\ aquatic\ animal\leftarrow\\amphibian\leftarrow land\ animal,aquatic\ animal\]

は二つの極小モデル{land animal}と{aquatic animal}を持つが、amphibianを含む極小モデルが存在しないため、GDWAのもとでは¬amphibianが推論される。このように極小モデルのもとで定義されたGCWAは選言を排他的(exclusive)に解釈し、選言に含まれる複数のアトムが同時に真となる包含的(inclusive)な解釈が排除されることがある。

古典論理における選言は本来、包含的な解釈も含むため、この意味でGCWAによる推論結果は強すぎると言える。そこでGCWAを弱めて選言の包含的な解釈のもとで否定推論を行う方式としてWGCWA(weak GCWA)またはDDR(disjunctive database rule)が提案された。WGCWAではプログラムから導出される、基礎アトムからなる選言の集合に含まれないような基礎アトムの否定を推論する。上の例ではamphibian∨land_animal∨aquatic_animalがプログラムから導出されるため、ここに含まれるamphibianの否定は推論されない。

WCGWAやDDRはGCWAを緩和した否定推論を実現するが、選言の包含解釈に基づくプログラムのモデル論は提供しない。またプログラムが排他的な選言と包含的な選言を同時に含む場合はGCWAもWGCWA(DDR)も対処できない。そこで排他的な選言と包含を区別し、2種類の異なる選言を含むプログラムの宣言的意味論として可能モデル意味論(possible model semantics)が導入された。前述の例ではプログラムは三つの可能モデル{land_animal},{aquatic_animal},{land_animal,aquatic_animal,amphibian}を持つ。ここで最初の二つは極小モデルであるが、三つ目は非極小なモデルになっている。可能モデル意味論の元では排他的な選言と包含的な選言はプログラム中に記述した負例によって区別される。

例えば、カレーライスとラーメンと野菜サラダの三つのメニューがあり、このうちカレーライスとラーメンを同時に食べるのはカロリ過多のため不可という場合以下のように記述できる。

\[curry\ ∨\ noodles\ ∨\ salad\leftarrow\\\leftarrow curry,noodles\]

このモデルの可能モデルは[curry},{noodles],{salad},{curry,salsd},{noodel,salad}の五つとなる。可能モデル意味論は極小モデル意味論と比べて選言の解釈が城南に記述できるという知識表現上のメリットがあるばかりでなく、計算量も一般に低く抑えられる。確定論理プログラムでは可能モデルは最小モデルと一致する。

選言論理プログラムの記述文にデフォルトの否定を導入したものを標準選言論理プログラム(normal disjunctive logic program)と呼ぶ。標準選言論理プログラムは以下の形式のルールの集合となる。

\[A_1∨\dots∨A_l\leftarrow A_{l+1},\dots,A_m,not\ A_{m+1},\dots,not\ A_n\quad(4)\]

(A1,…,Anはアトム)の集合となる。標準選言論理プログラムの意味論としては、安定モデルと整礎モデルが拡張された意味論が提案され、このうち安定モデル意味論を拡張したものが解集合意味論へと発展していく。

選言論理プログラミングはルールのヘッドが選言を含むため、ゴール駆動による湿布ダウン型の証明手続は一般に複雑となる。そこで選言論理プログラムの極小モデル全体をモデル生成手続によりボトムアップ的に計算する手法が提案されている。この手法はのちに一般的選言プログラムの安定モデルの計算および解集合の計算手続に発展している。

標準選言プログラムにおけるnotはデフォルトの否定を意味したが、これに対して論理否定¬による明示的否定(explicit negation)をデフォルトの否定と区別して使うプログラムのクラスを拡張選言論理プログラム(extended disjunctive logic program)と呼ぶ。拡張選言プログラムは以下の形式のルール

\[L_1;\dots;L_i\leftarrow_{l+1},\dots,L_m,not\ L`{m+1},\dots,not\ L_n\quad(5)\]

の集合となる。式(4)と異なりL1,…,Lnは正負のリテラルで、セミコロン(;)は選言を表す。ルールのヘッドで∨の代わりに”;”が使われている理由は、古典論理ではp∨¬pはトートロジーであるが、拡張選言論理プログラムではルールp;¬p←はトートロジーではないため両者を異なる記号で区別している。また古典論理では論理式p←qと¬p←¬qは同値な論理式であるが、拡張選言論理プログラムでは両者は同値ではない。拡張選言論理プログラムのうち、ヘッドに選言を含まないようなルールから構成されるものを特に拡張論理プログラム(extended logic program)と呼ぶ。このように2種類の否定を区別していることにより、意味が微妙に異なる知識を表現することが可能になる。

\[cross\leftarrow not\ car\]

は車が走ってくることが認識されなければ道路を渡るという行動を表現しているのに対して

\[cross\leftarrow ¬ car\]

は車が走ってこないことを認識した上で道路を渡るという行動を表現している。両者を比較すると、プログラムからcarという肯定事実が証明できなければcrossを帰結するのが前者であるのに対し、プログラムから¬carという否定事実が証明された後にcrossを帰結するのが後者となる。

拡張選言論理プログラムでは明示的否定を使って否定事実がプログラムから直接証明されるため、証明されていない事実は否定とみなす閉世界仮説(CWA)は用いず、証明されていない事実は否定も肯定もしない開世界仮説(open world assumption;OWA)の立場がとられる。CWAはプログラム中に記述された肯定情報が完全で、それ以外の情報を否定とみなす場合に有効であるが、肯定情報が不完全でCWAを適用したくない場合にはOWAが有効となる。

拡張選言論理プログラムでは否定知識が陽に記述されるため、プログラムが矛盾する可能性がある。そこで矛盾を回避する方法として、相反する帰結を導くルールの間に優先順位を導入するもの、プログラムに含まれるルールの無矛盾な極大部分集合の解集合を計算する方法、プログラム野中に矛盾を局所化する矛盾許容論理(paraconsistent logic)に基づく形式化等がある。

拡張選言論理プログラムに含まれるルールのヘッドにデフォルトの否定の出現を許容するプログラムのクラスを一般拡張選言論理プログラム(general extended disjunctive logic programming)と呼ぶ。一般拡張選言論理プログラムは以下の形式のルール

\[L_1;\dots;L_k;not\ L_{k+1};\dots;not\  L_t leftarrow L_{t+1},\dots,L_m,not\ L_{m+1},\dots,not\ L_n\quad(7)\]

(L1,…,Lnは正負のリテラル)の集合である。一般拡張選言論理プログラムはLifschizらにより導入され、Inoueによって知識表現への応用が示された。一般拡張選言論理プログラムの意味論は、拡張選言論理プログラムの解集合を拡張することによって定義される。

一般拡張選言論理プログラムが拡張選言プログラムと異なる点は、ルール(7)のヘッドに出現するデフォルトの否定の効果により解集合が極小とは限らない点にある。例えばプログラム

\[p;not\ p\leftarrow\quad(8)\]

は二つの解集合∅と{p}を持つ、ルール(8)は解集合がアトムpを含むか含まないかという2通りの可能性を宣言的に記述しており、この形式のルールはアブダクティブ論理プログラミング(abductive logic programing)における候補仮説の表現に使えることがわかっている。

一般拡張選言論理プログラムは一般に複数の解集合を持つが、解集合の間に優先順位を導入する枠組みとして、順序付き拡張選言論理プログラム(logic prigram with ordered disjunction;LPOD)等がある。LPODは以下の形式のルール

\[L_1\times\dots\times L_l\leftarrow L_{l+1},\dots,L_m,not\ L_{m+1},\dots,not\ L_n\quad(9)\]

(L1,…,Lnは正負のリテラル)の集合で、xは順序付き選言(ordered disjunction)と呼ばれる。ルール(9)におけるL1x…xLlの意味はL1が成り立てばL1を帰結し、L1が成り立たなければL2を帰結し…といった具合となる。つまりLPODのルールにおいてはヘッドに含まれるリテラルがランク付けされ、ボディが成り立つ場合に、ヘッドの帰結のLiがLj(i>j)より優先される。

LPODを使った知識表現の例を一つ示す。以下のプログラムが与えられた時

\begin{eqnarray}&(r_1)&\quad cinema\times beach\leftarrow not\ hot\\&(r_2)&\quad beach\times cinema\leftarrow hot\\&(r_3)&\quad hot\leftarrow summer, not\ ¬hot\\&(r_4)&\quad  ¬beah\leftarrow rain\end{eqnarray}

それぞのルールの意味は、(r1)暑くなければ海に行くより映画に行くことを好み、(r2)暑ければその逆で、(r3)夏は通常暑く、(r4)雨が降れば海辺には行かないとなる。

解集合に優先順位を導入する仕組みとしてはLPODのほかに、拡張論理プログラムにおいてルール間の優先順位を指定する方法、一般拡張選言論理プログラムにおいてリテラルとデフォルト否定されたリテラルの優先関係を記述する方法などがある。

論理プログラミングによって記述された問題を、解集合意味論の下で解決する方法を解集合プログラミング(answer set programming;ASP)と呼ぶ。ASPではプログラムは問題の解決が満たすべき制約式の集合であると考えられ、プログラムの解集合が問題の解となる。

従ってASPでは与えられたプログラムの解集合を計算する手続きが必要となり、このような手続きはASPソルバと呼ばれる。典型的なASPソルバは(1)変数を含むプログラムを基礎化し、(2)基礎化されたプログラムの解集合を計算するという2段階からなる。

ASPソルバの問題点の一つは、上記(1)を有限時間で終了するためには基礎項全体の集合が有限でなければならず、関数記号が一般に使えないという制約があることである。論理プログラミング言語Prologでは関数記号は高階オブジェクトを項として表現し、関数記号の一種であるリスト記号は[・|・]は複雑なオブジェクトを再起的に定義する上でも有効であった。一方、ASPソルバでは関数記号の使用が制限されるため、問題を記述する上で従来のプログラミング方法を変える必要がある。そこでASPソルバではオブジェクトが満たすべき制約式をプログラム中に記述し、項や再帰的定義を用いて表現していたオブジェクトを解集合として表現する方法をとる。

これらの知識表現の違いを例題を使って見てみる。今、与えられた無向グラフのクリーク(無向グラフG=(V,E)におけるノードの部分集合C⊆Vのうち、Cに属する任意の二つのノードを結ぶエッジが存在する場合、Cをクリーク(clique)と呼ぶ)を求める問題を以下の確定論理プログラムで記述したとする。

\begin{eqnarray}&clique([ ])&\\&clique([x])&\leftarrow node(x)\\&clique([y|x])&\leftarrow clique(x),allconnected(y,x)\end{eqnarray}

ここで、allconected(y,x)はノードyがノードxに含まれず、かつxに含まれるすべてのノードとエッジでつながっていてxの要素に重複がない場合に真になるものとする。いまグラフGに含まれるノードとエッジの事実が

\[F=\{node(a),node(b),node(c),edge(a,b),edge(b,a),edge(b,c),edge(c,b)\}\]

として与えられた時に、上のプログラムはGに含まれるクリークを述語cliqueの引数に含まれるリスト

\[clique([ ]),clique([a]),clique([b]),clique([c]),\\clique([a,b]),clique([b,a]),clique([b,c]),clique([c,b])\]

として計算し、これらの解はプログラムの唯一の最小モデルに含まれる。

一方、ASPでは同じ問題が以下のように記述される。

\[clique(x)\leftarrow node(x),not\lnot clique(x)\\\lnot clique(x)\leftarrow node(x),not\ clique(x)\\\leftarrow clique(x),clique(y),x\neq y,not\ clique(x,y)\]

上記のプログラムの最初の二つのルールはノードをクリークに含まれるもの(clique)とそうでないもの(¬clique)に分類する。3番目のルールはクリークに含まれるノードが満たすべき条件をヘッドが空の制約(constrain)として記述している。

この制約の意味は、cliqueに含まれる二つの異なるノードxとyについてはedge(x,y)が成り立たなければいけないことを言明している。この結果、クリークを構成するノードは、解集合に含まれる述語cliqueの引数として表明され、事実Fが与えられたとき、それぞれの回はプログラムの六つの異なる解集合として計算される。

\[\{\lnot clique(a),\lnot clique(b), \lnot clique(c)\}\cup F,\\\{clique(a),\lnot clique(b), \lnot clique(c)\}\cup F,\\\{\lnot clique(a),clique(b), \lnot clique(c)\}\cup F,\\\{\lnot clique(a),\lnot clique(b), clique(c)\}\cup F,\\\{clique(a), clique(b), \lnot clique(c)\}\cup F,\\\{\lnot clique(a),clique(b), clique(c)\}\cup F\]

上記の例で見た通り、ASPではヘッドが空の制約をプログラム中に記述することによって、もとめるべき解集合を計算する。一般的には、制約

\[\leftarrow L\quad(10)\]

はLであってはならないという禁止を表現し、

\[\leftarrow not\ L\quad(11)\]

はLでなければならないという強制を表現する。制約(10)によりリテラルLを含む集合は解候補から除かれ、制約(11)によりリテラルLを含まない集合は解候補から覗かれる。ヘッドが空のルールは、論理プログラミングではKowalskiらによるプログラムの手続的解釈に従って問合せを表現するゴールとして用いられ、演繹データベースやアブダクティブ論理プログラミングにおける一貫性制約(integrity constraint)として導入された経緯はあるが、プログラム中に記述されて推論の過程で用いられるようになったのはASPによる知識表現がポピュラーになってからである。

計算量の観点からは、有限の基礎ルールから構成される標準論理プログラムが安定モデルをもつかどうかの決定問題はNP完全である。このことからNPのクラスに属する決定問題は原理的に変数を含まない標準論理プログラムで記述でき、決定問題の解の存在はプログラムの安定モデルの存在判定に帰着することができる。

ASPソルバが開発されASPがプログラミング言語として問題解決に利用されるようになると、プログラムをコンパクトに記述し、問題を効率的に処理するためのASP言語の構文の拡張が行われるようになった。以下で、現在ASPで採用されている代表時な言語拡張について述べる。

SMODELSは標準論理プログラムの安定モデルを計算するシステムで、その構文の中で個数制約(cardinarity constrait)と呼ばれる以下の式が採用されている。

\[U\{A_1,\dots,A_m,not\ A_{m+1},\dots,not\ A_n\}\quad(12)\]

ここで、各A_iはアトムで式(12)の意味は、A₁,…,A_m, not A_m+1,…,not A_nのうちモデルによって充足されるものの個数がU以上V以下という意味となる。こで、上限あるいは下限が存在しない場合は、それぞれVあるいはUが省略されることもある。この個数制約をルールを記述するアトムのかわりに用いる。例えば、ルール

\[1\{p,\}\leftarrow\{r,s,not\ t\}\]

はボディに含まれるr,s,not tのうち二つ以上が成り立てば、ヘッドに含まれるp,qのうち少なくとも一つが成り立つという意味になる。またアトムが変数を含む場合は、変数に対する条件付けを行う。例えば

\[\{clique(x)\quad node(x)\}\leftarrow\]

はクリークcloqueに含まれる変数さはnode(x)であることを記述している。このとき、上式に制約

\[\leftarrow clique(x),clique(y)x\neq y,not\ edge(x,y)\]

を加えた二つのルールから構成されるプログラムは、nodeとedgeの事実が与えられた時にクリークを計算する。このプログラムを標準のASPプログミングと比較すると、記述文がコンパクトになっていることがわかる。

個数制約(12)はさらに重み付き制約(weighted constraint)と呼ばれる以下の制約式に拡張される。

\[\{A_1=\omega_1,\dots,A_m=\omega_m,not\ A_{m+1}=\omega_{m+1},\dots,not\ A_n=\omega_m\}V\quad(13)\]

ここで、各ωiはアトムAiあるいはデフォルト否定notAiの重みを表す。式(13)の意味は、A₁,…,A_m,not A_m+1,…,not A_nのうち解集合よって充足されるものの重みがU以上V以下という意味となる。個別制約(12)は重み付き制約(13)においてω1=…..=ωn=1である特殊な場合であると考えることができる。

重み付き制約を使うと標準論理プログラムのルール

\[A\leftarrow A_1,\dots,A_m,not\ A_{m+1},\dots,not\ A_n\]

は

\[1{A=1]\leftarrowm+n\{A_1=1,\dots,A_m=1,not\ A_{m+1}=1,\dots,not\ A_n=1\}\]

と解釈される。一般に以下の形式のルール

\[C\leftarrow C_1,\dots,C_m,not\ C_{m+1},\dots,not\ C_n\quad(14)\]

(C,C1,…,Cnは重み付き制約)から構成されるプログラムを重み付きプログラム(weighted program)と呼ぶ。重み付き制約の中で特に重要なのは、重み付きルール(weighted rule)と呼ばれる以下の形式のルール

\[A \leftarrow\omega\{A_1=\omega_1,\dots,A_m=\omega_m,not\ A_{m+1}=\omega_{m+1},\dots,not\ A_n=\omega_n\}\quad(15)\]

および選択ルール(choise rule)と呼ばれる以下の形式のルール

\[\{A_1,\dots,A_l\}\leftarrow A_{l+1},\dots,A_m,not\ A_{m+1}.\dots,not\ A_n\quad(16)\]

となる。重み付きルールは重み付き制約からなる条件部の下限を指定しており、選択ルールはボディの条件が成り立つ時にヘッドのアトム集合の任意の部分集合が選択されることを表現している。ルール(15)とルール(16)は基礎制約(basic constraint)と呼ばれ、重み付きプログラムのルール(14)はこれら2種類の基礎制約に変換可能である。なお個体制約や重み付き制約から構成されるルールは、適当なアトムを新たに導入することで通常の標準論理プログラムのルールに書き換えることができる。