응답 집합 프로그래밍

응답 집합 프로그래밍(Answer set programming, ASP)은 어려운 (주로 NP-난해) 검색 문제에 초점을 맞춘 선언형 프로그래밍의 한 형태이다. 이는 논리형 프로그래밍의 안정 모델 (응답 집합) 의미론에 기반을 둔다. ASP에서 검색 문제는 안정 모델을 계산하는 것으로 축소되며, 안정 모델을 생성하는 프로그램인 응답 집합 해결기가 검색을 수행하는 데 사용된다. 많은 응답 집합 해결기의 설계에 사용되는 계산 과정은 DPLL 알고리즘의 향상된 버전이며, 원칙적으로 항상 종료된다 (프롤로그 쿼리 평가와 달리, 무한 루프로 이어질 수 있다).

더 일반적인 의미에서 ASP는 지식 표현에 대한 응답 집합의 모든 응용 프로그램과 이러한 응용 프로그램에서 발생하는 문제를 해결하기 위한 프롤로그 스타일 쿼리 평가 사용을 포함한다.^[1]^[2]

역사

응답 집합 프로그래밍의 초기 예는 1997년 디모풀로스, 네벨, 쾰러가 제안한 계획 방법이었다.^[3]^[4] 그들의 접근 방식은 계획과 안정 모델 간의 관계에 기반을 둔다.^[5] 1998년 소이니넨과 니멜라는^[6] 현재 응답 집합 프로그래밍으로 알려진 것을 제품 구성 문제에 적용했다.^[4] 1999년, "응답 집합 프로그래밍"이라는 용어가 "The Logic Programming Paradigm"이라는 책에 두 편의 논문 모음 제목으로 처음 등장했다.^[4] 이 논문들 중 첫 번째 논문은 검색을 위한 응답 집합 해결기 사용을 새로운 프로그래밍 패러다임으로 식별했다.^[7] 같은 해 니멜라도 "안정 모델 의미론을 가진 논리 프로그램"을 새로운 패러다임으로 제안했다.^[8]

응답 집합 프로그래밍 언어 AnsProlog

Lparse는 원래 응답 집합 해결기 smodels의 접지 도구(프런트엔드)로 생성된 프로그램의 이름이다. Lparse가 허용하는 언어는 이제 일반적으로 AnsProlog라고 불리며,^[9] 논리의 응답 집합 프로그래밍(Answer Set Programming in Logic)의 약어이다.^[10] 이제 assat, clasp, cmodels, gNt, nomore++ 및 pbmodels를 포함한 다른 많은 응답 집합 해결기에서 동일한 방식으로 사용된다. (dlv는 예외이다. dlv용으로 작성된 ASP 프로그램의 구문은 다소 다르다.)

AnsProlog 프로그램은 다음과 같은 형식의 규칙으로 구성된다.

<head> :- <body> .

<body>가 비어 있으면 :- ("만약") 기호는 생략된다. 이러한 규칙을 사실(fact)이라고 한다. 가장 간단한 Lparse 규칙은 제약 조건이 있는 규칙이다.

이 언어에 포함된 또 다른 유용한 구성은 선택(choice)이다. 예를 들어, 다음 선택 규칙은

{p,q,r}.

안정 모델에 $p,q,r$ 원자 중 어떤 것을 포함할지 임의로 선택하라는 의미이다. 이 선택 규칙만 포함하고 다른 규칙은 없는 Lparse 프로그램은 8개의 안정 모델(즉, $\{p,q,r\}$ 의 임의의 부분 집합)을 가진다. 안정 모델의 정의는 선택 규칙이 있는 프로그램으로 일반화되었다.^[11] 선택 규칙은 안정 모델 의미론 하의 명제 공식에 대한 약어로도 취급될 수 있다.^[12] 예를 들어, 위 선택 규칙은 세 개의 "배중률" 공식의 논리곱에 대한 약어로 볼 수 있다.

(p\lor \neg p)\land (q\lor \neg q)\land (r\lor \neg r).

Lparse 언어는 또한 다음과 같은 "제약 조건이 있는" 선택 규칙을 작성할 수 있게 한다.

1{p,q,r}2.

이 규칙은 $p,q,r$ 원자 중 최소 1개, 최대 2개를 선택하라는 의미이다. 이 규칙의 안정 모델 의미론 하의 의미는 명제 공식으로 표현된다.

(p\lor \neg p)\land (q\lor \neg q)\land (r\lor \neg r)

\land \,(p\lor q\lor r)\land \neg (p\land q\land r).

카디널리티 경계는 규칙의 본문에도 사용될 수 있다. 예를 들면 다음과 같다.

:- 2{p,q,r}.

