Logické programování omezení - Constraint logic programming

Logické programování omezení je forma omezovacího programování , ve kterém je logické programování rozšířeno o koncepty z uspokojení omezení . Logický program omezení je logický program, který obsahuje omezení v těle klauzulí. Příklad klauzule zahrnující omezení je . V této klauzuli je omezení; , A jsou literály jsou v pravidelném logické programování. Tato klauzule uvádí jednu podmínku, za které platí prohlášení : je větší než nula a obě a jsou pravdivé. A(X,Y) :- X+Y>0, B(X), C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

Stejně jako v běžném logickém programování jsou programy dotazovány na prokazatelnost cíle, který může kromě literálů obsahovat i omezení. Důkaz pro cíl se skládá z klauzulí, jejichž těla jsou uspokojivá omezení, a z doslovů, které lze zase dokázat pomocí jiných klauzulí. Popravu provádí tlumočník, který začíná od cíle a rekurzivně skenuje klauzule snažící se dokázat cíl. Omezení zjištěná během tohoto skenování jsou umístěna do sady s názvem úložiště omezení . Pokud se zjistí, že tato sada je neuspokojivá, tlumočník ustoupí a pokusí se použít jiné klauzule k prokázání cíle. V praxi lze uspokojivost úložiště omezení zkontrolovat pomocí neúplného algoritmu, který ne vždy zjistí nekonzistenci.

Přehled

Formálně jsou programy s logikou omezení jako běžné logické programy, ale tělo klauzulí může kromě pravidelných logických programovacích literálů obsahovat omezení. Jako příklad X>0je omezení a je zahrnuto v poslední klauzuli následujícího programu logiky omezení.

B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).

Stejně jako v běžném logickém programování, vyhodnocení cíle, jako je, A(X,1)vyžaduje vyhodnocení těla poslední klauzule pomocí Y=1. Stejně jako v běžném logickém programování to zase vyžaduje prokázání cíle B(X,1). Na rozdíl od pravidelného logického programování to také vyžaduje splnění omezení: X>0omezení v těle poslední klauzule (v pravidelném logickém programování nelze X> 0 prokázat, pokud X není vázáno na plně základní termín a provedení program selže, pokud tomu tak není).

Zda je omezení splněno, nelze vždy určit, když se na omezení narazí. V tomto případě například není hodnota Xvyhodnocena při vyhodnocení poslední klauzule. V důsledku toho X>0není v tuto chvíli omezení splněno ani porušeno. Místo toho , aby tlumočník pokračoval ve vyhodnocování B(X,1)a poté zkontroloval, zda je výsledná hodnota hodnoty Xkladná, uloží omezení X>0a poté pokračuje v hodnocení B(X,1); tímto způsobem může tlumočník detekovat porušení omezení X>0během vyhodnocování B(X,1)a okamžitě se vrátit, pokud tomu tak je, místo čekání na vyhodnocení B(X,1)závěru.

Obecně platí, že vyhodnocení programu logiky omezení probíhá stejně jako běžný program logiky. Omezení zjištěná během vyhodnocování jsou však umístěna v sadě nazývané úložiště omezení. Vyhodnocení cíle například A(X,1)pokračuje hodnocením textu první klauzule pomocí Y=1; toto hodnocení přidává X>0do úložiště omezení a vyžaduje, aby byl cíl B(X,1)prokázán. Při pokusu o prokázání tohoto cíle je použita první klauzule, ale její vyhodnocení přidává X<0úložiště omezení. Toto přidání činí obchod s omezeními neuspokojivým. Tlumočník pak ustoupí a odebere poslední přírůstek z úložiště omezení. Vyhodnocení druhé klauzule přidá X=1a Y>0do úložiště omezení. Vzhledem k tomu, že úložiště omezení je uspokojivé a nezbývá než dokázat žádný jiný doslovný překlad, tlumočník s řešením přestane X=1, Y=1.

Sémantika

Sémantiku programů logiky omezení lze definovat pomocí virtuálního tlumočníka, který udržuje pár během provádění. První prvek této dvojice se nazývá aktuální cíl; druhý prvek se nazývá úložiště omezení. Současným cílem obsahuje literály interpret se snaží dokázat, a může také obsahovat určitá omezení se snaží uspokojit; store omezení obsahuje všechny vazby interpret převzala splnitelná doposud. ${\ displaystyle \ langle G, S \ rangle}$

