응답 집합 프로그래밍

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

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

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

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

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

<head> :- <body> .

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

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

{p,q,r}.

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

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

1{p,q,r}2.

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

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

:- 2{p,q,r}.

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

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

그래프 색칠
그래프 의 -색칠은  함수로, 모든 인접한 정점 쌍 에 대해 를 만족한다. 주어진 그래프의 -색칠을 찾거나 (존재하지 않는 경우) 판별하기 위해 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 are vertices
e(1,55). % there is an edge from 1 to 55
. . .

그리고 의 숫자 값을 명령줄에서 지정하여 smodels를 실행하면, smodels 출력에 있는  형식의 원자들이 의 -색칠을 나타낼 것이다.

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

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

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

이것은 생성 및 테스트 조직의 또 다른 예시이다. 1행의 선택 규칙은 개의 정점으로 구성된 모든 집합을 "생성"한다. 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행의 선택 규칙은 모서리 집합의 모든 부분 집합을 "생성"한다. 세 개의 제약 조건은 해밀턴 회로가 아닌 부분 집합을 "제거"한다. 마지막 제약 조건은 보조 술어  ("는 0에서 도달 가능하다")를 사용하여 이 조건을 만족하지 않는 정점을 금지한다. 이 술어는 6행과 7행에서 재귀적으로 정의된다.

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

의존 구문 분석
자연어 처리에서 의존 기반 구문 분석은 ASP 문제로 공식화될 수 있다.
다음 코드는 라틴어 문장 "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라고 불리는 표준 언어 사양을 발표했으며, 최근 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와 같은 접지 시스템을 프런트엔드로 사용하여 접지를 강제함으로써 간접적으로만 지원한다. 접지의 필요성은 절의 조합 폭발을 야기할 수 있다. 따라서 즉석에서 접지를 수행하는 시스템이 유리할 수 있다.

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

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

 같이 보기 
 기본 논리
 논리형 프로그래밍
 비단조 논리
 프롤로그 (프로그래밍 언어)
 안정 모델 의미론

 각주 

 외부 링크 
 ASP-Core-2 2.03c 입력 언어 사양
 제1회 ASP 시스템 경쟁
 제2회 ASP 경쟁
 제3회 ASP 경쟁
 제4회 ASP 경쟁
 Platypus
 데비안/우분투용으로 패키징된 다양한 응답 집합 해결기 
 Clasp Answer Set Solver

분류:논리 프로그래밍