이 제약 조건을 Lparse 프로그램에 추가하면 $p,q,r$ 원자 중 최소 2개를 포함하는 안정 모델이 제거된다. 이 규칙의 의미는 명제 공식으로 표현될 수 있다.

\neg ((p\land q)\lor (p\land r)\lor (q\land r)).

변수(다른 프롤로그처럼 대문자로 시작)는 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)

여기서 start와 end는 상수 값의 산술 표현식이다. 범위는 호환 가능한 방식으로 수치 도메인을 정의하는 데 주로 사용되는 표기법 단축키이다. 예를 들어, 다음 사실은

a(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)}.

안정 모델 생성

`filename` 파일에 저장된 Lparse 프로그램의 안정 모델을 찾으려면 다음 명령을 사용한다.

% lparse ${filename} | smodels

옵션 0은 smodels에게 프로그램의 모든 안정 모델을 찾도록 지시한다. 예를 들어, `test` 파일에 다음과 같은 규칙이 포함되어 있다면

1{p,q,r}2.
s :- not p.

다음 명령은 다음과 같은 출력을 생성한다.

% lparse test | smodels 0
Answer: 1
Stable Model: q p
Answer: 2
Stable Model: p
Answer: 3
Stable Model: r p
Answer: 4
Stable Model: q s
Answer: 5
Stable Model: r s
Answer: 6
Stable Model: r q s

ASP 프로그램 예시

그래프 색칠

그래프 $G=\left\langle V,E\right\rangle$ 의 $n$ -색칠은 $\mathrm {color} :V\to \{1,\dots ,n\}$ 함수로, 모든 인접한 정점 쌍 $(x,y)\in E$ 에 대해 $\mathrm {color} (x)\neq \mathrm {color} (y)$ 를 만족한다. 주어진 그래프의 $n$ -색칠을 찾거나 (존재하지 않는 경우) 판별하기 위해 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행은 숫자 $1,\dots ,n$ 을 색으로 정의한다. 2행의 선택 규칙에 따르면, 각 정점 $x$ 에 고유한 색 $i$ 가 할당되어야 한다. 3행의 제약 조건은 정점 $x$ 와 $y$ 사이에 연결하는 모서리가 있는 경우 동일한 색을 할당하는 것을 금지한다.