Zpočátku je aktuálním cílem cíl a úložiště omezení je prázdné. Tlumočník pokračuje odstraněním prvního prvku z aktuálního cíle a jeho analýzou. Podrobnosti této analýzy jsou vysvětleny níže, ale nakonec tato analýza může způsobit úspěšné ukončení nebo selhání. Tato analýza může zahrnovat rekurzivní volání a přidání nových literálů k aktuálnímu cíli a nové omezení do úložiště omezení. Pokud dojde k vygenerování selhání, tlumočník ustoupí. Úspěšné ukončení je generováno, když je aktuální cíl prázdný a úložiště omezení je uspokojivé.

Podrobnosti o analýze doslovně odstraněného z cíle jsou následující. Poté, co odstraníte tento literál z přední části cíle, zkontroluje se, zda se jedná o omezení nebo doslovný. Pokud se jedná o omezení, přidá se do úložiště omezení. Pokud je to doslovné, je vybrána klauzule, jejíž hlava má stejný predikát doslovného; klauzule se přepíše nahrazením jejích proměnných novými proměnnými (proměnné, které se v cíli nevyskytují): výsledek se nazývá nová varianta klauzule; tělo čerstvé varianty klauzule je pak umístěno před branku; rovnost každého argumentu doslovného textu s odpovídající jedním z čerstvých variantních hlav je také umístěna před branku.

Během těchto operací se provádějí některé kontroly. Zejména je u úložiště omezení zkontrolována konzistence pokaždé, když je do něj přidáno nové omezení. V zásadě platí, že kdykoli je úložiště omezení nevyhovující, může algoritmus ustoupit. Kontrola neuspokojivosti v každém kroku by však byla neúčinná. Z tohoto důvodu lze místo toho použít neúplnou kontrolu spokojenosti. V praxi je splnitelnost kontrolována pomocí metod, které úložiště omezení zjednodušují, to znamená přepsat jej do ekvivalentní, ale jednodušeji řešitelné formy. Tyto metody mohou někdy, ale ne vždy prokázat neuspokojitelnost neuspokojitelného úložiště omezení.

Tlumočník prokázal cíl, když je aktuální cíl prázdný a úložiště omezení není detekováno jako nesplnitelné. Výsledkem provedení je aktuální sada (zjednodušených) omezení. Tato sada může obsahovat omezení, jako je vynucení proměnných na konkrétní hodnotu, ale může také zahrnovat omezení, jako jsou pouze vázané proměnné, aniž by jim byla přidělena konkrétní hodnota. ${\ displaystyle X = 2}$${\ displaystyle X> 2}$

Formálně je sémantika omezovacího logického programování definována z hlediska derivací . Přechod je dvojice párů cíl/obchod, poznamenal . Taková dvojice uvádí možnost přechodu ze státu do stavu . Takový přechod je možný ve třech možných případech: ${\ Displaystyle \ langle G, S \ rangle \ rightarrow \ langle G ', S' \ rangle}$${\ displaystyle \ langle G, S \ rangle}$${\ displaystyle \ langle G ', S' \ rangle}$

