Шектеулермен логикалық бағдарламалау

Кіріспе

Шектеулерді қанағаттандырумен логикалық бағдарламалау

Шектеулерді қанағаттандырумен логикалық бағдарламалау – бұл шектеулерді бағдарламалаудың бір түрі, онда логикалық бағдарламалау шектеулерді қанағаттандырудан алынған ұғымдарды қосу арқылы кеңейтіледі. Шектеулі логикалық бағдарлама – бұл клаузалардың денесінде шектеулер бар логикалық бағдарлама. Шектеуді қамтитын клаузаның мысалы: Бұл клаузада – шектеу; A(X,Y), B(X) және C(Y) – қалыпты логикалық бағдарламалаудағыдай литералдар болып табылады. Бұл клауза A(X,Y) мәлімдемесінің орындалуына бір шартты белгілейді: X+Y нөлден үлкен және B(X) және C(Y) екеуі де дұрыс. Қалыпты логикалық бағдарламалаудағыдай, бағдарламаларға мақсаттың дәлелденуі туралы сұрақтар қойылады, олардың өзінде литералдармен қатар шектеулер де болуы мүмкін. Мақсаттың дәлелі – басқа клаузаларды қолдана отырып дәлелденетін қанағаттандырылатын шектеулер мен литералдардан тұратын клаузалар жиынтығы. Орындау интерпретатор арқылы жүзеге асырылады, ол мақсаттан басталып, мақсатты дәлелдеуге тырысатын клаузаларды рекурсивті түрде қарап шығады. Осы қарау кезінде кездесетін шектеулер «шектеулер қоймасы» деп аталатын жиынтыққа орналастырылады. Егер бұл жиынтық қанағаттандырылмайтын болып табылса, интерпретатор кері қайтады, мақсатты дәлелдеу үшін басқа клаузаларды қолдануға тырысады. Іс жүзінде, шектеулер қоймасының қанағаттандырылуы толық емес алгоритмді қолдану арқылы тексерілуі мүмкін, ол әрқашан сәйкессіздікті анықтап шығара бермейді.

Шолу

Формальды түрде, шектеу логикалық бағдарламалар тұрақты логикалық бағдарламаларға ұқсас, бірақ клаузалардың денесінде тұрақты логикалық бағдарламалау литералдарымен қатар шектеулер де болуы мүмкін. Мысалы, X>0 – бұл шектеу және келесі шектеу логикалық бағдарламаның соңғы клаузасында қамтылған. B(X,1): X<0. B(X,Y): X=1, Y>0. A(X,Y): X>0, B(X,Y). Тұрақты логикалық бағдарламалаудағыдай, A(X,1) сияқты мақсатты бағалау үшін Y=1 болғанда соңғы клаузаның денесін бағалау қажет. Тұрақты логикалық бағдарламалаудағыдай, бұл өз кезегінде B(X,1) мақсатын дәлелдеуді талап етеді. Тұрақты логикалық бағдарламалаудан өзгеше, бұл сонымен қатар шектеудің орындалуын талап етеді: X>0, соңғы клаузаның денесіндегі шектеу. (Тұрақты логикалық бағдарламалауда, X>0 толыққанды негізделген терминге байланысты болмаса, дәлелдеу мүмкін емес, және егер бұл жағдай болмаса, бағдарлама орындалуы сәтсіз аяқталады.) Шектеудің орындалуын кездескен кезде әрқашан анықтауға болмайды. Мысалы, бұл жағдайда соңғы клауза бағаланған кезде X-тің мәні анықталмайды. Нәтижесінде, X>0 шектеуі бұл сәтте орындалмайды да, бұзылмайды да. B(X,1) бағалауын жалғастырып, содан кейін X-тің нәтижесінде алынған мәні оң екенін тексерудің орнына, интерпретатор X>0 шектеуін сақтайды және содан кейін B(X,1) бағалауын жалғастырады; осылайша, интерпретатор B(X,1) бағалау кезінде X>0 шектеуінің бұзылуын анықтай алады және егер бұл орын алса, B(X,1) бағалауын күтудің орнына дереу кері қайтады. Жалпы, шектеу логикалық бағдарламаны бағалау тұрақты логикалық бағдарлама сияқты жүргізіледі. Дегенмен, бағалау кезінде кездесетін шектеулер «шектеу сақтағышы» деп аталатын жиынға орналастырылады. Мысалы, A(X,1) мақсатын бағалау Y=1 болғанда бірінші клаузаның денесін бағалау арқылы жүзеге асырылады; бұл бағалау X>0 шектеуін шектеу сақтағышына қосады және B(X,1) мақсатын дәлелдеуді талап етеді. Осы мақсатты дәлелдеуге тырысқанда, бірінші клауза қолданылады, бірақ оның бағалауы X<0 шектеуін шектеу сақтағышына қосады. Бұл қосылым шектеу сақтағышын қанағаттандырылмайтын етеді. Интерпретатор содан кейін кері қайтады және шектеу сақтағышынан соңғы қосылымды алып тастайды. Екінші клаузаны бағалау X=1 және Y>0 шектеуін шектеу сақтағышына қосады. Шектеу сақтағышы қанағаттандырылатындықтан және дәлелдеуге басқа литераль қалмағандықтан, интерпретатор X=1, Y=1 шешімімен тоқтайды.

