Answer Set Programming(Draft)要約: 第1,2章

はじめに

Vladimir Lifschitz氏によるAnswer Set Programming (Draft) (リンク)の第1章第2章の要約です。輪講に利用したものをほぼそのまま流用しているので、表記がおかしかったらごめんなさい。

Clingoについて

HomebrewであればこれでOKです。

% brew install clingo

そのほかの方法はここにありますが、試していないのでやってみてください。
また、clingoのドキュメンテーションはここです。

Table of contents

• Rules
• Directives and Comments
• Arithmetric
• Definitions
• Choice Rules
• Global and Local Variablles
• Constraints
• Anonymous Variables

Rules

ルールの構成

large(C) :- size(C,S1), size(uk,S2), S1 > S2.

• 意味は「Cの大きさがS1かつukの大きさはS2かつS1 > S2ならばCは大きい」
• large(C)はhead(頭部)
• size(C,S1), size(uk,S2), S1 > S2はbody(本体)
  • :-がないルールは、bodyがないルールとして扱う。
• large(C),size(C,S1),size(uk,S2)はatom
  • 関係や性質を表すpredicate(述語) symbolとカッコ内の引数のリスト（任意）からなる
  • コンマで区切られた表現は、論理積$\wedge$と同じ
• S1>S2はcomparison
  • =, !=, <, >, <=, >=のいずれかのシンボルと、その両側の二つの引数からなる
• 引数になる表現をtermと呼ぶ
  • Symbolic constraint - 小文字から始まる文字、数字、アンダ-スコアの文字列
  • Numeric constraint - 10進数の整数
  • Variables - 大文字から始まる文字、数字、アンダースコアの文字列
  • 複雑なtermは後述
• Atomやruleなどの内、variableがないものをgroundであるといい、「事実」を示す
  • ex) size(uk,64).

Stable modelの導出

large(C) :- size(C,S1), size(uk,S2), S1 > S2.
size(uk,64).  size(france,65).

large(france)がstable modelに含まれるのは、C,S1,S2をそれぞれfrance, 65, 64に置き換えた

large(france) :- size(france,65), size(uk,64), 65 > 64.

が存在するからである

• bodyのatomは事実として与えられている
• comparisonは真である

その他ルールに関して

• p(X) :- X > 7.のような無限にstable modelが存在するようなルールは”unsafe variable”のエラーで実行できない
• size(uk,64). size(france,65).は
  size(france,65; uk,64).のように省略して書くことができる (pooling)

Directives and Comments

• #show p/2.
  • predicate symbolがpで引数が2のもの以外を表示しない
    • clingoでは、同じpredicates symbolでも引数の数が異なれば別の述語として扱う
• #const c0=uk.
  • symbolic constraint c0を定数ukに置き換える
  • コマンドラインオプション -c c0=ukも同じ
• #include “large_input.lp”.
  • 他のファイルを連結する
  • コマンドから% clingo large.lp large_input.lpも同じ
• %から行末まではコメント

Arithmetric

• 変数、定数と以下のシンボルで複雑なtermを表現できる
• +,*,**(べき乗),/(整数除算),\(除算のあまり),||(絶対値)
• -,&(bit AND),?(bit OR), ^(bit XOR), ~(bit NOT) (PDFには何故か乗っていない?)
• 0..3は集合{0,1,2,3}を示す。(interval)
  • ex) p(N,N*N+N+41) :- N = 0..2. のstable modelは
    p(0, 41) p(1, 43) p(2, 47)
    • N=0..2は$N\in{0,1,2}$を表す
  • ex) p(0..2).はp(0; 1; 2).と同じ
  • ex) p(0..2,0..1).は p(0,0; 0,1; 1,0; 1,1; 2,0; 2,1).と同じ

Definitions

• 多くのルールは定義として見ることができる

  • ex) grandparent/2はparent/2を使って次のように表現できる

      grandparent(X, Z) :- parent(X, Y), parent(Y, Z)
    

• predicateは複数の定義から成ることもある

  parent(X, Y) :- mother(X, Y).
  parent(X, Y) :- father(X, Y).
  