• prvek G je vazba C , a ; jinými slovy, omezení lze přesunout z cíle do úložiště omezení${\ displaystyle G '= G \ zpětné lomítko \ {C \}}$${\ Displaystyle S '= S \ cup \ {C \}}$
• prvek G je doslovný , existuje klauzule, že přepsána pomocí nové proměnné, je , je G se nahrazuje , a ; jinými slovy, doslovný výraz lze nahradit tělem nové varianty klauze, která má v hlavě stejný predikát, přičemž k cíli přidáme tělo nové varianty a výše uvedené rovnosti výrazů${\ Displaystyle L (t_ {1}, \ ldots, t_ {n})}$${\ Displaystyle L (t_ {1} ', \ ldots, t_ {n}'):-B}$${\ displaystyle G '}$${\ Displaystyle L (t_ {1}, \ ldots, t_ {n})}$${\ Displaystyle t_ {1} = t_ {1} ', \ ldots, t_ {n} = t_ {n}', B}$${\ displaystyle S '= S}$
• S a jsou ekvivalentní podle specifické sémantiky omezení${\ displaystyle S '}$

Sekvence přechodů je derivace. Cíl G může být prokázáno, zda existuje původ od do nějakého splnitelná omezení ukládání S . Tato sémantika formalizuje možný vývoj tlumočníka, který si libovolně zvolí doslovný cíl, který má zpracovat, a klauzuli, která nahradí doslovné výrazy. Jinými slovy, cíl je v rámci této sémantiky prokázán, pokud existuje řada možností doslovných a klauzulí, mezi možnými mnoha, které vedou k prázdnému cíli a uspokojivému obchodu. ${\ displaystyle \ langle G, \ emptyset \ rangle}$${\ displaystyle \ langle \ emptyset, S \ rangle}$

Skuteční tlumočníci zpracovávají prvky cíle v LIFO pořadí: prvky se přidávají vpředu a zpracovávají se zepředu. Rovněž volí klauzuli druhého pravidla podle pořadí, ve kterém jsou zapsána, a přepisují úložiště omezení, když je změněno.

Třetím možným druhem přechodu je nahrazení úložiště omezení ekvivalentním. Tato náhrada je omezena na ty, které jsou prováděny specifickými metodami, jako je šíření omezení . Sémantika programování logiky omezení je parametrická nejen pro druh použitých vazeb, ale také pro metodu pro přepis úložiště omezení. Konkrétní metody používané v praxi nahrazují úložiště omezení metodou, jejíž řešení je jednodušší. Pokud je úložiště omezení nevyhovující, může toto zjednodušení někdy tuto neuspokojitelnost zjistit, ale ne vždy.

Výsledek vyhodnocení cíle proti programu logiky omezení je definován, pokud je cíl prokázán. V tomto případě existuje odvození od počátečního páru k páru, kde je cíl prázdný. Úložiště omezení tohoto druhého páru je považováno za výsledek vyhodnocení. Důvodem je, že úložiště omezení obsahuje všechna omezení považovaná za splnitelná k prokázání cíle. Jinými slovy, cíl je prokázán u všech proměnných hodnocení, která splňují tato omezení.

Párová rovnost výrazů dvou literálů je často kompaktně označována : toto je zkratka pro omezení . Běžná varianta sémantiky pro programování logiky omezení se přidává přímo do úložiště omezení, nikoli do cíle. ${\ Displaystyle L (t_ {1}, \ ldots, t_ {n}) = L (t_ {1} ', \ ldots, t_ {n}')}$${\ displaystyle t_ {1} = t_ {1} ', \ ldots, t_ {n} = t_ {n}'}$${\ Displaystyle L (t_ {1}, \ ldots, t_ {n}) = L (t_ {1} ', \ ldots, t_ {n}')}$

Pravidla a podmínky

Používají se různé definice termínů, které generují různé druhy omezovacího logického programování: přes stromy, reality nebo konečné domény. Druhem omezení, které je vždy přítomno, je rovnost výrazů. Taková omezení jsou nezbytná, protože tlumočník přidává t1=t2k cíli, kdykoli je doslovný text P(...t1...)nahrazen tělem nové varianty klauzule, jejíž hlava je P(...t2...).

Stromové termíny

Logické programování omezení pomocí stromových výrazů emuluje pravidelné logické programování ukládáním náhrad jako omezení v úložišti omezení. Termíny jsou proměnné, konstanty a funkční symboly používané pro jiné termíny. Jediná uvažovaná omezení jsou rovnosti a nerovnosti mezi podmínkami. Rovnost je obzvláště důležitá, protože taková omezení t1=t2jsou často generována tlumočníkem. Omezení rovnosti podmínek lze zjednodušit, což je vyřešeno sjednocením :

Omezení t1=t2lze zjednodušit, pokud jsou oba termíny funkční symboly aplikované na jiné termíny. Pokud jsou dva funkční symboly stejné a počet podtermů je také stejný, lze toto omezení nahradit párovou rovností subtermů. Pokud se termíny skládají z různých funkčních symbolů nebo stejného funktoru, ale s různým počtem výrazů, je omezení nesplnitelné.

Pokud je jedním ze dvou výrazů proměnná, jedinou povolenou hodnotou, kterou může proměnná nabývat, je jiný výraz. Výsledkem je, že jiný výraz může nahradit proměnnou v aktuálním úložišti cílů a omezení, čímž se proměnná prakticky odebere z úvahy. V konkrétním případě rovnosti proměnné se sebou může být omezení odstraněno jako vždy splněno.

V této formě uspokojení z omezení jsou proměnné hodnoty termíny.

Reality

Logické programování s reálnými čísly používá jako výrazy skutečné výrazy. Pokud nejsou použity žádné funkční symboly, termíny jsou výrazy nad reálnými hodnotami, případně včetně proměnných. V tomto případě může každá proměnná považovat za hodnotu pouze skutečné číslo.

Abychom byli přesní, termíny jsou výrazy nad proměnnými a skutečnými konstantami. Rovnost mezi pojmy je druh omezení, které je vždy přítomné, protože tlumočník generuje rovnost podmínek během provádění. Jako příklad platí, že pokud první doslovný text aktuálního cíle je A(X+1)a tlumočník si vybral klauzuli, která je A(Y-1):-Y=1po přepsání proměnnými, omezení přidaná k aktuálnímu cíli jsou X+1=Y-1a . Pravidla zjednodušení použitá pro funkční symboly se zjevně nepoužívají: není neuspokojivá jen proto, že první výraz je vytvořen pomocí a druhý pomocí . ${\ displaystyle Y = 1}$X+1=Y-1+-

Symboly reálných a funkčních symbolů lze kombinovat, což vede k výrazům, které jsou výrazy oproti reálným a funkčním symbolům aplikovaným na jiné výrazy. Formálně jsou proměnné a skutečné konstanty výrazy, jako jakýkoli aritmetický operátor nad jinými výrazy. Proměnné, konstanty (symboly s nulovou funkcí) a výrazy jsou termíny, jako jakýkoli funkční symbol aplikovaný na termíny. Jinými slovy, termíny jsou postaveny na výrazech, zatímco výrazy jsou postaveny na číslech a proměnných. V tomto případě se proměnné pohybují nad reálnými čísly a termíny . Jinými slovy, proměnná může mít hodnotu jako skutečné číslo, zatímco jiná výraz.

Rovnost dvou výrazů lze zjednodušit pomocí pravidel pro stromové výrazy, pokud žádný z těchto dvou výrazů není skutečným výrazem. Pokud mají například dva termíny stejný funkční symbol a počet podtermů, lze jejich omezení rovnosti nahradit rovností subtermů.

Konečné domény

Třetí třída omezení používaných v programování logiky omezení je ta u konečných domén. Hodnoty proměnných jsou v tomto případě převzaty z konečné domény, často z celých čísel . Pro každou proměnnou lze zadat jinou doménu: X::[1..5]například znamená, že hodnota Xje mezi 1a 5. Doménu proměnné lze také zadat výčtem všech hodnot, které proměnná může nabývat; proto lze výše uvedenou doménovou deklaraci také sepsat X::[1,2,3,4,5]. Tento druhý způsob určení domény umožňuje domény, které nejsou složeny z celých čísel, jako například X::[george,mary,john]. Není -li doména proměnné zadána, předpokládá se, že jde o sadu celých čísel reprezentovatelných v jazyce. Skupině proměnných lze přidělit stejnou doménu pomocí deklarace jako [X,Y,Z]::[1..5].

Doménu proměnné lze během provádění zmenšit. Skutečně, když tlumočník přidává omezení do úložiště omezení, provádí šíření omezení k vynucení formy lokální konzistence a tyto operace mohou omezit doménu proměnných. Pokud se doména proměnné stane prázdnou, úložiště omezení je nekonzistentní a algoritmus se vrací zpět. Pokud se doména proměnné stane singletonem , lze proměnné přiřadit jedinečnou hodnotu v její doméně. Formy konzistenci typicky vynucené jsou obloukové konzistence , hyper-oblouk konzistence a vázaný konzistence . Aktuální doménu proměnné lze zkontrolovat pomocí konkrétních literálů; například dom(X,D)zjistí aktuální doménu Dproměnné X.

Pokud jde o domény reálných oblastí, lze použít funktory s doménami celých čísel. V tomto případě může být výraz výrazem přes celá čísla, konstantou nebo aplikací funktoru nad jinými výrazy. Proměnná může mít jako hodnotu libovolný výraz, pokud její doména nebyla zadána jako sada celých čísel nebo konstant.

Obchod s omezeními

Úložiště omezení obsahuje omezení, která jsou v současné době považována za splnitelná. Lze zvážit, jaká je současná náhrada za pravidelné logické programování. Pokud jsou povoleny pouze stromové výrazy, úložiště omezení obsahuje omezení ve formuláři t1=t2; tato omezení jsou zjednodušena sjednocením, což má za následek omezení formuláře variable=term; taková omezení jsou ekvivalentní substituci.

Úložiště omezení však může také obsahovat omezení ve formuláři t1!=t2, pokud !=je povolen rozdíl mezi podmínkami. Pokud jsou povolena omezení týkající se reálných nebo konečných domén, úložiště omezení může také obsahovat omezení specifická pro doménu, jako X+2=Y/2je atd.

Úložiště omezení rozšiřuje koncept současné substituce dvěma způsoby. Za prvé, neobsahuje pouze omezení odvozená z přirovnání literálu k hlavě nové varianty klauzule, ale také omezení těla klauzulí. Za druhé, neobsahuje pouze omezení formuláře, variable=valueale také omezení uvažovaného omezovacího jazyka. Zatímco výsledkem úspěšného vyhodnocení pravidelného logického programu je konečná náhrada, výsledkem pro logický program omezení je konečné úložiště omezení, které může obsahovat omezení tvaru proměnná = hodnota, ale obecně může obsahovat libovolná omezení.

Omezení specifická pro doménu mohou přicházet do úložiště omezení jak z těla klauzulí, tak z porovnání literálu s hlavičkou klauzule: například pokud tlumočník přepíše literál A(X+2)klauzulí, jejíž nová hlava hlavy je A(Y/2), omezení X+2=Y/2se přidá do obchod s omezeními. Pokud se proměnná objeví ve výrazu skutečné nebo konečné domény, může mít hodnotu pouze ve skutečné nebo konečné doméně. Taková proměnná nemůže považovat výraz vytvořený z funktoru aplikovaného na jiné výrazy za hodnotu. Úložiště omezení je neuspokojitelné, pokud je proměnná vázána tak, aby přijímala jak hodnotu konkrétní domény, tak funktor aplikovaný na výrazy.

Po přidání omezení do úložiště omezení jsou v úložišti omezení provedeny některé operace. Jaké operace se provádějí, závisí na uvažované doméně a omezeních. Sjednocení se například používá pro rovnosti konečných stromů, eliminace proměnných pro polynomiální rovnice nad reálnými hodnotami, šíření omezení k vynucení formy lokální konzistence pro konečné domény. Tyto operace jsou zaměřeny na zjednodušení kontroly omezení a vyřešení úložiště omezení.

V důsledku těchto operací může přidání nových omezení změnit stará. Je důležité, aby tlumočník dokázal tyto změny vrátit zpět, když se vrací zpět. Nejjednodušší metoda je, když tlumočník uloží úplný stav úložiště pokaždé, když se rozhodne (zvolí klauzuli k přepsání cíle). Existují efektivnější metody umožňující návratu úložiště omezení do předchozího stavu. Zejména je možné pouze uložit změny v úložišti omezení provedené mezi dvěma body výběru, včetně změn provedených ve starých omezeních. To lze provést jednoduchým uložením staré hodnoty omezení, která byla upravena; této metodě se říká trailing . Pokročilejší metodou je uložit změny, které byly provedeny na upravených omezeních. Lineární omezení se například změní úpravou jeho koeficientu: uložení rozdílu mezi starým a novým koeficientem umožňuje vrátit změnu. Tato druhá metoda se nazývá sémantické zpětné sledování , protože sémantika změny je uložena spíše než stará verze omezení.

Značení

Literály označování se používají u proměnných nad konečnými doménami ke kontrole uspokojivosti nebo částečné uspokojivosti úložiště omezení a k nalezení uspokojivého přiřazení. Doslovný popisek má formu labeling([variables]), kde argumentem je seznam proměnných přes konečné domény. Kdykoli interpret vyhodnotí takový doslovný výraz, provede vyhledávání v doménách proměnných seznamu, aby našel přiřazení, které splňuje všechna relevantní omezení. Obvykle se to provádí formou zpětného sledování : proměnné se vyhodnocují v pořadí, zkouší všechny možné hodnoty pro každou z nich a zpětné sledování, když je zjištěna nekonzistence.

Prvním použitím doslovného označení je skutečná kontrola splnitelnosti nebo částečné uspokojivosti úložiště omezení. Když tlumočník přidá omezení do úložiště omezení, vynutí pouze formu místní konzistence. Tato operace nemusí detekovat nekonzistenci, i když je úložiště omezení neuspokojivé. Doslovný popisek nad sadou proměnných vynucuje kontrolu splnitelnosti omezení přes tyto proměnné. Výsledkem je, že použití všech proměnných uvedených v úložišti omezení vede ke kontrole uspokojivosti úložiště.

Druhé použití literálu označení je ve skutečnosti určit vyhodnocení proměnných, které splňuje úložiště omezení. Bez doslovného označení jsou proměnným přiřazeny hodnoty pouze tehdy, když úložiště omezení obsahuje omezení formuláře X=valuea když lokální konzistence redukuje doménu proměnné na jedinou hodnotu. Doslovný popisek nad některými proměnnými nutí tyto proměnné vyhodnotit. Jinými slovy, po zvážení doslovného označení je všem proměnným přiřazena hodnota.

Programy logiky omezení jsou obvykle napsány takovým způsobem, že se literály označování vyhodnotí až poté, co se v úložišti omezení nahromadí co nejvíce omezení. Důvodem je, že označování literálů vynucuje vyhledávání a vyhledávání je efektivnější, pokud je třeba splnit více omezení. Problém splňování je typický řeší omezení logického programu, který má následující strukturu:

solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)