Formally, constraint logic programs are like regular logic programs, but the body of clauses can contain constraints, in addition to the regular logic programming literals. As an example, X>0 is a constraint, and is included in the last clause of the following constraint logic program. B(X,1): X<0. B(X,Y): X=1, Y>0. A(X,Y): X>0, B(X,Y). Like in regular logic programming, evaluating a goal such as A(X,1) requires evaluating the body of the last clause with Y=1. Like in regular logic programming, this in turn requires proving the goal B(X,1). Contrary to regular logic programming, this also requires a constraint to be satisfied: X>0, the constraint in the body of the last clause. (In regular logic programming, X>0 cannot be proved unless X is bound to a fully ground term and execution of the program will fail if that is not the case.) Whether a constraint is satisfied cannot always be determined when the constraint is encountered. In this case, for example, the value of X is not determined when the last clause is evaluated. As a result, the constraint X>0 is neither satisfied nor violated at this point. Rather than proceeding in the evaluation of B(X,1) and then checking whether the resulting value of X is positive afterwards, the interpreter stores the constraint X>0 and then proceeds in the evaluation of B(X,1); this way, the interpreter can detect violation of the constraint X>0 during the evaluation of B(X,1), and backtrack immediately if this is the case, rather than waiting for the evaluation of B(X,1) to conclude. In general, the evaluation of a constraint logic program proceeds as does a regular logic program. However, constraints encountered during evaluation are placed in a set called a constraint store. As an example, the evaluation of the goal A(X,1) proceeds by evaluating the body of the first clause with Y=1; this evaluation adds X>0 to the constraint store and requires the goal B(X,1) to be proven. While trying to prove this goal, the first clause is applied but its evaluation adds X<0 to the constraint store. This addition makes the constraint store unsatisfiable. The interpreter then backtracks, removing the last addition from the constraint store. The evaluation of the second clause adds X=1 and Y>0 to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution X=1, Y=1.

Шарттар мен ережелер

Терминдердің әртүрлі анықтамалары қолданылады, осы арқылы әртүрлі шектеулер логикалық бағдарламалау түрлері пайда болады: ағаштар, нақты сандар немесе шекті домендер бойынша. Терминдердің теңдігі – әрқашан болатын шектеудің бір түрі. Мұндай шектеулер қажет, себебі интерпретатор P(t1) сөзбе-сөзін P(t2) басы бар жаңа варианттың денесімен ауыстырғанда t1=t2 теңдігін мақсатқа қосады.

Ағаш терминдері