이 파일을 $G$ 의 정의와 결합하면 (예:

v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .

그리고 $n$ 의 숫자 값을 명령줄에서 지정하여 smodels를 실행하면, smodels 출력에 있는 $\mathrm {color} (\dots ,\dots )$ 형식의 원자들이 $G$ 의 $n$ -색칠을 나타낼 것이다.

이 예시의 프로그램은 간단한 ASP 프로그램에서 자주 볼 수 있는 "생성 및 테스트" 구성을 보여준다. 선택 규칙은 "잠재적 해" 집합을 설명한다. 이는 주어진 검색 문제의 해 집합의 단순한 상위 집합이다. 그 다음에는 허용되지 않는 모든 잠재적 해를 제거하는 제약 조건이 따른다. 그러나 smodels 및 다른 응답 집합 해결기에서 사용되는 검색 과정은 시행착오에 기반을 두지 않는다.

큰 클릭

그래프의 클릭은 쌍으로 인접한 정점들의 집합이다. 다음 Lparse 프로그램은 주어진 유향 그래프에서 크기가 $\geq n$ 인 클릭을 찾거나 존재하지 않는다고 판별한다.

n {in(X) : v(X)}.
:- in(X), in(Y), X!=Y, not e(X,Y).

이것은 생성 및 테스트 조직의 또 다른 예시이다. 1행의 선택 규칙은 $\geq n$ 개의 정점으로 구성된 모든 집합을 "생성"한다. 2행의 제약 조건은 클릭이 아닌 집합을 "제거"한다.

해밀턴 회로

유향 그래프의 해밀턴 회로는 그래프의 각 정점을 정확히 한 번 통과하는 경로이다. 다음 Lparse 프로그램은 주어진 유향 그래프에 해밀턴 회로가 존재하는 경우 이를 찾는 데 사용될 수 있다. 0은 정점 중 하나라고 가정한다.

{in(X,Y)} :- e(X,Y).

:- 2 {in(X,Y) : e(X,Y)}, v(X).
:- 2 {in(X,Y) : e(X,Y)}, v(Y).

r(X) :- in(0,X), v(X).
r(Y) :- r(X), in(X,Y), e(X,Y).

:- not r(X), v(X).

1행의 선택 규칙은 모서리 집합의 모든 부분 집합을 "생성"한다. 세 개의 제약 조건은 해밀턴 회로가 아닌 부분 집합을 "제거"한다. 마지막 제약 조건은 보조 술어 $r(x)$ (" $x$ 는 0에서 도달 가능하다")를 사용하여 이 조건을 만족하지 않는 정점을 금지한다. 이 술어는 6행과 7행에서 재귀적으로 정의된다.

이 프로그램은 보다 일반적인 "생성, 정의 및 테스트" 조직의 예시이다. 이는 모든 "나쁜" 잠재적 해를 제거하는 데 도움이 되는 보조 술어의 정의를 포함한다.

의존 구문 분석

자연어 처리에서 의존 기반 구문 분석은 ASP 문제로 공식화될 수 있다.^[13] 다음 코드는 라틴어 문장 "Puella pulchra in villa linguam latinam discit"("예쁜 소녀는 빌라에서 라틴어를 배우고 있다")를 구문 분석한다. 구문 트리는 문장 단어 간의 의존성을 나타내는 arc 술어로 표현된다. 계산된 구조는 선형 순서가 있는 루트 트리이다.

% ********** input sentence **********
word(1, puella). word(2, pulchra). word(3, in). word(4, villa). word(5, linguam). word(6, latinam). word(7, discit).
% ********** lexicon **********
1{ node(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{ node(X, attr(puella, n, fem, nom, sg));
   node(X, attr(puella, n, fem, abl, sg)) }1 :- word(X, puella).
1{ node(X, attr(villa, n, fem, nom, sg));
   node(X, attr(villa, n, fem, abl, sg)) }1 :- word(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).
% ********** syntactic rules **********
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, Gender, Case, Number)), node(Y, attr(_, a, Gender, Case, 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).
% ********** guaranteeing the treeness of the graph **********
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, not path(X, Y).
leaf(X) :- node(X, _), not 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에서 영감을 받은 충돌 기반 알고리즘을 사용하는 하이브리드 접근 방식을 사용한다. 이러한 접근 방식은 초기 퇴각검색 알고리즘에 비해 성능을 크게 향상시키며, 종종 10배 정도 향상시킨다.

Potassco 프로젝트는 clasp, 접지 시스템(gringo), 증분 시스템(iclingo), 제약 해결기(clingcon), 액션 언어에서 ASP 컴파일러(coala), 분산 메시지 전달 인터페이스 구현(claspar) 등 아래의 많은 시스템에 대한 우산 역할을 한다.

대부분의 시스템은 변수를 지원하지만, Lparse 또는 gringo와 같은 접지 시스템을 프런트엔드로 사용하여 접지를 강제함으로써 간접적으로만 지원한다. 접지의 필요성은 절의 조합 폭발을 야기할 수 있다. 따라서 즉석에서 접지를 수행하는 시스템이 유리할 수 있다.^[15]

Galliwasp 시스템^[16] 및 s(CASP)^[17]와 같은 응답 집합 프로그래밍의 쿼리 기반 구현은 분해 증명과 코귀납법을 조합하여 접지를 완전히 피한다.

플랫폼			기능					메커니즘
이름	OS	라이선스	변수	함수 기호	명시적 집합	명시적 목록	비배타적 (선택 규칙) 지원
ASPeRiX 보관됨 2016-11-08 - 웨이백 머신	리눅스	GPL	예				아니요	온더플라이 접지
ASSAT	솔라리스	프리웨어						SAT-해결기 기반
Clasp Answer Set Solver	리눅스, MacOS, 윈도우	MIT 허가서	Clingo에서 가능	예	아니요	아니요	예	증분, SAT-해결기 영감(nogood, conflict-driven)
Cmodels	리눅스, 솔라리스	GPL	접지 필요				예	증분, SAT-해결기 영감(nogood, conflict-driven)
diff-SAT	리눅스, MacOS, 윈도우 (자바 가상 머신)	MIT 허가서	접지 필요				예	SAT-해결기 영감(nogood, conflict-driven). 확률 문제 해결 및 응답 집합 샘플링 지원
DLV	리눅스, MacOS, 윈도우^[18]	학술 및 비상업 교육용, 비영리 단체용으로 무료^[18]	예	예	아니요	아니요	예	Lparse 호환 안 됨
DLV-Complex	리눅스, MacOS, 윈도우	GPL		예	예	예	예	DLV 기반 - Lparse 호환 안 됨
GnT	리눅스	GPL	접지 필요				예	smodels 기반
nomore++	리눅스	GPL						리터럴+규칙 기반 결합
Platypus	리눅스, 솔라리스, 윈도우	GPL						분산, 다중 스레드 nomore++, smodels
Pbmodels	리눅스	?						의사 불리언 해결기 기반
Smodels	리눅스, MacOS, 윈도우	GPL	접지 필요	아니요	아니요	아니요	아니요
Smodels-cc 보관됨 2015-11-15 - 웨이백 머신	리눅스	?	접지 필요					SAT-해결기 기반; smodels w/충돌 절
Sup	리눅스	?						SAT-해결기 기반

같이 보기

각주

↑ Baral, Chitta (2003). 《Knowledge Representation, Reasoning and Declarative Problem Solving》. Cambridge University Press. ISBN 978-0-521-81802-5.
↑ Gelfond, Michael (2008). 〈Answer sets〉. van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce. 《Handbook of Knowledge Representation》. Elsevier. 285–316쪽. ISBN 978-0-08-055702-1. as PDF 보관됨 2016-03-03 - 웨이백 머신
↑ Dimopoulos, Y.; Nebel, B.; Köhler, J. (1997). 〈Encoding planning problems in non-monotonic logic programs〉. Steel, Sam; Alami, Rachid. 《Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, France, September 24–26, 1997, Proceedings》. Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence 1348. Springer. 273–285쪽. ISBN 978-3-540-63912-1. as Postscript
↑ ^가 ^나 ^다 Lifschitz, Vladimir (2008년 7월 13일). 《What is answer set programming?》 (PDF). 《Proceedings of the 23rd National Conference on Artificial Intelligence》 3 (AAAI Press). 1594–1597쪽.
↑ Subrahmanian, V.S.; Zaniolo, C. (1995). 〈Relating stable models and AI planning domains〉. Sterling, Leon. 《Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming》. MIT Press. 233–247쪽. ISBN 978-0-262-69177-2. as Postscript
↑ Soininen, T.; Niemelä, I. (1998), 《Formalizing configuration knowledge using rules with choices》 (Postscript) (TKO-B142), Laboratory of Information Processing Science, Helsinki University of Technology
↑ Marek, V.; Truszczyński, M. (1999년 5월 20일). 〈Stable models and an alternative logic programming paradigm〉. Apt, Krzysztof R. 《The Logic programming paradigm: a 25-year perspective》 (PDF). Springer. 169–181쪽. arXiv:cs/9809032. ISBN 978-3-540-65463-6.
↑ Niemelä, I. (November 1999). 《Logic programs with stable model semantics as a constraint programming paradigm》 (Postscript,gzipped). 《Annals of Mathematics and Artificial Intelligence》 25. 241–273쪽. doi:10.1023/A:1018930122475. S2CID 14465318.
↑ Crick, Tom (2009). 《Superoptimisation: Provably Optimal Code Generation using Answer Set Programming》 (PDF) (Ph.D.). University of Bath. Docket 20352. 2016년 3월 4일에 원본 문서 (PDF)에서 보존된 문서. 2011년 5월 27일에 확인함.
↑ Rogelio Davila. “AnsProlog, an overview” (PowerPoint).
↑ Niemelä, I.; Simons, P.; Soinenen, T. (2000). 〈Stable model semantics of weight constraint rules〉. Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald. 《Logic Programming and Nonmonotonic Reasoning: 5th International Conference, LPNMR '99, El Paso, Texas, USA, December 2–4, 1999 Proceedings》. Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence 1730. Springer. 317–331쪽. ISBN 978-3-540-66749-0. as Postscript
↑ Ferraris, P.; Lifschitz, V. (January 2005). 《Weight constraints as nested expressions》. 《Theory and Practice of Logic Programming》 5. 45–74쪽. arXiv:cs/0312045. doi:10.1017/S1471068403001923. S2CID 5051610. as Postscript
↑ “Dependency parsing”. 2015년 4월 15일에 원본 문서에서 보존된 문서. 2015년 4월 15일에 확인함.
↑ “ASP-Core-2 Input Language Specification” (PDF). 2018년 5월 14일에 확인함.
↑ Lefèvre, Claire; Béatrix, Christopher; Stéphan, Igor; Garcia, Laurent (May 2017). 《ASPeRiX, a first-order forward chaining approach for answer set computing*》. 《Theory and Practice of Logic Programming》 (영어) 17. 266–310쪽. arXiv:1503.07717. doi:10.1017/S1471068416000569. ISSN 1471-0684. S2CID 2371655.
↑ Marple, Kyle.; Gupta, Gopal. (2012). 〈Galliwasp: A Goal-Directed Answer Set Solver〉. Albert, Elvira. 《Logic-Based Program Synthesis and Transformation, 22nd International Symposium, LOPSTR 2012, Leuven, Belgium, September 18-20, 2012, Revised Selected Papers》. Springer. 122–136쪽.
↑ Arias, J.; Carro, M.; Salazar, E.; Marple, K.; Gupta, G. (2018). 《Constraint Answer Set Programming without Grounding》. 《Theory and Practice of Logic Programming》 18. 337–354쪽. arXiv:1804.11162. doi:10.1017/S1471068418000285. S2CID 13754645.
↑ ^가 ^나 “DLV System company page”. DLVSYSTEM s.r.l. 2011년 11월 16일에 확인함.