Když interpret vyhodnotí cíl solve(args), umístí tělo aktuální varianty první klauzule do aktuálního cíle. Protože první cíl je constraints(X'), vyhodnotí se druhá klauzule a tato operace přesune všechna omezení v aktuálním cíli a nakonec v úložišti omezení. Doslovný labeling(X')je pak vyhodnocen a vynucen hledání řešení úložiště omezení. Protože úložiště omezení obsahuje přesně omezení původního problému uspokojení omezení, tato operace hledá řešení původního problému.

Programové reformulace

Daný program logiky omezení může být přeformulován, aby se zlepšila jeho účinnost. Prvním pravidlem je, že popisovací literály by měly být umístěny poté, co se v úložišti omezení nahromadí tolik omezení na označených literálech. I když je teoreticky ekvivalentní , hledání, které se provádí, když interpret narazí na literál označení, je v úložišti omezení, které toto omezení neobsahuje . V důsledku toho může generovat řešení, jako například ta , u nichž se později zjistí, že nesplňují toto omezení. Na druhou stranu ve druhé formulaci je vyhledávání prováděno pouze tehdy, když je omezení již v úložišti omezení. Výsledkem je, že vyhledávání vrací pouze řešení, která jsou s ním konzistentní, s využitím výhody, že další omezení zmenšují prostor pro vyhledávání. A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

