응답 세트 프로그래밍
Answer set programming프로그래밍 패러다임 |
---|
ASP(Answer set programming)는 어려운(주로 NP-hard) 검색 문제를 지향하는 선언형 프로그래밍의 한 형태입니다.이것은 논리 프로그래밍의 안정적인 모델(응답 집합) 의미론에 기초합니다.ASP에서는 검색 문제가 안정적인 모델을 계산하기 위해 축소되고, 안정적인 모델을 생성하기 위한 프로그램인 응답 집합 솔버가 검색을 수행하기 위해 사용됩니다.다수의 응답 세트솔버 설계에 채용된 계산 프로세스는 DPLL 알고리즘의 확장으로 원칙적으로 항상 종료됩니다(프롤로그 쿼리 평가와는 달리 무한 루프가 발생할 수 있습니다).
좀 더 일반적인 의미에서 ASP에는 지식[1][2] 표현에 대한 모든 응답 세트 응용 프로그램과 이러한 응용 프로그램에서 발생하는 문제를 해결하기 위한 프롤로그 형식의 쿼리 평가 사용이 포함됩니다.
역사
응답 세트 프로그래밍의 초기 예는 1997년 Dimopoulos, Nebel 및 [3][4]Köhler가 제안한 계획 방법입니다.이들의 접근 방식은 계획과 안정적인 [5]모델 간의 관계를 기반으로 합니다.1998년 Soinen과 Niemelae는[6] 현재 응답 세트 프로그래밍으로 알려진 것을 제품 [4]구성 문제에 적용했습니다.1999년, "정답 집합 프로그래밍"이라는 용어는 두 [4]논문 모음의 제목으로 논리 프로그래밍 패러다임이라는 책에서 처음으로 등장했습니다.이 논문들 중 첫 번째 논문은 검색을 위한 응답 집합 솔버의 사용을 새로운 프로그래밍 [7]패러다임으로 식별했다.같은 해 니멜래는 새로운 [8]패러다임으로 "안정적인 모델 의미론을 가진 논리 프로그램"을 제안했다.
Answer 세트 프로그래밍 언어 AnsProlog
Lparse는 원래 Answer set solver smodel의 접지 도구(프런트 엔드)로 작성된 프로그램의 이름입니다.Lparse가 받아들이는 언어는 현재 일반적으로 AnsProlog로 [9]불리며,[10] Logic의 Answer Set Programming의 줄임말입니다.현재는 assat, 클래스프, cmodel, gNt, nomore++ 및 pbmodel을 포함한 많은 다른 응답 세트솔러에서도 같은 방법으로 사용되고 있습니다.(dlv는 예외입니다.dlv용으로 작성된ASP 프로그램의 구문은 다소 다릅니다).
AnsProlog 프로그램은 폼의 규칙으로 구성됩니다.
< >머리> :- < >몸> .
기호:-
(「if」)는, 다음의 경우에 드롭 됩니다.<body>
비어 있습니다. 이러한 규칙을 사실이라고 합니다.가장 간단한 종류의 Lparse 규칙은 제약이 있는 규칙입니다.
이 언어에 포함된 다른 유용한 구성 요소는 선택입니다.예를 들어, 선택 규칙
{p,q,r}.
다음과 같이 말합니다된 에 포함할원자 q, rp, 중 어느 것을 임의로 선택합니다.이 선택 규칙과 다른 규칙이 없는 Lparse 프로그램에는 8개의 안정적인 모델({, 이 있습니다.안정적인 모델의 정의는 선택 [11]규칙이 있는 프로그램으로 일반화되었습니다.선택 규칙은 또한 안정적인 [12]모델 의미론 하에서 명제 공식의 약자로 취급될 수 있다.예를 들어, 위의 선택 규칙은 세 가지 "제외된 중간" 공식의 결합에 대한 약어로 볼 수 있습니다.
Lparse 언어를 사용하면 다음과 같은 "제한된" 선택 규칙을 작성할 수도 있습니다.
1{p,q,r}2.
규칙에는 pq, p중 적어도1개를 선택하지만 2개를 넘지 않도록 되어 있습니다.안정적 모델 의미론 하에서 이 규칙의 의미는 명제 공식으로 표현된다.
카디널리티 바운드는 규칙 본문에서도 사용할 수 있습니다.다음은 예를 제시하겠습니다.
:- 2{p,q,r}.
Lparse 프로그램에 이 제약을 추가하면 p 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는 상수 값 산술식입니다.범위는 주로 호환되는 방법으로 숫자 도메인을 정의하기 위해 사용되는 알림 단축키입니다.예를 들어, 사실은
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)}.
안정적인 모델 생성
파일에 저장된 Lparse 프로그램의 안정적인 모델을 찾으려면${filename}
명령어를 사용합니다.
lparse ${140}모델 %
옵션 0은 프로그램의 모든 안정적인 모델을 찾도록 Smodel에게 지시합니다.예를 들어, 파일이test
규칙을 포함합니다.
1{p,q,r}2. s :- 것은 아니다. p.
명령어를 실행하면 출력이 생성됩니다.
% lparse 검정 모형 0 답: 1 안정적인 모형: q p 답: 2 안정적인 모형: p 답: 3 안정적인 모형: r p 답: 4 안정적인 모형: q s 답: 5 안정적인 모형: r s 답: 6 안정적인 모형: r q s
ASP 프로그램의 예
그래프 색칠
G 、 E { G = \ \ V , \ \ }의n { displaystyle \ { : V { , ,} { \ mathrm { color } : } - \ \ { 1,rangle } \ langle } 。또는 인접한 모든정점 y )E ( EASP를 사용하여 특정 그래프의 n{\ n -컬러를 (또는 존재하지 않는다고 판단합니다).
이 작업은 다음 Lparse 프로그램을 사용하여 수행할 수 있습니다.
c(1..n). 1 {색.(X,I) : c(I)} 1 :- v(X). :- 색.(X,I), 색.(Y,I), e(X,Y), c(I).
1행은 1, (\ 1을 색으로 정의합니다.2행의 선택 규칙에 따라 각 x x\x에 고유한 색상 i를 할당해야 합니다.라인 3의 구속조건은 x x와 y y를 연결하는 가장자리가 있는 경우 동일한 색상을 지정할 수 없습니다.
이 파일을 G G의 정의와 조합하면 다음과 같습니다.
v(1..100). % 1,...100은 정점입니다. e(1,55). 엣지가 1에서 55까지 있는 비율 . . .
smodels를 실행하고 명령줄에서 n n의 숫자 값을 지정하면 smodels 출력에서 l , )(\) 의 원자는의n(\ g 을 나타냅니다.
이 예의 프로그램은 단순한 ASP 프로그램에서 자주 볼 수 있는 "생성 및 테스트" 구성을 보여 줍니다.선택 규칙은 특정 검색 문제에 대한 솔루션 집합의 단순한 상위 집합인 "잠재적 솔루션" 집합을 설명합니다.그 뒤에 제약이 따르는데, 이 제약은 수용 불가능한 모든 잠재적 해결책을 제거합니다.그러나 Smodel 및 기타 응답 세트솔러에 의해 사용되는 검색 프로세스는 시행착오를 기반으로 하지 않습니다.
대규모 집단
그래프의 클리크는 쌍으로 인접한 정점의 집합입니다.다음 Lparse 프로그램은 지정된 그래프에서 크기 n의 클리크를 찾거나 존재하지 않는다고 판단합니다.
n {에(X) : v(X)}. :- 에(X), 에(Y), v(X), v(Y), X!=Y, 것은 아니다. e(X,Y), 것은 아니다. e(Y,X).
이것은 생성 및 테스트 구성의 또 다른 예입니다.라인 1의 선택 규칙은 \ n 정점으로 구성된 모든 세트를 "생성"합니다.라인 2의 제약에 의해, 클리어가 아닌 세트가 「위드 아웃」됩니다.
해밀턴 순환
방향 그래프의 해밀턴 사이클은 그래프의 각 정점을 정확히 한 번 통과하는 사이클입니다.다음 Lparse 프로그램은 주어진 방향 그래프에서 해밀턴 사이클이 존재하는 경우 이를 찾기 위해 사용할 수 있습니다. 우리는 0이 정점 중 하나라고 가정합니다.
{에(X,Y)} :- e(X,Y). :- 2 {에(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의 선택 규칙은 에지 세트의 모든 하위 집합을 "생성"합니다.세 가지 제약조건은 해밀턴 사이클이 아닌 서브셋을 "풀어내기" 합니다.이들 중 마지막은 술어 r)\ r x는 0"부터 도달 가능)를 사용하여 이 조건을 충족하지 않는 정점을 금지합니다.이 술어는 6행과 7행에서 재귀적으로 정의되어 있습니다.
이 프로그램은 보다 일반적인 "생성, 정의 및 테스트" 조직의 한 예입니다.모든 "나쁜" 잠재적 솔루션을 제거하는 데 도움이 되는 보조 술어의 정의를 포함합니다.
의존관계 해석
자연어 처리에서는 의존성 기반의 파싱이 ASP [13]문제로 공식화될 수 있습니다.다음 암호는 라틴어 문장 "Puella pulchra in villa linguam latinam discit", "예쁜 소녀가 빌라에서 라틴어를 배우고 있습니다."를 구문 해석합니다.구문 트리는 문장 단어 간의 종속성을 나타내는 호 술어로 표현됩니다.계산된 구조는 선형 순서 루트 트리입니다.
%********** 입력문************** 단어(1, 푸에라). 단어(2, 풀크라). 단어(3, 에). 단어(4, 별장). 단어(5, 언어). 단어(6, 라틴어). 단어(7, 디스켓). %******************* 어휘 1{ 노드(X, 특성(풀처, a, 펨, 명명하다, sg)); 노드(X, 특성(풀처, a, 펨, 애블, sg)) }1 :- 단어(X, 풀크라). 노드(X, 특성(라틴어, a, 펨, 액세스, sg)) :- 단어(X, 라틴어). 1{ 노드(X, 특성(푸에라, n, 펨, 명명하다, sg)); 노드(X, 특성(푸에라, n, 펨, 애블, sg)) }1 :- 단어(X, 푸에라). 1{ 노드(X, 특성(별장, n, 펨, 명명하다, sg)); 노드(X, 특성(별장, n, 펨, 애블, sg)) }1 :- 단어(X, 별장). 노드(X, 특성(언어, n, 펨, 액세스, sg)) :- 단어(X, 언어). 노드(X, 특성(분리하다, v, 존재하다, 3, sg)) :- 단어(X, 디스켓). 노드(X, 특성(에, p)) :- 단어(X, 에). % ********* 구문 규칙 *************** 0{ 아아크(X, Y, 서브j) }1 :- 노드(X, 특성(_, v, _, 3, sg)), 노드(Y, 특성(_, n, _, 명명하다, sg)). 0{ 아아크(X, Y, 도비지) }1 :- 노드(X, 특성(_, v, _, 3, sg)), 노드(Y, 특성(_, n, _, 액세스, sg)). 0{ 아아크(X, Y, 특성) }1 :- 노드(X, 특성(_, n, 성별, 사례., 번호)), 노드(Y, 특성(_, a, 성별, 사례., 번호)). 0{ 아아크(X, Y, 준비하다) }1 :- 노드(X, 특성(_, p)), 노드(Y, 특성(_, n, _, 애블, _)), X < > Y. 0{ 아아크(X, Y, 어드밴스) }1 :- 노드(X, 특성(_, v, _, _, _)), 노드(Y, 특성(_, p)), 것은 아니다. 잎사귀(Y). %**************************그래프의 선명함을 보증합니다. 1{ 뿌리(X):노드(X, _) }1. :- 아아크(X, Z, _), 아아크(Y, Z, _), X != Y. :- 아아크(X, Y, L1), 아아크(X, Y, L2), L1 != L2. 경로.(X, Y) :- 아아크(X, Y, _). 경로.(X, Z) :- 아아크(X, Y, _), 경로.(Y, Z). :- 경로.(X, X). :- 뿌리(X), 노드(Y, _), X != Y, 것은 아니다. 경로.(X, Y). 잎사귀(X) :- 노드(X, _), 것은 아니다. 아아크(X, _, _).
언어 표준화 및 ASP 경쟁 제품
ASP 표준화 작업 그룹은 ASP-Core-2라고 [14]불리는 표준 언어 사양을 작성했으며, 이를 위해 최신 ASP 시스템이 수렴되고 있습니다.ASP-Core-2는 ASP 해결사가 여러 참조 문제에 대해 정기적으로 벤치마킹되는 Answer Set Programming Competition의 참조 언어입니다.
구현 비교
Smodels와 같은 초기 시스템은 해결책을 찾기 위해 역추적을 사용했습니다.Boolean SAT 솔버의 이론과 실천이 진화함에 따라 ASSAT 및 Cmodels를 포함한 다수의 ASP 솔버가 SAT 솔버 위에 구축되었습니다.이러한 ASP 공식은 SAT 제안으로 변환되어 SAT 솔버를 적용한 후 ASP 형태로 다시 변환되었습니다.Class와 같은 최신 시스템에서는 SAT에서 영감을 받은 충돌 기반 알고리즘을 사용하여 하이브리드 방식을 사용하며, 완전한 부울 논리 형식으로 변환하지 않습니다.이러한 접근방식을 통해 성능의 대폭적인 향상을 실현할 수 있습니다.대부분의 경우 이전 역추적 알고리즘에 비해 성능의 대폭적인 향상을 기대할 수 있습니다.
Potassco 프로젝트는 클래스프, 접지 시스템(gringo), 증분 시스템(ilingo), 제약 해결사(ringcon), ASP 컴파일러에 대한 액션 언어(coala), 분산 MPI 구현(claspar) 등을 포함한 많은 시스템의 우산 역할을 합니다.
대부분의 시스템은 Lparse 또는 Gringo 등의 접지 시스템을 프런트 엔드로 사용하여 변수를 지원하지만 간접적으로만 접지합니다.접지가 필요하기 때문에 절의 조합이 폭발적으로 증가할 수 있습니다.따라서 즉시 접지를 실행하는 시스템이 [15]유리할 수 있습니다.
Galliwasp 시스템[16] 및 s(CASP)[17]와 같은 응답 세트프로그래밍의 쿼리 구동 실장은 분해능과 공유도를 조합하여 완전히 접지를 회피합니다.
플랫폼 | 특징들 | 메카닉스 | ||||||
---|---|---|---|---|---|---|---|---|
이름. | OS | 라이선스 | 변수 | 기능 기호 | 명시적 집합 | 명시적 리스트 | 분리(선택 규칙) 지원 | |
ASPeRiX | 리눅스 | GPL | 네. | 아니요. | 온 더 플라이 | |||
앗사 | 솔라리스 | 프리웨어 | SAT 솔루션 기반 | |||||
답안 세트솔버 걸쇠 | Linux, macOS, Windows | MIT 라이선스 | 네, 클링고에서 | 네. | 아니요. | 아니요. | 네. | 증분형, SAT 해결사(부적합, 충돌 주도형) |
CModels | Linux, Solaris | GPL | 접지 필요 | 네. | 증분형, SAT 해결사(부적합, 충돌 주도형) | |||
diff- | Linux, macOS, Windows(Java 가상 머신) | MIT 라이선스 | 접지 필요 | 네. | SAT 해결사(불량, 갈등)에 대한 영감을 받았습니다.확률론적 문제 해결 및 응답 세트 샘플링 지원 | |||
DLV | Linux, macOS, Windows[18] | 학술적, 비상업적 교육용 및 비영리 단체용[18] 무료 | 네. | 네. | 아니요. | 아니요. | 네. | LParse와 호환되지 않음 |
DLV 콤플렉스 | Linux, macOS, Windows | GPL | 네. | 네. | 네. | 네. | DLV를 기반으로 구축 - LParse와 호환되지 않음 | |
GnT | 리눅스 | GPL | 접지 필요 | 네. | 스모델 위에 세워지다 | |||
nomore++ | 리눅스 | GPL | 복합 리터럴+규칙 베이스 | |||||
오리너구리과 | Linux, Solaris, Windows | GPL | 분산, 멀티패키지 nomore+, smodel | |||||
PB모델 | 리눅스 | ? | 의사 결정 솔버 베이스 | |||||
스모델 | Linux, macOS, Windows | GPL | 접지 필요 | 아니요. | 아니요. | 아니요. | 아니요. | |
Smodels-cc | 리눅스 | ? | 접지 필요 | SAT 솔루션 기반, 컨플릭트 조항이 포함된 Smodel | ||||
Sup(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". In van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.). Handbook of Knowledge Representation. Elsevier. pp. 285–316. ISBN 978-0-08-055702-1. PDF로 Wayback Machine에 보관된 2016-03-03
- ^ Dimopoulos, Y.; Nebel, B.; Köhler, J. (1997). "Encoding planning problems in non-monotonic logic programs". In Steel, Sam; Alami, Rachid (eds.). 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. Vol. 1348. Springer. pp. 273–285. ISBN 978-3-540-63912-1. 추서로
- ^ a b c Lifschitz, Vladimir (13 July 2008). "What is answer set programming?" (PDF). Proceedings of the 23rd National Conference on Artificial Intelligence. AAAI Press. 3: 1594–1597.
- ^ Subrahmanian, V.S.; Zaniolo, C. (1995). "Relating stable models and AI planning domains". In Sterling, Leon (ed.). Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming. MIT Press. pp. 233–247. ISBN 978-0-262-69177-2. 추서로
- ^ Soininen, T.; Niemelä, I. (1998), Formalizing configuration knowledge using rules with choices (Postscript), Laboratory of Information Processing Science, Helsinki University of Technology
- ^ Marek, V.; Truszczyński, M. (20 May 1999). "Stable models and an alternative logic programming paradigm". In Apt, Krzysztof R. (ed.). The Logic programming paradigm: a 25-year perspective (PDF). Springer. pp. 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 (3/4): 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. Archived from the original (PDF) on 2016-03-04. Retrieved 2011-05-27.
- ^ Rogelio Davila. "AnsProlog, an overview" (PowerPoint).
- ^ Niemelä, I.; Simons, P.; Soinenen, T. (2000). "Stable model semantics of weight constraint rules". In Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald (eds.). 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. Vol. 1730. Springer. pp. 317–331. ISBN 978-3-540-66749-0. 추서로
- ^ Ferraris, P.; Lifschitz, V. (January 2005). "Weight constraints as nested expressions". Theory and Practice of Logic Programming. 5 (1–2): 45–74. arXiv:cs/0312045. doi:10.1017/S1471068403001923. S2CID 5051610. 추서로
- ^ "Dependency parsing". Archived from the original on 2015-04-15. Retrieved 2015-04-15.
- ^ "ASP-Core-2 Input Language Specification" (PDF). Retrieved 14 May 2018.
- ^ 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 (3): 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". In Albert, Elvira (ed.). Logic-Based Program Synthesis and Transformation, 22nd International Symposium, LOPSTR 2012, Leuven, Belgium, September 18-20, 2012, Revised Selected Papers. Springer. pp. 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 (3–4): 337–354. doi:10.1017/S1471068418000285. S2CID 13754645.
- ^ a b "DLV System company page". DLVSYSTEM s.r.l. Retrieved 16 November 2011.