Ағаш терминдерімен шектеу логикалық бағдарламалау, шектеулер қоймасында алмастыруларды шектеулер ретінде сақтап, тұрақты логикалық бағдарламалауды эмуляциялайды. Терминдер – басқа терминдерге қолданылатын айнымалылар, тұрақтылар және функциялық символдар. Қарастырылатын жалғыз шектеулер – терминдер арасындағы теңдіктер мен теңсіздіктер. Теңдік ерекше маңызды, себебі интерпретатор жиі t1=t2 сияқты шектеулерді жасайды. Терминдердегі теңдік шектеулерін біріктіру арқылы оңайлатуға, яғни шешуге болады: егер екі термин де басқа терминдерге қолданылатын функциялық символдар болса, t1=t2 шектеуін оңайлатуға болады. Егер екі функциялық символ да бірдей болса және қосалқы терминдердің саны да бірдей болса, бұл шектеуді қосалқы терминдердің жұптық теңдігімен алмастыруға болады. Егер терминдер әртүрлі функциялық символдардан құралған болса немесе бір функциядан, бірақ әртүрлі сандағы терминдерден тұрса, шектеу қанағаттандырылмайды. Егер екі терминнің бірі айнымалы болса, айнымалыға рұқсат етілген жалғыз мән – екінші термин. Нәтижесінде, екінші термин ағымдағы мақсатта және шектеулер қоймасында айнымалыны алмастыра алады, осылайша айнымалыны қарастырудан шығарып тастайды. Атап айтқанда, айнымалы өзімен тең болса, шектеу әрқашан қанағаттандырылған деп есептеліп, алынып тасталуы мүмкін. Бұл шектеуді қанағаттандыру түрінде айнымалы мәндері терминдер болып табылады.

Реалдар

Нақты сандармен шектелген логикалық бағдарламалау нақты өрнектерді термин ретінде пайдаланады. Функция белгілері қолданылмаған жағдайда, терминдер нақты сандардағы өрнектер болып табылады, және оларда айнымалылар болуы мүмкін. Мұндай жағдайда, әрбір айнымалы тек нақты санды ғана мән ретінде қабылдай алады. Нақтырақ айтқанда, терминдер – айнымалылар мен нақты тұрақтылар арқылы құрастырылған өрнектер. Терминдер арасындағы теңдік – әрқашан болатын шектеу түрі, себебі интерпретатор орындау барысында терминдердің теңдігін жасайды. Мысалы, егер ағымдағы мақсаттың бірінші литералы A(X+1) болса және интерпретатор A(Y 1): Y=1 деген клаузаны таңдаса, қайта жазудан кейін айнымалылар бойынша, ағымдағы мақсатқа қосылатын шектеулер X+1=Y 1 болады. Функция белгілері үшін қолданылатын оңайлату ережелері, әрине, қолданылмайды: X+1=Y 1 теңдеуі, бірінші өрнек + операторы арқылы, екіншісі болса басқаша құрастырылғандықтан, қанағаттандырылмайды. Нақты сандар мен функция белгілерін біріктіруге болады, нәтижесінде терминдер басқа терминдерге қолданылатын нақты сандар мен функция белгілері арқылы құрастырылған өрнектерге айналады. Формальды түрде, айнымалылар мен нақты тұрақтылар – басқа өрнектердегі кез келген арифметикалық оператор сияқты өрнектер болып табылады. Айнымалылар, тұрақтылар (нөлдік аритметикалық функция белгілері) және өрнектер – терминдерге қолданылатын кез келген функция белгісі сияқты терминдер болып табылады. Басқаша айтқанда, терминдер өрнектерден, ал өрнектер сандар мен айнымалылардан құралады. Бұл жағдайда, айнымалылар нақты сандар және терминдер арасында өзгереді. Яғни, бір айнымалы нақты санды, ал екіншісі терминді мән ретінде қабылдай алады. Екі терминнің теңдігін ағаш тәрізді терминдер үшін қолданылатын ережелер арқылы оңайлатуға болады, егер екі терминнің ешқайсысы нақты өрнек болмаса. Мысалы, егер екі терминнің функция белгісі мен субтерминдер саны бірдей болса, олардың теңдік шектеуін субтерминдердің теңдігімен алмастыруға болады.

Шекті домендер