Druhou reformulací, která může zvýšit účinnost, je umístit omezení před literály do těla klauzulí. Opět platí, a jsou v zásadě rovnocenné. První však může vyžadovat více výpočtů. Pokud například úložiště omezení obsahuje omezení , tlumočník rekurzivně vyhodnotí v prvním případě; pokud se to podaří, pak zjistí, že úložiště omezení je při přidávání nekonzistentní . V druhém případě při vyhodnocování této klauzule interpret nejprve přidá do úložiště omezení a poté případně vyhodnotí . Protože úložiště omezení po přidání se ukáže být nekonzistentní, rekurzivní vyhodnocení se neprovádí vůbec. A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

Třetí reformulace, která může zvýšit účinnost, je přidání nadbytečných omezení. Pokud programátor ví (jakýmikoli prostředky), že řešení problému splňuje konkrétní omezení, může toto omezení zahrnout, aby způsobilo nesoulad úložiště omezení co nejdříve. Pokud je například předem známo, že vyhodnocení B(X)bude mít kladnou hodnotu pro X, programátor může přidat X>0před jakýmkoli výskytem B(X). Jako příklad A(X,Y):-B(X),C(X)selže na cíl A(-2,Z), ale to se zjistí až při vyhodnocování dílčího cíle B(X). Na druhou stranu, pokud je výše uvedená klauzule nahrazena , tlumočník ustupuje, jakmile je omezení přidáno do úložiště omezení, což se stane před vyhodnocením sudého spuštění. A(X,Y):-X>0,A(X),B(X)X>0B(X)