• predicateは再帰的に定義することができる

  ancestor(X, Y) :- parent(X, Y).
  ancestor(X, Z) :- ancestor(X, Y), ancestor(Y, Z).
  

• 1ステップで定義できないこともある

  composite(N) :- N= 1..5, I = 2..N-1, N\I=0.
  prime(N) :- N=2..5, not composite(N).
  

• notはnegation as failureを示す

  • 導出できない時に真になる
  • 言い換えれば、明示的に述語を否定することによって真になるわけではないということでもある。

Choice Rules

• ASPでは複数のstable modelが存在するものを扱うことが多い

• {p(a); q(b)}.はp(a), q(b)がそれぞれ含まれるかを選んだ全ての通りのモデルを表すルールである

  • このルールだけの場合、stable modelは$\phi$, p(a), q(b), p(a)q(b)の4通り
  • 全てのstable modelを見るためには% clingo choice.lp 0で実行

• poolingとintervalを利用することもできる

  • {p(1;2;3)}.と{p(1..3)}.は{p(1); p(2); p(3)}.と同じ

• モデルに含まれる要素の数の上限と下限を1 {p(1..3)} 2.のように定義できる

  • このルールのみのstable modelはp(1), p(2), p(3), p(1)p(2), p(1)p(3), p(2)p(3)
  • 下限や上限のみを指定することもできる
  • 下限と上限が等しい時{p(1..3)}=2.のように書ける

Global and Local variables

• Choice ruleのbodyには変数を含めることもできる(Global variables)

  • {p(X); q(X)} = 1 :- X=1..2.はp(1)かq(1)のいずれかと、p(2)とq(2)のいずれかを安定モデルに含む
  • {p(1); q(1)} = 1. {p(2); q(2)} = 1.と同じ

• Local variables はChoice ruleのカッコ内のatomを、すでに定義されているpredicateで定義したい時に利用できる

  • person/1が定義されている時、{elected(X) : person(X)} = 3.でstable modelは当選した人が3人のみになる
  • person(ann; bob; carol; dan; elaine; fred)ならば、上の式は
    {elected(ann; bob; carol; dan; elaine; fred)} = 3 と同じ

Constraints

• Headがないルールはconstraintであり、bodyを満たすmodelはstable modelとならないという制約を示す

  • :- p(1). の時、stable modelはp(1)を含まない
  • :- not p(1). の時、stable modelは必ずp(1)を含む
  • :- p(1), p(2).の時、p(1)とp(2)を両方含むmodelはstable modelにならない

• constraintは変数を含むことができる

  • :- p(X), q(X).はp/1とq/1が互いに素であることを示す（p/1とq/1を同時に満たす要素が存在しないstable modelを排除する)

• comparisonを含むこともできる

  • :- f(X, Y1), f(X, Y2), Y1 != Y2.はf/2が関数であることを示す
  • constraintのbodyのcomparisonは、headの逆のcomparisonに置き換えることができる
    • ex) Y1 = Y2 :- f(X, Y1), f(X, Y2).

Anonymous Variables

• filled/3はfilled(R, C, X)が行R列Cに値Xが入っている表を表すとする。

• R1 = R2 :- filled(R1, C1, X), filled(R2, C2, X).は同じ値は同じ行にしか入らないことを示している。

  • C1,C2は一度しか使われていない

• 上記のような一度しか登場しない変数はアンダースコアに置き換えることができる
  R1 = R2 :- filled(R1, _, X), filled(R2, _, X).

• 内部的には補助的な述語に置換されている

  R1 = R2 :- aux(R1, X), aux(R2, X).
  aux :- filled(R, Var, X).
  

  • aux/2は結果には表示されない

• この処理方法は特に否定が利用される場合に重要である

  • {p(1..2)} :- not p(Var).はVarについてunsafeとしてエラーとなる

  • {p(1..2)} :- not p(_).は以下に置換されて、p(1), p(2), p(1)p(2)のstable modelが出力される

      {p(1..2)}.
      aux :- p(Var).
      :- not aux.
    

終わりに

clingoのタグください。