Логикалық шектеулер бағдарламалауда қолданылатын шектеулердің үшінші класы – шекті домендер. Бұл жағдайда айнымалылардың мәндері шекті доменнен алынады, көбінесе бүтін сандардан. Әр айнымалы үшін әртүрлі доменді белгілеуге болады: мысалы, X::[1 5] дегеніміз, X мәні 1 мен 5 арасында екендігін білдіреді. Айнымалының доменін айнымалы алатын барлық мәндерді тізімдеу арқылы да беруге болады; сондықтан жоғарыдағы доменді декларацияны X::[1,2,3,4,5] деп те жазуға болады. Доменді белгілеудің осы екінші тәсілі X::[george,mary,john] сияқты бүтін сандардан құралмаған домендерге мүмкіндік береді. Егер айнымалының домені көрсетілмесе, ол тілде бейнеленетін бүтін сандар жиыны деп есептеледі. [X,Y,Z]::[1 5] сияқты декларацияны қолдана отырып, айнымалылар тобына бірдей доменді беруге болады. Айнымалының домені орындау кезінде қысқартылуы мүмкін. Шындығында, интерпретатор шектеулерді шектеу қоймасына қосқанда, ол жергілікті сәйкестіктің бір түрін қамтамасыз ету үшін шектеулерді таратуды жүзеге асырады, және бұл операциялар айнымалылардың доменін азайтуы мүмкін. Егер айнымалының домені бос болса, шектеулер қоймасы сәйкессіз болады, ал алгоритм кері қадам жасайды. Егер айнымалының домені жеке элементтен тұрса, айнымалыға оның доменіндегі бірегей мәнді тағайындауға болады. Әдетте қолданылатын сәйкестік түрлері – доғалық сәйкестік, гипердоғалық сәйкестік және шекаралық сәйкестік. Өзгергіштің ағымдағы доменін тексеру үшін нақты литеральдарды пайдалануға болады; мысалы, dom(X,D) X өзгергіштің ағымдағы доменін D ретінде анықтайды. Нақты сандардың домендеріне келетін болсақ, бүтін сандар домендерімен функторларды қолдануға болады. Бұл жағдайда термин бүтін сандардағы өрнек, тұрақты немесе басқа терминдерге функтордың қолданылуы болуы мүмкін. Егер өзгергіштің домені бүтін сандар немесе тұрақтылар жиыны ретінде көрсетілмесе, ол кез келген терминді мән ретінде қабылдауы мүмкін.

Шектеулер қоймасы

Шектеулер қоймасы қазіргі уақытта қанағаттандырылатыны болжамдалған шектеулерді қамтиды. Оны жүйелі логикалық бағдарламалаудағы ағымдағы алмастыру ретінде қарастыруға болады. Тек ағаш тәрізді терминдерге рұқсат болғанда, шектеулер қоймасында t1=t2 түріндегі шектеулер болады; бұл шектеулер біріктіру арқылы қарапайымдатылады, нәтижесінде өзгермелі=термин түріндегі шектеулер пайда болады; мұндай шектеулер алмастыруға баламалы. Дегенмен, егер терминдер арасындағы тең еместік рұқсат етілсе, шектеулер қоймасында t1!=t2 түріндегі шектеулер де болуы мүмкін. Нақты сандар немесе шекті домендер бойынша шектеулерге рұқсат болғанда, шектеулер қоймасында X+2=Y/2 сияқты доменге тән шектеулер де болуы мүмкін. Шектеулер қоймасы ағымдағы алмастыру тұжырымын екі жағынан кеңейтеді. Біріншіден, ол жаңа варианттың басымен сәйкес келетін сөз тіркесінен туындаған шектеулерді ғана емес, сонымен қатар сөз тіркесінің денесіндегі шектеулерді де қамтиды. Екіншіден, ол тек өзгермелі=мәнді түріндегі шектеулерді ғана емес, сонымен қатар қарастырылып отырған шектеу тіліне қатысты шектеулерді де қамтиды. Жүйелі логикалық бағдарламаның сәтті орындалуының нәтижесі соңғы алмастыру болса, шектеу логикалық бағдарламаның нәтижесі соңғы шектеулер қоймасы болып табылады, ол өзгермелі=мәнді түріндегі шектеулерді қамтуы мүмкін, бірақ жалпы жағдайда кез келген шектеулерді қамтуы мүмкін. Доменге тән шектеулер сөз тіркесінің денесінен де, сөз тіркесін сөз тіркесінің басымен сәйкестендіруден де шектеулер қоймасына түсуі мүмкін: мысалы, егер интерпретатор A(X+2) сөз тіркесін A(Y/2) басы болатын жаңа вариантты сөз тіркесімен қайта жазса, X+2=Y/2 шектеуі шектеулер қоймасына қосылады. Егер айнымалы нақты сан немесе шекті домендік өрнекте пайда болса, ол тек нақты сан немесе шекті домендегі мәнді қабылдай алады. Мұндай айнымалы басқа терминдерге қолданылатын функтордан құралған терминді мән ретінде қабылдамайды. Шектеулер қоймасы қанағаттандырылмайды, егер айнымалы белгілі бір доменнің мәнін де, терминдерге қолданылатын функторды да қабылдауға міндетті болса. Шектеу қоймасына шектеу қосылғаннан кейін, оның үстінде бірнеше операциялар орындалады. Орындалатын операциялар қарастырылып отырған домен мен шектеулерге байланысты. Мысалы, шекті ағаш теңдіктері үшін біріктіру, нақты сандардағы көпмүшелік теңдеулер үшін айнымалыларды жою, шекті домендер үшін жергілікті сәйкестіктің бір түрін сақтау үшін шектеу тарату қолданылады. Бұл операциялар шектеулер қоймасын қанағаттандыруға тексеру және шешуді жеңілдетуге бағытталған. Бұл операциялардың нәтижесінде жаңа шектеулердің қосылуы ескі шектеулерді өзгерте алады. Интерпретатор осы өзгерістерді кері қайтара білуі маңызды. Ең қарапайым әдіс – интерпретатордың әр таңдау жасаған сайын қойманың толық күйін сақтауы (ол мақсатты қайта жазу үшін сөз тіркесін таңдайды). Шектеулер қоймасын бұрынғы күйіне қайтаруға мүмкіндік беретін тиімді әдістер де бар. Атап айтқанда, екі таңдау нүктесі арасында шектеулер қоймасында жасалған өзгерістерді, соның ішінде ескі шектеулерге енгізілген өзгерістерді сақтау жеткілікті. Бұл өзгертілген шектеулердің ескі мәнін сақтау арқылы жасалуы мүмкін; бұл әдіс іздеу деп аталады. Көбірек жетілдірілген әдіс – өзгертілген шектеулерге енгізілген өзгерістерді сақтау. Мысалы, сызықтық шектеу оның коэффициентін өзгерту арқылы өзгертіледі: ескі және жаңа коэффициент арасындағы айырманы сақтау өзгерісті кері қайтаруға мүмкіндік береді. Бұл екінші әдіс семантикалық кері ілгерілеу деп аталады, өйткені өзгерістің семантикасы ғана сақталады, шектеулердің ескі нұсқасы емес.