Pravidla zpracování omezení

Pravidla zpracování omezení byla původně definována jako samostatný formalismus pro určování řešitelů omezení a později byla začleněna do logického programování. Existují dva druhy pravidel zpracování omezení. Pravidla prvního druhu určují, že za dané podmínky je množina omezení ekvivalentní jinému. Pravidla druhého druhu specifikují, že za dané podmínky sada omezení implikuje další. V programovacím jazyce logiky omezení podporujícím pravidla pro zpracování omezení může programátor použít tato pravidla k určení možných přepisů úložiště omezení a možného přidání omezení do něj. Následuje příklad pravidel:

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

První pravidlo říká, že pokud B(X)to obchod zahrnuje, A(X)lze omezení přepsat jako C(X). Jako příklad N*X>0lze přepsat, jako X>0by to znamenalo obchod N>0. Symbol <=>se v logice podobá ekvivalenci a říká, že první omezení je ekvivalentní druhému. V praxi to znamená, že první omezení lze nahradit druhým.

Druhé pravidlo místo toho specifikuje, že toto druhé omezení je důsledkem prvního, pokud je omezení uprostřed způsobeno úložištěm omezení. V důsledku toho, pokud A(X)je v úložišti omezení a B(X)je zahrnuto v úložišti omezení, C(X)lze jej přidat do úložiště. Na rozdíl od případu ekvivalence jde o doplnění, nikoli o náhradu: nové omezení se přidá, ale staré zůstane.

Ekvivalence umožňuje zjednodušení úložiště omezení nahrazením některých omezení jednoduššími; zejména je -li třetí omezení v pravidle ekvivalence truea druhé omezení s sebou nese, je první omezení odstraněno z úložiště omezení. Inference umožňuje přidání nových omezení, což může vést k prokázání nekonzistence úložiště omezení a obecně může snížit množství vyhledávání potřebného k prokázání jeho splnitelnosti.

