برنامهنویسی مجموعه جواب
برنامهنویسی مجموعه جواب (به انگلیسی: Answer set programming) با کوتهنوشت ASP نوعی برنامهنویسی اعلانی است که به سمت مسائل جستجوی مشکل (در اصل انپی سخت) گرایش دارد. ASP مبتنی بر معناشناسی مدل پایدار (مجموعه جواب) در برنامهنویسی منطقی است. در ASP مسائل جستجو به محاسبه مدلهای پایدار کاهش مییابد، و از حلکنندههای مجموعه جواب-برنامههای تولید مدلهای پایدار- برای ایجاد جستجو استفاده میشود. فرایند محاسباتی استفاده شده در طراحی بسیاری از حلکنندههای مجموعه جواب، نوعی بهبود الگوریتم DPLL هستند، و در اصل همیشه خاتمه مییابند (برخلاف ارزیابی پرسمان در پرولوگ، که میتواند منجر به حلقه بیپایان شود).
پارادایمهای برنامهنویسی |
---|
|
در مفهوم عمومیتر، ASP شامل همه کاربردهای مجموعه جواب در نمایش دانش است،[1][2] و از ارزیابی پرسمان شبه-پرولوگ برای حل مسائلی که در این کاربردها بروز میکند، استفاده میکند.
تاریخچه
یکی از مثالهای اولیه برنامهنویسی مجموعه جواب، روش برنامهریزی بود که در سال ۱۹۹۳ توسط دیموپولوس، نبل و کوهلر[3] ارائه شد. دیدگاه آنها مبتنی بر رابطه بین برنامهها و مدلهای پایدار بود.[4] سوینینن و نیملا[5] آنچه امروزه برنامهنویسی مجموعه جواب نامیده میشود را به مسئله پیکربندی محصول اعمال کرد. استفاده از حلکنندههای مجموعه جواب برای جستجو توسط مارک و تروشسینسکی به عنوان یک پارادایم برنامهنویسی، اولین بار در مقاله ای که چشمانداز ۲۵ ساله دربارهٔ پارادایم برنامهنویسی منطقی در سال ۱۹۹۹ منتشر شد،[6] و در [Niemelä 1999][7] شناسایی شد. در واقع اصطلاحشناسی جدید «مجموعه جواب» به جای «مدل پایدار» اولین بار توسط لیفشیتس[8] در یک مقاله که نمایش دهنده مجلدهای پیشنگرانه در مقاله مارک-تروشچینسکی بود، پیشنهاد شد.
زبان برنامهنویسی مجموعه جواب AnsProlog
Lparse نام برنامهای است که در اصل به عنوان یک ابزار زمینهای (front-end) برای حلکننده مجموعه جواب smodels ساخته شدهاست. امروزه به زبانی که Lparse میپذیرد، معمولاً AnsProlog گفته میشود،[9] که کوتهنوشتی برای عبارت «برنامهنویسی مجموعه جواب در منطق» است.[10] از این زبان امروزه در خیلی از حلکنندههای مجموعه جواب دیگر، شامل assat, clasp, cmodels, gNt, nomore++ و pbmodels استفاده میشود. (اما زبان dlv یک اسثتثنا است زیرا نحو برنامههای ASP نوشته شده به dlv متفاوت است).
برنامه AnsProlog شامل قواعدی از حالت
<head> :- <body> .
نماد :-
(یعنی اگر) اگر قسمت بدنه (یعنی <body>
) خالی باشد، حذف میشود؛ به این نوع از قواعد، «واقعیت» یا fact گفته میشود. سادهترین نوع قواعد Lparse, قواعد محدودیتدار هستند.
یک ساختار مفید دیگر که در این زبان وجود دارد، مفهوم «گزینه یا choice» است. برای مثال، قاعده گزینه
{p,q,r}.
میگوید: به صورت دلخواه انتخاب کنید که کدامیک از اتمهای در مدل پایدار شامل بشود. برنامه Lparse ای که شامل این قاعده انتخاب است و هیچ قاعده دیگری ندارد، به تعداد ۸ عدد مدل پایدار دارد-که زیرمجموعههای دلخواه هستند. تعریف یک مدل پایدار را میتوان به برنامههای دارای قواعد انتخاب تعمیم داد.[11] قواعد گزینه میتواند به صورت اختصاری از کوتاه شدهای از فرمولهای گزارهای تحت معناشناسی مدل پایدار رفتار کنند.[12] برای مثال، قاعده گزینه بالا را میتوان به صورت نوع مختصری برای عطف سه فرمول «اصل طرد ثالث» در نظر گرفت:
زبان Lparse به ما امکان نوشتن قواعد گزینه «محدودشده» را نیز میدهد، مثل
1{p,q,r}2.
این قاعده میگوید: حداقل یکی از اتمهای ، اما نه بیشتر از ۲ تا اتم را انتخاب کنید. معنای این قاعده تحت معناشناسی مدل پایدار توسط فرمول گزارهای زیر نمایش مییابد:
محدودههای کاردینالیتی (تعدادی)، در بدنه یک قاعده هم قابل استفاده اند، برای مثال
:- 2{p,q,r}.
اگر این محدودیت را به برنامه Lparse اضافه کنیم، مدلهای پایداری که حداقل دو اتم را حذف میکند. معنی این قاعده را میتوان توسط توسط فرمول گزارهای زیر نمایش داد:
در 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.
است، یک «محدوده یا range» حالت زیر را دارد:
(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)}.
است.
تولید مدلهای پایدار
برای یافتن یک مدل پایدار برنامه Lparse که در فایل ${filename}
ذخیره شدهاست، ما از فرمان زیر استفاده میکنیم
% 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
رنگآمیزی گراف
رنگآمیزی تایی یک گراف یک تابع such that برای هر جفت از راسهای مجاور است. ما میخواهیم از 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).
خط ۱ تعریف کننده اعداد به عنوان رنگها است. بر اساس قاعده انتخاب موجود در خط ۲، یک رنگ یکتا را باید به هر راس انتساب داد. محدودیت موجود در خط ۳ از انتساب رنگ مشابه به راسهای و ، موقعی که یک یال آنها را به هم متصل کند، جلوگیری میکند.
اگر ما این فایل را با یک تعریف از مثل تعریف زیر ترکیب کنیم:
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), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).
این یک مثال دیگر برای سازمان «تولید و آزمون» است. قاعده گزینه در خط ۱ «تولیدکننده» همه مجموعههای شامل راس است. محدودیت خط ۲، همه مجموعههایی که کلیک نیستند را «هرس میکند».
دور همیلتونی
یک دور همیلتونی در یک گراف جهتدار یک دور است که از هر راس گراف دقیقاً یکبار عبور میکند. برنامه 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).
قاعده گزینه در خط ۱ همه زیرمجموعههای مجموعه یالها را «تولید میکند». سه محدودیت، زیرمجموعههایی که دور همیلتونی نیستند را «هرس میکنند». آخرین آنها از گزارهٔ کمکی ( قابل دستیابی از 0 است) استفاده میکند تا راسهایی که این شرط را برآورده نمیکنند را ممنوعسازی کند. این گزاره در خطوط ۶ و ۷ به صورت بازگشتی تعریف شدهاند.
این برنامه یک مثال از سازمان کلیتر «تولید، تعریف، و آزمون» است: شامل تعریف یک گزاره کمکی است که به ما کمک میکند تا همه راهحلهای بالقوه «بد» را حذف کند.
تجزیهکننده وابستگی
در پردازش زبانهای طبیعی، «تجزیهکننده مبتنی بر وابستگی» را میتوان توسط یک برنامه 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 بولی تکامل یافتند، تعدادی از حلکنندههای ASP روی حلکنندههای SAT ساخته شدند، که شامل ASSAT و Cmodels بودند. این حلکنندهها فرمول ASP را به گزارههای SAT تبدیل میکردند، سپس حلکننده SAT اعمال میشد، و سپس جوابها را به حالت ASP باز تبدیل میکردند. سامانههای جدیدتر، مثل Clasp، از یک دیدگاه ترکیبی استفاده میکند، که از الگوریتمهای مغایرتگرای الهامگرفته از SAT استفاده میکرد، و در آن نیازی به تبدیل کامل به یک حالت بولی-منطقی نبود. این دیدگاهها به ما امکان بهبود کارایی قابل توجهی را میدهد، که معمولاً با یک مرتبه بزرگی بهتر از الگوریتمهای پسگرد قدیمی بود.
پروژه پوتسکو (Potassco) به صورت چتری برای بسیاری از سامانههای زیر عمل میکند، که شامل clasp، سامانههای زیرین (gringo)، سامانههای افزایشی (iclingo)، حلکنندههای محدودیتی (clingcon)، زبان عملی برای کامپایلرهای ASP یا (coala)، پیادهسازیهای MPI توزیعشده (claspar) و خیلی موارد دیگر است.
بیشتر این سامانهها از متغیرها پشتیبانی میکنند، اما فقط به صورت غیرمستقیم، با تحمیل زمینه، با استفاده از یک سامانه زمینی مثل Lparse or gringo به عنوان یک front-end. نیاز به زمینه میتواند منجر به یک انفجار ترکیبیاتی از بندها شود؛ از این رو سامانههایی که از زمینههای on-the-fly استفاده میکنند، میتوانند یک مزیت داشته باشند.
پیادهسازیهای پرسمانگرا از برنامهنویسی مجموعه جواب، مثل سامانه Galliwasp[15] و s(ASP)[16] و s(CASP)[17] از در اصل زمینه جلوگیری میکنند، این کار از طریق ترکیبی از رزلوشن و کواینداکشن انجام میشود.
Platform | Features | Mechanics | ||||||
---|---|---|---|---|---|---|---|---|
Name | OS | Licence | Variables | Function symbols | Explicit sets | Explicit lists | Disjunctive (choice rules) support | |
ASPeRiX | Linux | GPL | آری | نه | on-the-fly grounding | |||
ASSAT | Solaris | Freeware | SAT-solver based | |||||
Clasp Answer Set Solver | Linux, macOS, Windows | MIT License | Yes, in Clingo | آری | نه | نه | آری | incremental, SAT-solver inspired (nogood, conflict-driven) |
Cmodels | Linux, Solaris | GPL | Requires grounding | آری | incremental, SAT-solver inspired (nogood, conflict-driven) | |||
diff-SAT | Linux, macOS, Windows (Java Virtual Machine) | MIT License | Requires grounding | آری | SAT-solver inspired (nogood, conflict-driven). Supports solving probabilistic problems and answer set sampling | |||
DLV | Linux, macOS, Windows[18] | free for academic and non-commercial educational use, and for non-profit organizations[18] | آری | آری | نه | نه | آری | not Lparse compatible |
DLV-Complex | Linux, macOS, Windows | GPL | آری | آری | آری | آری | built on top of DLV — not Lparse compatible | |
GnT | Linux | GPL | Requires grounding | آری | built on top of smodels | |||
Jekejeke | Linux, macOS, Windows (Java Virtual Machine) | Proprietary | آری | آری | آری | DPLL Variant via Safe Forward Chaining | ||
nomore++ | Linux | GPL | combined literal+rule-based | |||||
Platypus | Linux, Solaris, Windows | GPL | distributed, multi-threaded nomore++, smodels | |||||
Pbmodels | Linux | ? | pseudo-boolean solver based | |||||
Smodels | Linux, macOS, Windows | GPL | Requires grounding | نه | نه | نه | نه | |
Smodels-cc | Linux | ? | Requires grounding | SAT-solver based; smodels w/conflict clauses | ||||
Sup | Linux | ? | SAT-solver based |
پانویس
- 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. Handbook of Knowledge Representation. Elsevier. pp. 285–316. ISBN 978-0-08-055702-1. as PDF بایگانیشده در ۲۰۱۶-۰۳-۰۳ توسط Wayback Machine
- Dimopoulos, Y.; Nebel, B.; Köhler, J. (1997). "Encoding planning problems in non-monotonic logic programs". In 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. pp. 273–285. ISBN 978-3-540-63912-1. as Postscript
- Subrahmanian, V.S.; Zaniolo, C. (1995). "Relating stable models and AI planning domains". In Sterling, Leon. Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming. MIT Press. pp. 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). "Stable models and an alternative logic programming paradigm". In Apt, Krzysztof R. The Logic programming paradigm: a 25-year perspective (PDF). Springer. pp. 169–181. arXiv:cs/9809032. ISBN 978-3-540-65463-6.
- Niemelä, I. (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.
- Lifschitz, V. (1999). "Action Languages, Answer Sets, and Planning". In Apt 1999, pp. 357–374
- 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. 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. pp. 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 (1–2): 45–74. arXiv:cs/0312045. doi:10.1017/S1471068403001923. as Postscript
- "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.
- Marple, Kyle.; Gupta, Gopal. (2012). "Galliwasp: A Goal-Directed Answer Set Solver". In Albert, Elvira. Logic-Based Program Synthesis and Transformation, 22nd International Symposium, LOPSTR 2012, Leuven, Belgium, September 18-20, 2012, Revised Selected Papers. Springer. pp. 122–136.
- Marple, K.; Salazar, E.; Gupta, G. (2017). "Computing Stable Models of Normal Logic Programs Without Grounding". CoRR. abs/1709.00501.
- 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.
- "DLV System company page". DLVSYSTEM s.r.l. Retrieved 16 November 2011.
منابع
مشارکتکنندگان ویکیپدیا. «Answer set programming». در دانشنامهٔ ویکیپدیای انگلیسی، بازبینیشده در ۳ ژوئن ۲۰۲۱.