The constraint store contains the constraints that are currently assumed satisfiable. It can be considered what the current substitution is for regular logic programming. When only tree terms are allowed, the constraint store contains constraints in the form t1=t2; these constraints are simplified by unification, resulting in constraints of the form variable=term; such constraints are equivalent to a substitution. However, the constraint store may also contain constraints in the form t1!=t2, if the difference != between terms is allowed. When constraints over reals or finite domains are allowed, the constraint store may also contain domain specific constraints like X+2=Y/2, etc. The constraint store extends the concept of current substitution in two ways. First, it does not only contain the constraints derived from equating a literal with the head of a fresh variant of a clause, but also the constraints of the body of clauses. Second, it does not only contain constraints of the form variable=value but also constraints on the considered constraint language. While the result of a successful evaluation of a regular logic program is the final substitution, the result for a constraint logic program is the final constraint store, which may contain constraint of the form variable=value but in general may contain arbitrary constraints. Domain specific constraints may come to the constraint store both from the body of a clauses and from equating a literal with a clause head: for example, if the interpreter rewrites the literal A(X+2) with a clause whose fresh variant head is A(Y/2), the constraint X+2=Y/2 is added to the constraint store. If a variable appears in a real or finite domain expression, it can only take a value in the reals or the finite domain. Such a variable cannot take a term made of a functor applied to other terms as a value. The constraint store is unsatisfiable if a variable is bound to take both a value of the specific domain and a functor applied to terms. After a constraint is added to the constraint store, some operations are performed on the constraint store. Which operations are performed depends on the considered domain and constraints. For example, unification is used for finite tree equalities, variable elimination for polynomial equations over reals, constraint propagation to enforce a form of local consistency for finite domains. These operations are aimed at making the constraint store simpler to be checked for satisfiability and solved. As a result of these operations, the addition of new constraints may change the old ones. It is essential that the interpreter is able to undo these changes when it backtracks. The simplest case method is for the interpreter to save the complete state of the store every time it makes a choice (it chooses a clause to rewrite a goal). More efficient methods for allowing the constraint store to return to a previous state exist. In particular, one may just save the changes to the constraint store made between two points of choice, including the changes made to the old constraints. This can be done by simply saving the old value of the constraints that have been modified; this method is called trailing. A more advanced method is to save the changes that have been done on the modified constraints. For example, a linear constraint is changed by modifying its coefficient: saving the difference between the old and new coefficient allows reverting a change. This second method is called semantic backtracking,
because the semantics of the change is saved rather than the old version of the constraints only.