Logické programovací doložky ve spojení s pravidly zpracování omezení lze použít k určení metody pro stanovení uspokojivosti úložiště omezení. Různé klauzule se používají k implementaci různých voleb metody; pravidla pro zpracování omezení se používají k přepsání úložiště omezení během provádění. Například lze tímto způsobem implementovat zpětné sledování pomocí šíření jednotek . Let holds(L)představuje propoziční klauzuli, ve které jsou literály v seznamu Lve stejném pořadí, v jakém jsou vyhodnoceny. Algoritmus lze implementovat pomocí klauzulí pro volbu přiřazení doslovného textu na hodnotu true nebo false a pomocí pravidel zpracování omezení k určení šíření. Tato pravidla určují, že holds([l|L])je možné je odstranit, pokud l=truevyplývá z úložiště, a lze je přepsat, jako holds(L)by l=falsez obchodu vyplývalo. Podobně holds([l])lze nahradit l=true. V tomto příkladu je volba hodnoty proměnné implementována pomocí klauzulí logického programování; lze jej však zakódovat v pravidlech zpracování omezení pomocí rozšíření nazývaného disjunktivní pravidla zpracování omezení nebo CHR ^∨ .

Vyhodnocení zdola nahoru

Standardní strategie hodnocení logických programů je shora dolů a nejprve hloubka : z cíle je identifikována řada klauzulí, které by mohly dokázat cíl, a provede se rekurze přes doslovné části jejich těl. Alternativní strategií je začít od faktů a používat klauzule k odvozování nových faktů; tato strategie se nazývá zdola nahoru . Považuje se za lepší než ten shora dolů, když je cílem vytvořit všechny důsledky daného programu, spíše než prokazovat jediný cíl. Zejména zjištění všech důsledků programu standardním způsobem shora dolů a hloubkou nejprve nemusí skončit, zatímco skončí strategie hodnocení zdola nahoru .

Strategie hodnocení zdola nahoru udržuje soubor faktů, které byly během hodnocení dosud prokázány. Tato sada je zpočátku prázdná. S každým krokem se odvozují nová fakta použitím klauzule programu na stávající fakta a přidávají se do sady. Například vyhodnocení následujícího programu zdola nahoru vyžaduje dva kroky:

A(q).
B(X):-A(X).

Soubor důsledků je zpočátku prázdný. V prvním kroku A(q)je jedinou klauzulí, jejíž tělo lze prokázat (protože je prázdná), a A(q)proto je přidána k aktuálnímu souboru důsledků. V druhém kroku, protože A(q)je prokázáno, lze použít druhou klauzuli a B(q)přidává se k důsledkům. Protože nelze prokázat žádný jiný důsledek {A(q),B(q)}, exekuce končí.

Výhodou hodnocení zdola nahoru oproti hodnocení shora dolů je, že cykly derivací nevytvářejí nekonečnou smyčku . Důvodem je, že přidání důsledku k aktuálnímu souboru důsledků, který jej již obsahuje, nemá žádný účinek. Jako příklad, přidání třetí klauzule do výše uvedeného programu generuje cyklus derivací v hodnocení shora dolů:

A(q).
B(X):-A(X).
A(X):-B(X).

Při vyhodnocování všech odpovědí na cíl A(X)by například strategie shora dolů vytvořila následující derivace:

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

Jinými slovy, A(q)nejprve se vytvoří jediný důsledek , ale pak algoritmus cykluje nad derivacemi, které nevytvářejí žádnou jinou odpověď. Obecněji může strategie hodnocení shora dolů procházet možnými derivacemi, případně pokud existují jiné.

Strategie zdola nahoru nemá stejnou nevýhodu, protože důsledky, které již byly odvozeny, nemají žádný účinek. U výše uvedeného programu začíná strategie zdola nahoru přidávat A(q)k souboru důsledků; ve druhém kroku B(X):-A(X)slouží k odvození B(q); Ve třetím kroku, pouze fakta, která lze odvodit ze současných následky jsou A(q)i B(q), které jsou však již v sadě následků. V důsledku toho se algoritmus zastaví.

Ve výše uvedeném příkladu byly použity pouze pozemní literály. Obecně platí, že každá klauzule, která obsahuje pouze omezení v těle, je považována za skutečnost. Například klauzule A(X):-X>0,X<10je také považována za fakt. Pro tuto rozšířenou definici faktů mohou být některá fakta ekvivalentní, i když nejsou syntakticky stejná. Například A(q)je ekvivalentní A(X):-X=qa oba jsou ekvivalentní A(X):-X=Y, Y=q. K vyřešení tohoto problému jsou fakta přeložena do normální formy, ve které hlava obsahuje n-tici různých proměnných; dvě fakta jsou pak ekvivalentní, pokud jsou jejich těla ekvivalentní proměnným hlavy, to znamená, že jejich sady řešení jsou stejné, pokud jsou omezeny na tyto proměnné.

