Жауап жиын бағдарламалау: Қиын іздеу мәселелеріне шолу
Answer set programming
Жауап жинағы бағдарламалау (ASP) – қиын іздеу мәселелерін шешуге бағытталған декларативті бағдарламалау парадигмасы. Іздеуді жеңілдетеді, шешімдерді табуға көмектеседі.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Қиын іздеу мәселелеріне бағытталған бағдарламалау парадигмасы.
Programming paradigm focused on difficult search problems
Жауаптар жиынтығын бағдарламалау (ASP) — негізінен NP қиын мәселелер сияқты қиын іздеу мәселелеріне бағытталған декларативтік бағдарламалаудың бір түрі. Ол логикалық бағдарламалаудың тұрақты модель (жауаптар жиынтығы) семантикасына негізделген. ASP-да іздеу мәселелері тұрақты модельдерді есептеуге дейін тоғытылады, ал іздеуді жүзеге асыру үшін жауаптар жиынтығын шешушілер — тұрақты модельдерді құратын бағдарламалар пайдаланылады. Көптеген жауаптар жиынтығын шешушілерді жобалауда қолданылатын есептеу процесі DPLL алгоритмінің жетілдірілген нұсқасы болып табылады және принцип бойынша, ол әрқашан аяқталады (Prolog сұраныстарын бағалаудан өзгеше, ол шексіз циклға түсуі мүмкін). Әдеттегідей, ASP жауаптар жиынтығын білімді көрсету және логикалық қорыту салаларындағы қолданылуын, сондай-ақ осы салаларда туындайтын мәселелерді шешу үшін Prolog стиліндегі сұраныстарды бағалауды қамтиды.
Answer set programming (ASP) is a form of declarative programming oriented towards difficult (primarily NP hard) search problems. It is based on the stable model (answer set) semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers—programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm and, in principle, it always terminates (unlike Prolog query evaluation, which may lead to an infinite loop). In a more general sense, ASP includes all applications of answer sets to knowledge representation and reasoning and the use of Prolog style query evaluation for solving problems arising in these applications.
Үлкен топ
Графиктегі клика – жұп-жұп көршілес төбелердің жиынтығы. Келесі Lparse бағдарламасы берілген бағытталған графикте белгілі бір өлшемдегі кликаны табады немесе оның жоқ екенін анықтайды: n {in(X) : v(X)}. : in(X), in(Y), X!=Y, e(X,Y) болмауы. Бұл – «жасау және тексеру» ұйымдастыру принципінің тағы бір мысалы. 1-жолдағы таңдау ережесі белгілі бір саны бар төбелерден тұратын барлық жиынтықтарды «жасайды». 2-жолдағы шектеу клика емес жиынтықтарды «іріктеп тастайды».
A clique in a graph is a set of pairwise adjacent vertices. The following Lparse program finds a clique of size in a given directed graph, or determines that it does not exist:
n {in(X) : v(X)}. : in(X), in(Y), X!=Y, not e(X,Y). This is another example of the generate and test organization. The choice rule in Line 1 "generates" all sets consisting of vertices. The constraint in Line 2 "weeds out" the sets that are not cliques.
Гамильтон циклы
Бағытталған графтағы Гамильтон циклі – графтың әрбір төбесінен дәл бір рет өтетін цикл. Егер болса, берілген бағытталған графтағы Гамильтон циклін табу үшін келесі 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) : in(0,X), v(X). r(Y) : r(X), in(X,Y), e(X,Y). : not r(X), v(X). 1-жолдағы таңдау ережесі қабырғалар жиынының барлық ішкі жиынтықтарын «жасайды». Үш шектеу Гамильтон циклы емес ішкі жиынтықтарды «жояды». Соңғысы қосымша предикатты қолданады («0-дан қол жетімді») осы шартты орындамайтын төбелерді қабылдамау үшін. Бұл предикат 6 және 7-жолдарда рекурсивті түрде анықталады. Бұл бағдарлама «жасау, анықтау және тексеру» деген жалпы ұйымдастырудың мысалы болып табылады: ол бізге барлық «жаман» мүмкін шешімдерді жоюға көмектесетін қосымша предикаттың анықталуын қамтиды.
A Hamiltonian cycle in a directed graph is a cycle that passes through each vertex of the graph exactly once. The following Lparse program can be used to find a Hamiltonian cycle in a given directed graph if it exists; we assume that 0 is one of the vertices. {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). The choice rule in Line 1 "generates" all subsets of the set of edges. The three constraints "weed out" the subsets that are not Hamiltonian cycles. The last of them uses the auxiliary predicate (" is reachable from 0") to prohibit the vertices that do not satisfy this condition. This predicate is defined recursively in Lines 6 and 7. This program is an example of the more general "generate, define and test" organization: it includes the definition of an auxiliary predicate that helps us eliminate all "bad" potential solutions.
Тілдерді стандарттау және ASP конкурсы
ASP стандарттау жұмыс тобы ASP Core 2 деп аталатын стандартты тілдің сипаттамасын жасады, соңғы ASP жүйелері оған қарай бірігіп келеді. ASP Core 2 – Жауаптар жиынтығын бағдарламалау (Answer Set Programming) жарысының анықтамалық тілі болып табылады, онда ASP шешімдегіштері бірқатар анықтамалық мәселелер бойынша үнемі салыстырылып бағаланады.
The ASP standardization working group produced a standard language specification, called ASP Core 2, towards which recent ASP systems are converging. ASP Core 2 is the reference language for the Answer Set Programming Competition, in which ASP solvers are periodically benchmarked over a number of reference problems.
Іске асыруды салыстыру
Ертедегі жүйелер, мысалы, smodels, шешімдерді табу үшін кері іздеуді қолданды. Бульдік SAT шешімдерінің теориясы мен тәжірибесі дамыған сайын, ASSAT және Cmodels-ті қоса алғанда, көптеген ASP шешімдері SAT шешімдерінің үстіне салынды. Олар ASP формуласын SAT ұсыныстарына айналдырды, SAT шешімін қолданды, содан кейін шешімдерді ASP түріне қайта айналдырды. Clasp сияқты жақындағы жүйелер гибридтік тәсілді қолданады, SAT-тан шабыттанған, қақтығысқа негізделген алгоритмдерді пайдаланады, бірақ толығымен Бульдік логикалық формаға түрленбейді. Бұл тәсілдер өнімділіктің айтарлықтай жақсаруына мүмкіндік береді, көбінесе бұрынғы кері іздеу алгоритмдерінен бірнеше есе артық. Potassco жобасы төмендегі көптеген жүйелер үшін шатыр ретінде әрекет етеді, соның ішінде clasp, негіздеу жүйелері (gringo), инкременттік жүйелер (iclingo), шектеулерді шешушілер (clingcon), ASP компиляторларына әрекет ету тілі (coala), таратылған хабар алмасу интерфейсі (claspar) және тағы да басқалары. Көптеген жүйелер айнымалыларды қолдайды, бірақ тек жанама түрде, Lparse немесе gringo сияқты негіздеу жүйесін алдыңғы қатар ретінде пайдалану арқылы негіздеуді міндеттейді. Негіздеу қажеттілігі шарттардың комбинаторлық жарылысына әкелуі мүмкін; сондықтан, жүріс барысында негіздеуді орындайтын жүйелер артықшылыққа ие болуы мүмкін. Galliwasp жүйесі және s(CASP) сияқты жауап жиынтығын бағдарламалаудың сұрауға негізделген жүзеге асырылымдары, шешімділік және коиндукцияның комбинациясын пайдалану арқылы негіздеуден толығымен аулақ болады.
Early systems, such as smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict driven algorithms inspired by SAT, without fully converting into a Boolean logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms. The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language to ASP compilers (coala), distributed Message Passing Interface implementations (claspar), and many others. Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on the fly grounding might have an advantage. Query driven implementations of answer set programming, such as the Galliwasp system and s(CASP) avoid grounding altogether by using a combination of resolution and coinduction. Platform Features Mechanics Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) supportASPeRiX LinuxGPLon the fly groundingASSATSolarisFreewareSAT solver basedClasp Answer Set SolverLinux, macOS, WindowsMIT Licenseincremental, SAT solver inspired (nogood, conflict driven)CmodelsLinux, SolarisGPLincremental, SAT solver inspired (nogood, conflict driven)diff SATLinux, macOS, Windows (Java virtual machine)MIT LicenseSAT solver inspired (nogood, conflict driven). Supports solving probabilistic problems and answer set samplingDLVLinux, macOS, Windowsfree for academic and non commercial educational use, and for non profit organizationsnot Lparse compatibleDLV ComplexLinux, macOS, WindowsGPLbuilt on top of DLV — not Lparse compatibleGnTLinuxGPL built on top of smodelsnomore++LinuxGPLcombined literal+rule basedPlatypusLinux, Solaris, WindowsGPLdistributed, multi threaded nomore++, smodelsPbmodelsLinux?pseudo boolean solver basedSmodelsLinux, macOS, WindowsGPLSmodels cc Linux?SAT solver based; smodels w/conflict clausesSupLinux?SAT solver based
Platform Features Mechanics Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) supportASPeRiX LinuxGPLжүргізу кезінде негіздеуASSATSolarisFreewareSAT шешімдеріне негізделгенClasp Answer Set SolverLinux, macOS, WindowsMIT Licenseинкременттік, SAT шешімдерінен шабыттанған (жаман емес, қақтығысқа негізделген)CmodelsLinux, SolarisGPLинкременттік, SAT шешімдерінен шабыттанған (жаман емес, қақтығысқа негізделген)diff SATLinux, macOS, Windows (Java virtual machine)MIT LicenseSAT шешімдерінен шабыттанған (жаман емес, қақтығысқа негізделген). Ықтималдық мәселелерді шешуді және жауап жиынтығын үлгілеуді қолдайдыDLVLinux, macOS, Windowsакадемиялық және коммерциялық емес білім беру мақсатында тегін, сондай-ақ коммерциялық емес ұйымдар үшін жарамдыDLV ComplexLinux, macOS, WindowsGPLDLV-ге негізделген, Lparse-ке сәйкес келмейдіGnTLinuxGPL smodels-ке негізделгенnomore++LinuxGPLқұрама литераль+ережеге негізделгенPlatypusLinux, Solaris, WindowsGPLтаратылған, көп жіпті nomore++, smodelsPbmodelsLinux?pseudo boolean шешімдеріне негізделгенSmodelsLinux, macOS, WindowsGPLSmodels cc Linux?SAT шешімдеріне негізделген; smodels w/қақтығыс шарттарыSupLinux?SAT шешімдеріне негізделген
Early systems, such as smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict driven algorithms inspired by SAT, without fully converting into a Boolean logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms. The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language to ASP compilers (coala), distributed Message Passing Interface implementations (claspar), and many others. Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on the fly grounding might have an advantage. Query driven implementations of answer set programming, such as the Galliwasp system and s(CASP) avoid grounding altogether by using a combination of resolution and coinduction. Platform Features Mechanics Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) supportASPeRiX LinuxGPLon the fly groundingASSATSolarisFreewareSAT solver basedClasp Answer Set SolverLinux, macOS, WindowsMIT Licenseincremental, SAT solver inspired (nogood, conflict driven)CmodelsLinux, SolarisGPLincremental, SAT solver inspired (nogood, conflict driven)diff SATLinux, macOS, Windows (Java virtual machine)MIT LicenseSAT solver inspired (nogood, conflict driven). Supports solving probabilistic problems and answer set samplingDLVLinux, macOS, Windowsfree for academic and non commercial educational use, and for non profit organizationsnot Lparse compatibleDLV ComplexLinux, macOS, WindowsGPLbuilt on top of DLV — not Lparse compatibleGnTLinuxGPL built on top of smodelsnomore++LinuxGPLcombined literal+rule basedPlatypusLinux, Solaris, WindowsGPLdistributed, multi threaded nomore++, smodelsPbmodelsLinux?pseudo boolean solver basedSmodelsLinux, macOS, WindowsGPLSmodels cc Linux?SAT solver based; smodels w/conflict clausesSupLinux?SAT solver based