Таңбалау

Жазылу литералдары шекті домендердегі айнымалыларда шектеу сақтаудың қанағаттандырылуын немесе ішінара қанағаттандырылуын тексеру және қанағаттандыратын тағайындаманы табу үшін қолданылады. Жазылу литералы – labeling([айнымалылар]) түрінде болады, мұнда аргумент – шекті домендердегі айнымалылардың тізімі. Интерпретатор мұндай литералды бағалағанда, тізімдегі айнымалылардың домендерінде барлық тиісті шектеулерді қанағаттандыратын тағайындаманы табу үшін іздеу жүргізеді. Әдетте, бұл кері іздеудің бір түрімен жасалады: айнымалылар әрқайсысы үшін барлық мүмкін мәндерді сынап, сәйкессіздік анықталғанда кері іздеу арқылы бағаланады. Жазылу литералының бірінші қолданылуы – шектеу сақтаудың нақты қанағаттандырылуын немесе ішінара қанағаттандырылуын тексеру. Интерпретатор шектеу сақтау қоймасына шектеуді қосқанда, ол тек жергілікті сәйкестіктің бір түрін ғана қолданады. Бұл операция, егер шектеу сақтау қанағаттандырылмаса да, сәйкессіздікті анықтамауы мүмкін. Айнымалылар жиынтығына жазылу литералын қолдану осы айнымалылар бойынша шектеулердің қанағаттандырылуын тексереді. Нәтижесінде, шектеу сақтау қоймасында көрсетілген барлық айнымалыларды пайдалану қойманың қанағаттандырылуын тексеруге әкеледі. Жазылу литералының екінші қолданылуы – шектеуді сақтауды қанағаттандыратын айнымалылардың бағалауын нақты анықтау. Жазылу литералы болмаса, айнымалыларға тек қана шектеу сақтау қоймасында X=мәні түріндегі шектеулер болған кезде және жергілікті сәйкестік айнымалының доменін бір ғана мәнге дейін азайтатын кезде ғана мәндер беріледі. Кейбір айнымалыларға жазылу литералын қолдану осы айнымалыларды бағалауға мәжбүрлейді. Басқаша айтқанда, жазылу литералы қарастырылғаннан кейін барлық айнымалыларға мән беріледі. Әдетте, шектеу логикасы бағдарламалары шектеулер қоймасында мүмкіндігінше көп шектеулер жинақталғаннан кейін ғана жазылу литералдары бағаланатын етіп жазылады. Себебі, жазылу литералдары іздеуді талап етеді, ал егер қанағаттандырылатын шектеулер көп болса, іздеу тиімдірек болады. Шектеулерді қанағаттандыру мәселесі әдетте келесі құрылымды шектеу логикалық бағдарламасымен шешіледі:

The labeling literals are used on variables over finite domains to check satisfiability or partial satisfiability of the constraint store and to find a satisfying assignment. A labeling literal is of the form labeling([variables]), where the argument is a list of variables over finite domains. Whenever the interpreter evaluates such a literal, it performs a search over the domains of the variables of the list to find an assignment that satisfies all relevant constraints. Typically, this is done by a form of backtracking: variables are evaluated in order, trying all possible values for each of them, and backtracking when inconsistency is detected. The first use of the labeling literal is to actual check satisfiability or partial satisfiability of the constraint store. When the interpreter adds a constraint to the constraint store, it only enforces a form of local consistency on it. This operation may not detect inconsistency even if the constraint store is unsatisfiable. A labeling literal over a set of variables enforces a satisfiability check of the constraints over these variables. As a result, using all variables mentioned in the constraint store results in checking satisfiability of the store. The second use of the labeling literal is to actually determine an evaluation of the variables that satisfies the constraint store. Without the labeling literal, variables are assigned values only when the constraint store contains a constraint of the form X=value and when local consistency reduces the domain of a variable to a single value. A labeling literal over some variables forces these variables to be evaluated. In other words, after the labeling literal has been considered, all variables are assigned a value. Typically, constraint logic programs are written in such a way labeling literals are evaluated only after as many constraints as possible have been accumulated in the constraint store. This is because labeling literals enforce search, and search is more efficient if there are more constraints to be satisfied. A constraint satisfaction problem is typical solved by a constraint logic program having the following structure:

Интерпретатор solve(аргументтер) мақсатын бағалағанда, ол бірінші ережесінің жаңа нұсқасының денесін ағымдағы мақсатқа орналастырады. Бірінші мақсат constraints(X') болғандықтан, екінші ереже бағаланады және бұл операция барлық шектеулерді ағымдағы мақсатқа және ақырында шектеу сақтау қоймасына көшіреді. Содан кейін labeling(X') литералы бағаланады, бұл шектеу сақтау қоймасының шешімін іздеуге мәжбүрлейді. Шектеу сақтау қоймасында бастапқы шектеулерді қанағаттандыру мәселесінің шектеулері дәл болғандықтан, бұл операция бастапқы мәселенің шешімін іздейді.

Бағдарламаның қайта құрылуы

Берілген шектеу логикалық бағдарлама тиімділігін арттыру үшін қайта құрылуы мүмкін. Бірінші ереже – таңбаланған литеральдарға мүмкіндігінше көп шектеулер жинақталғаннан кейін ғана таңбалау литеральдары орналастырылуы керек. Теориялық тұрғыдан алғанда, , интерпретатор таңбалау литералын кездестіргенде орындалатын іздеу X>0 шектеуін қамтымайтын шектеу қоймасында жүзеге асырылады. Нәтижесінде, ол X=1 сияқты шешімдерді тудыруы мүмкін, бұл шешімдер кейіннен бұл шектеуді қанағаттандырмайды. Екінші нұсқада іздеу тек қана шектеу X>0 шектеу қоймасында болған кезде ғана орындалады. Сәйкессіздіктерді ертерек анықтауға мүмкіндік беретін қосымша шектеулер іздеу кеңістігін қысқартады, нәтижесінде іздеу тек осы шектеуге сәйкес келетін шешімдерді ғана қайтарады. Тиімділікті арттыруға мүмкіндік беретін екінші қайта құру – бұл сөйлемдердің денесінде литеральдардың алдына шектеулерді қою. Тағы да айта кетейік, және принципте эквивалентті. Дегенмен, бірінші жағдайда көбірек есептеулер қажет болуы мүмкін. Мысалы, егер шектеу қоймасында X<2 шектеуі болса, интерпретатор бірінші жағдайда B(X) функциясын рекурсивті түрде бағалайды; егер ол сәтті аяқталса, онда X>0 шектеуін қосу кезінде шектеу қоймасы сәйкессіз екенін анықтайды. Екінші жағдайда, осы сөйлемді бағалау кезінде интерпретатор алдымен X>0 шектеуін шектеу қоймасына қосады, содан кейін, мүмкін, B(X) функциясын бағалайды. X>0 шектеуін қосылғаннан кейін шектеу қоймасы сәйкессіз болып шықса, B(X) функциясының рекурсивті бағалануы мүлдем орындалмайды. Үшінші қайта құру, тиімділікті арттыруға мүмкіндік береді – артық шектеулерді қосу. Егер бағдарламашы белгілі бір шектеуді қанағаттандыратын мәселенің шешімін білсе, ол бұл шектеуді қосып, шектеу қоймасының сәйкессіздігін мүмкіндігінше ертерек тудыруы мүмкін. Мысалы, егер B(X) функциясын бағалау X үшін оң мәнге әкелетіні алдын ала белгілі болса, бағдарламашы B(X) функциясының кез келген пайда болуынан бұрын X>0 шектеуін қосуы мүмкін. Мысалы, A(X,Y): B(X),C(X) мақсаты A(2,Z) үшін сәтсіз аяқталады, бірақ бұл тек B(X) қосалқы мақсатын бағалау кезінде анықталады. Екінші жағынан, егер жоғарыдағы сөйлем , арқылы ауыстырылса, интерпретатор X>0 шектеуін шектеу қоймасына қосылған кезде кері қадам жасайды, бұл B(X) функциясын бағалау басталғанға дейін болады.