Jak je popsáno, přístup zdola nahoru má tu výhodu, že nezohledňuje důsledky, které již byly odvozeny. Stále však může vyvodit důsledky, které jsou spojeny s těmi, které již byly odvozeny, aniž by se rovnaly jakémukoli z nich. Například vyhodnocení zdola nahoru následujícího programu je nekonečné:

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

Algoritmus hodnocení zdola nahoru nejprve odvodí, že A(X)platí pro X=0a X>0. Ve druhém kroku první skutečnost s třetí klauzulí umožňuje odvození A(1). Ve třetím kroku A(2)je odvozen atd. Tyto skutečnosti jsou však již spojeny skutečností, která A(X)platí pro všechny nezáporné X. Tuto nevýhodu lze překonat kontrolou faktů o implikacích, které je třeba přidat k aktuálnímu souboru důsledků. Pokud nový důsledek již obsahuje sada, není do něj přidán. Vzhledem k tomu, že fakta jsou uložena jako klauzule, případně s „lokálními proměnnými“, je zapojení proměnných nad jejich hlavami omezeno.

Souběžné programování logiky omezení

Souběžné verze programování logiky omezení jsou zaměřeny spíše na programování souběžných procesů než na řešení problémů s uspokojením omezení . Cíle v logickém programování omezení jsou vyhodnocovány souběžně; souběžný proces je proto naprogramován jako vyhodnocení cíle tlumočníkem .

Syntakticky jsou logické programy souběžných omezení podobné nesouběžným programům, jedinou výjimkou je, že klauzule obsahuje ochranné prvky , což jsou omezení, která mohou za určitých podmínek blokovat použitelnost klauzule. Sémanticky se souběžné programování logiky omezení liší od jeho nesouběžných verzí, protože vyhodnocení cíle je určeno k realizaci souběžného procesu, nikoli k nalezení řešení problému. Nejpozoruhodnější je, že tento rozdíl ovlivňuje chování tlumočníka, když je použitelná více než jedna klauzule: nekonkurenční programování logiky omezení rekurzivně zkouší všechny klauzule; programování logiky souběžných omezení volí pouze jednu. Toto je nejzjevnější účinek zamýšlené směrovosti tlumočníka, který nikdy nezreviduje volbu, kterou dříve přijal. Dalšími důsledky jsou sémantická možnost mít cíl, který nelze prokázat, zatímco celé hodnocení neselže, a konkrétní způsob, jak srovnat cíl a klauzuli.

Aplikace

Logické programování omezení bylo aplikováno na řadu oblastí, jako je automatické plánování , odvozování typů , stavebnictví , strojírenství , ověřování digitálních obvodů , řízení letového provozu , finance a další.

Dějiny

Programování logiky omezení zavedli Jaffar a Lassez v roce 1987. Zobecnili pozorování, že termín rovnice a nerovnosti v Prologu II jsou specifickou formou omezení, a zobecnili tuto myšlenku na libovolné omezující jazyky. První implementace tohoto konceptu byla Prolog III , CLP (R) a CHIP .

Viz také

• BProlog
• BNR Prolog (aka CLP (BNR))
• Čau
• CLP (R)
• Distribuován Oz Mozart
• Zatmění
• GNU Prolog
• SWI-Prolog

Reference

• Dechter, Rina (2003). Zpracování omezení . Morgan Kaufmann. ISBN 1-55860-890-7. ISBN  1-55860-890-7
• Apt, Krzysztof (2003). Zásady programování omezení . Cambridge University Press. ISBN 0-521-82583-0. ISBN  0-521-82583-0
• Marriott, Kim; Peter J. Stuckey (1998). Programování s omezeními: Úvod . Stiskněte MIT. ISBN  0-262-13341-5
• Frühwirth, Thom; Slim Abdennadher (2003). Základy programování omezení . Springer. ISBN 3-540-67623-6. ISBN  3-540-67623-6
• Jaffar, Joxan; Michael J. Maher (1994). „Programování logiky omezení: průzkum“ . Journal of Logic Programming . 19/20: 503–581. doi : 10,1016/0743-1066 (94) 90033-7 .
• Colmerauer, Alain (1987). „Otevření vesmíru Prolog III“. Byte . Srpen.

Reference