A given constraint logic program may be reformulated to improve its efficiency. A first rule is that labeling literals should be placed after as much constraints on the labeled literals are accumulated in the constraint store. While in theory is equivalent to , the search that is performed when the interpreter encounters the labeling literal is on a constraint store that does not contain the constraint X>0. As a result, it may generate solutions, such as X= 1, that are later found out not to satisfy this constraint. On the other hand, in the second formulation the search is performed only when the constraint is already in the constraint store. As a result, search only returns solutions that are consistent with it, taking advantage of the fact that additional constraints reduce the search space. A second reformulation that can increase efficiency is to place constraints before literals in the body of clauses. Again, and are in principle equivalent. However, the first may require more computation. For example, if the constraint store contains the constraint X< 2, the interpreter recursively evaluates B(X) in the first case; if it succeeds, it then finds out that the constraint store is inconsistent when adding X>0. In the second case, when evaluating that clause, the interpreter first adds X>0 to the constraint store and then possibly evaluates B(X). Since the constraint store after the addition of X>0 turns out to be inconsistent, the recursive evaluation of B(X) is not performed at all. A third reformulation that can increase efficiency is the addition of redundant constraints. If the programmer knows (by whatever means) that the solution of a problem satisfies a specific constraint, they can include that constraint to cause inconsistency of the constraint store as soon as possible. For example, if it is known beforehand that the evaluation of B(X) will result in a positive value for X, the programmer may add X>0 before any occurrence of B(X). As an example, A(X,Y): B(X),C(X) will fail on the goal A( 2,Z), but this is only found out during the evaluation of the subgoal B(X). On the other hand, if the above clause is replaced by , the interpreter backtracks as soon as the constraint X>0 is added to the constraint store, which happens before the evaluation of B(X) even starts.

Бір мезгілдегі шектеу логикасын бағдарламалау

Шектеу логикасы бағдарламалаудың бір мезгілдегі нұсқалары шектеуді қанағаттандыру мәселелерін шешуден гөрі бір мезгілдегі процестерді бағдарламалауға бағытталған. Шектеу логикасы бағдарламалаудағы мақсаттар бір мезгілде бағаланады; сондықтан бір мезгілдегі процесс интерпретатордың мақсатты бағалауы ретінде бағдарламаланады. Синтаксистік тұрғыдан, бір мезгілдегі шектеу логикалық бағдарламалары бір мезгілде емес бағдарламаларға ұқсас, тек ерекшелігі – бұл ережелерге күзетшілер кіреді, олар кейбір жағдайларда ережелердің қолданылуын тоқтататын шектеулер болып табылады. Семантикалық жағынан, бір мезгілдегі шектеу логикалық бағдарламалау бір мезгілде емес нұсқалардан ерекшеленеді, өйткені мақсатты бағалау проблемаға шешім табудың орнына бір мезгілдегі процесті жүзеге асыруды көздейді. Ең бастысы, бұл айырмашылық интерпретатордың бірден көп ереже қолданылған кезде қалай әрекет ететіндігіне әсер етеді: бір мезгілде емес шектеу логикасы бағдарламалауы барлық ережелерді рекурсивті түрде сынап көреді; бір мезгілдегі шектеу логикасы бағдарламалауы тек біреуін таңдайды. Бұл интерпретатордың бұрын қабылдаған шешімін қайта қарамайтынының ең айқын көрінісі. Бұның басқа да әсерлері бар – бүкіл бағалау сәтсіз аяқталмаса да, дәлелдеуге келмейтін мақсаттың болуының семантикалық мүмкіндігі және мақсатты ереже басымен теңестірудің ерекше тәсілі.

Қолданбалар

Шектеу логикалық бағдарламалау автоматтандырылған кестелеу, типтік қорытынды, азаматтық инженерия, механикалық инженерия, цифрлық тізбектерді тексеру, әуе трафигін басқару, қаржы және тағы да басқа салаларда қолданылған.

Тарих

Шектеулі логикалық бағдарламалау 1987 жылы Джаффар мен Лассез енгізді. Олар Prolog II терминдерінің теңдеулері мен теңдесу еместіктері шектеулердің нақты бір түрі екенін байқады және бұл идеяны кез келген шектеу тілдеріне жалпылады. Осы тұжырымдаманың алғашқы іске асырылымдары Prolog III, CLP(R) және CHIP болды.