11.5. Tervkészítés ítéletlogikával
A 10. fejezetben láthattuk, hogy a tervkészítés elvégezhető a szituációkalkulus egy tételének bizonyításával. A tétel azt mondja, hogy adott kiinduló állapotra és követőállapot-axiómákra, amelyek a cselekvések következményeit írják le, a cél egy adott cselekvéssorból adódó helyzetben igaz lesz. Ezt a megközelítést már 1969-ben sem találták eléggé hatékonynak érdekes tervek megtalálására. Napjaink fejlesztései az ítéletlogikához készített hatékony magyarázatadó algoritmusokra (lásd 7. fejezet) ismét felkeltették az érdeklődést a tervkészítés logikai magyarázatkészítési megközelítésére.
Az ebben a fejezetben tárgyalt megközelítés a tételbizonyítás helyett egy cselekvéssor kielégíthetőségének (satisfiability) vizsgálatán alapul. Ítéletlogikai mondatok modelljét fogjuk megtalálni, melyek a következőképpen néznek ki:
kiinduló állapot ∧ minden lehetséges cselekvésleírás ∧ cél
A mondat ítéletlogikai szimbólumokat fog tartalmazni, melyek a lehetséges cselekvés-előfordulások megfelelői. A modell, ami kielégíti a mondatot, igaz értéket rendel azokhoz a cselekvésekhez, amelyek részei a helyes tervnek, és hamis értéket a többihez. Egy olyan célkitűzés, mely egy nem helyes terv megfelelője, nem lesz modell, mivel nem lesz konzisztens azzal a feltételezéssel, hogy a cél igaz. Ha a tervkészítési probléma megoldhatatlan, akkor a mondat sem kielégíthető.
A STRIPS problémák ítéletlogikai leírásra való fordítását a tudásreprezentációs ciklus egy iskolapéldáján mutatjuk be: egy megfelelő axiómakészlettel indulunk, és úgy találjuk, hogy ezek az axiómák hamis, nem várt modelleket tesznek lehetővé, ezért további axiómákat adunk hozzájuk.
Kezdjük a nagyon egyszerű légi szállítási problémával. A kiinduló állapotban (0. időpont) a P1 repülő az SFO repülőtéren van, míg a P2 repülő a JFK-n. A cél, hogy a P1 legyen a JFK, a P2 pedig az SFO reptéren, azaz a repülőgépeknek helyet kell cserélniük. Először egymástól eltérő ítéletlogikai szimbólumokra van szükségünk az egyes időlépések kijelentéseihez. Az időpillanatok jelöléséhez felső indexeket használunk, mint a 7. fejezetben. Így a kiinduló állapot felírása az
Ott(P1, SFO)0 ∧ Ott(P2, JFK)0
(Emlékezzünk arra, hogy az Ott(P1, SFO)0 egy atomi szimbólum!) Mivel az ítéletlogika nem használja a zárt világ feltételezést, ezért a kiinduló állapotban definiálnunk kell a nem igaz ítéletlogikai állításokat is. Ha néhány állítás nem ismert a kiinduló állapotban, akkor ezek maradhatnak meghatározatlanok (nyílt világ feltételezés). Ebben a példában az
¬Ott(P1, JFK)0 ∧ ¬Ott(P2, SFO)0
kiinduló állapotot specifikáljuk. A célt magát egy megadott időlépéshez kell kapcsolni. Mivel nem tudjuk a priori, hogy hány lépésre van szükség a cél eléréséhez, megpróbálhatjuk feltételezni, hogy a cél igaz a kiinduló állapotban, T = 0 időpontban. Azaz a következőt állítjuk: Ott(P1, JFK)0 ∧ Ott(P2, SFO)0. Ha ez sikertelen, újra próbálkozunk T = 1-gyel, és így tovább, amíg a legkisebb megfelelő tervhosszt el nem érjük. T minden értékére a tudásbázis a 0. időponttól a T-ig tartó lépéseket fedő mondatokat fogja tartalmazni. Hogy biztosítsuk a leállást, egy önkényes Tmax felső korlátot kell állítanunk. Ezt az algoritmust mutatja a 11.15. ábra. Egy másik lehetséges megközelítést, mely elkerüli a többszörös megoldási kísérleteket, a 11.17. feladatban tárgyalunk.
11.15. ábra - A
SATPLAN algoritmus. A tervkészítési feladatot egy konjunktív normál formájú mondatra fordítjuk le, amelyben minden cél egy megadott T időpillanatban teljesül, és T-ig minden lépésre tartalmazza az axiómákat. (A fordítás részleteit a szövegben írjuk le.) Ha a kielégíthetőségi algoritmus talál modellt, akkor a tervet a modellben az igaz értéket kapott ítéletlogikai szimbólumokhoz tartozó cselekvések kinyerésével kapjuk meg. Ha nem létezik modell, akkor a folyamatot ismételjük, a célt egy lépéssel későbbre mozgatva.
A következő kérdés, hogy hogyan kódoljuk a cselekvés leírásokat az ítéletlogikában. A legegyszerűbb megközelítés, hogy minden cselekvés megjelenésére egy ítéletlogikai szimbólumot vezetünk be. Például a Repül(P1, SFO, JFK)0 igaz, ha a P1 repülőgép az SFO-ról a JFK-ra repül a 0. időpillanatban. Csakúgy, mint a 7. fejezetben, felírjuk az ítéletlogikai változatait a következő állapotaxiómáknak, melyeket a 10. fejezetben a szituációkalkulushoz fejlesztettünk ki. Adott például az
Ott(P1, JFK)1 ⇔ (Ott(P1, JFK)0 ∧ ¬(Repül(P1, JFK, SFO)0 ∧ Ott(P1, JFK)0))
∨ (Repül(P1, SFO, JFK)0 ∧ Ott(P1, SFO)0) (11.1)
axióma. Ennek jelentése, hogy a P1 repülő a JFK-n lesz az 1-es időpillanatban, ha a JFK-n volt a 0. időpillanatban, és onnan nem repült el, vagy ha az SFO-n volt a 0. időpillanatban, és elrepült a JFK-ra. Egy ilyen axiómára minden egyes repülőgéphez, repülőtérhez és időpillanathoz szükségünk van. Mindezeken túl minden egyes hozzáadott repülőtér egy új kiinduló, illetve ott végződő útvonalat ad az összes repülőtérhez, ezért további diszjunkciókat ad az összes axióma jobb oldalához.
Ha ezek az axiómák megvannak, akkor egy kielégíthetőségi algoritmust futtathatunk a terv megtalálására. Kell, hogy legyen olyan terv, ami a célt a T = 1 időpillanatban eléri, nevezetesen az a terv, melyben a két repülőgép helyet cserél. Tegyük fel, hogy a tudásbázis a következő:
kiinduló állapot ∧ követő állapot axiómák ∧ cél1 (11.2)
mely szerint a cél a T = 1 időpillanatban igaz. Ellenőrizhető, hogy az eljárás, melyben a
Repül(P1, SFO, JFK)0 és a Repül(P2, JFK, SFO)0
igaz, és minden más cselekvésszimbólum hamis, modellje a tudásbázisnak. Eddig itt minden rendben. Vannak más lehetséges modellek, melyeket a kielégíthetőségi algoritmus visszaadhat? Valójában igen. Ezen modellek mindegyike kielégítő terv? Sajnos nem. Vegyük például a
Repül(P1, SFO, JFK)0, a Repül(P1, JFK, SFO)0 és a Repül(P2, JFK, SFO)0
cselekvésszimbólumok által specifikált meglehetősen butácska tervet. Ez a terv buta, mert a P1 repülő az SFO-ról indul, ezért a Repül(P1, JFK, SFO)0 cselekvés végrehajthatatlan. Mindazonáltal a terv modellje a (11.2) egyenlet mondatának! Ez annyit jelent, hogy megfelel mindennek, amit eddig a problémáról állítottunk. Hogy megértsük miért, egy kicsit közelebbről meg kell vizsgálnunk, hogy a következő állapot axiómák mit mondanak el a cselekvésekről, melyeknek az előfeltételei nem teljesülnek (mint a (11.1) egyenletben). Az axiómák helyesen írják le, hogy semmi sem történik, ha egy ilyen cselekvést végrehajtunk (lásd 11.15. feladat), de nem állítják, hogy egy ilyen cselekvés nem hajtható végre! Hogy elkerüljük az illegális cselekvéseket tartalmazó tervek készítését, további előfeltétel axiómákat (precondition axioms) kell felvennünk, melyek biztosítják, hogy egy cselekvés megjelenéséhez az előfeltételeknek teljesülni kell.[116] Például szükségünk van az
Repül(P1, JFK, SFO)0 ⇒ Ott(P1, JFK)0
axiómára, mert az Ott(P1, JFK)0 hamis a kiinduló állapotban, így ez az axióma biztosítja, hogy a Repül(P1, JFK, SFO)0 minden modellben szintén hamis legyen. Az előfeltétel axiómák hozzáadásával már csak pontosan egy modell van, ami teljesíti az összes axiómát, amikor a célt az 1-es időpillanatban érjük el, nevezetesen az a modell, melyben a P1 repülőgép a JFK-ra, a P2 repülőgép pedig az SFO-ra repül. Vegyük észre, hogy ez a megoldás két párhuzamos cselekvést tartalmaz! Csakúgy, mint a GRAPHPLAN vagy a részben rendezett tervkészítés esetén.
További meglepetésekre számíthatunk, amikor egy új repülőteret illesztünk be, a LAX-ot (Los Angeles repülőtere). Most minden repülőgéphez minden állapotban két megengedett cselekvés is tartozik. Amikor egy kielégíthetőségi algoritmust futtatunk, úgy találjuk, hogy a Repül(P1 SFO, JFK)0, a Repül(P2, JFK, SFO)0 és a Repül(P2, JFK, LAX)0-ból álló modell kielégíti az axiómákat. Azaz a követő állapot axiómák és az előfeltétel axiómák megengedik, hogy egy repülőgép egyszerre két célállomásra is repülhessen! A kiinduló állapot a P2 mindkét repülőútjának előfeltételeit teljesíti, így a követő állapot axiómák szerint a P2 az SFO-n és a LAX-on található az 1-es időpillanatban, azaz a cél teljesül. Nyilvánvaló, hogy további axiómákat kell felvennünk, hogy kizárjuk ezeket a hibás megoldásokat. Az egyik megközelítés, hogy cselekvéskizáró axiómákat (action exclusion axioms) veszünk fel, melyek meggátolják az egyidejű cselekvéseket. Pédául teljes kizárást érhetünk el, ha az összes
¬(Repül(P2, JFK, SFO)0 ∧ Repül(P2, JFK, LAX)0)
alakú axiómát felvesszük. Ezek az axiómák biztosítják, hogy semelyik két cselekvés ne eshessen azonos időpontra. Ezek kizárják a hibás terveket, hatásukra minden terv teljesen rendezett lesz. Ez elveszíti a részben rendezett tervek rugalmasságát, és azáltal, hogy megnöveli a terv lépésszámát, a számítási idő is meghosszabbodhat.
A teljes kizárás helyett alkalmazhatunk csupán részleges kizárást, amikor az egyidejű cselekvéseket csak akkor zárjuk ki, ha kölcsönhatásba kerülnek. A feltételek a mutex cselekvések megfelelői: két cselekvés nem hajtható végre egyidejűleg, ha az egyik negálja a másik egy előfeltételét vagy következményét. Például a Repül(P2, JFK, LAX)0 és a Repül(P2, JFK, SFO)0 együtt nem következhet be, mert mindkettő negálja a másik előfeltételét. Másrészről azonban a Repül(P2, JFK, SFO)0 és a Repül(P2, JFK, SFO)0 együtt is bekövetkezhet, hiszen a járatok nem zavarják egymást. A részleges kizárás a teljes rendezés kényszere nélkül kiküszöböli a hibás terveket.
A kizárási axiómák néha nagyon buta eszköznek tűnnek. Ahelyett hogy kikötnénk, hogy egy gép nem repülhet egyszerre két reptérre, mondhatnánk egyszerűen, hogy egyetlen tárgy sem lehet egyszerre két helyen:
∀p, x, y, t x ≠ y ⇒ ¬(Ott(p, x)t ∧ Ott(p, y)t)
Ez a tény a követő állapot axiómákkal kombinálva, azt implikálja, hogy egy repülő nem repülhet egyszerre két reptérre. Az ilyen tényeket állapotkorlátozásoknak (state constraints) nevezzük. Az ítéletlogikában természetesen meg kell adnunk minden egyes állapotkorlátozás összes alappéldányát. A repülés feladatra az állapotkorlátozás elegendő az összes hibás terv kizárásához. Az állapotmegkötések gyakran sokkal tömörebbek, mint a cselekvéskizárási axiómák, ezek azonban a probléma eredeti STRIPS reprezentációjából nem mindig vezethetők le könnyedén.
Összefoglalva tehát a kielégíthetőségi tervkészítés, a kiinduló állapotot, a célt, a követő állapot axiómákat, az előfeltételeket, valamint a cselekvéskizárások vagy az állapotaxiómák egyikét tartalmazó mondathoz tartozó modellek megtalálását jelenti. Megmutatható, hogy az axiómák ezen halmaza elégséges, abban az értelemben, hogy a továbbiakban nincsenek hibás „megoldások”. Az ítéletlogikai mondatot kielégítő bármely modell megfelelő megoldása az eredeti problémának, azaz a terv minden sorba rendezése egy megengedett cselekvéssor, ami a célhoz vezet.
Az ítéletlogikai megközelítés legnagyobb hátránya az eredeti problémából generált tudásbázis mérete. A Repül(p, a1, a2) cselekvésséma például T × ∣Repülők∣ × ∣Repülőterek∣2 számú különböző állításlogikai szimbólumot eredményez. Általánosságban a cselekvésszimbólumok számának korlátja a T × ∣Act∣ × ∣O∣P, ahol az ∣Act∣ a cselekvéssémák száma, ∣O∣ a problémakör objektumainak száma, valamint P a cselekvés sémák maximális aritása (paramétereinek száma). A klózok száma még nagyobb. 10 időlépés, 12 repülőgép és 30 repülőtér esetén a teljes cselekvéskizárási axiómában 583 millió klóz van.
Mivel a cselekvésszimbólumok száma a cselekvéssémák aritásával exponenciálisan nő, megoldás lehet az aritás csökkentése. Ezt a szemantikus hálóktól (lásd 10. fejezet) kölcsönvett ötlet segítségével tehetjük meg. A szemantikus hálók csak bináris predikátumokat használnak, az ennél több argumentummal rendelkező predikátumokat egy bináris predikátumhalmazra képezzük le, ami külön ad meg minden predikátumot. Ezt az ötletet a Repül(P1, SFO, JFK)0 cselekvésszimbólumra alkalmazva, három új szimbólumot kapunk:
Repül1(P1)0: a P1 repülő a 0. időpontban repült
Repül2(SFO)0: a járat kiinduló állomása az SFO
Repül3(JFK)0: a járat célállomása a JFK
Ez a szimbólumfelosztásnak (symbol splitting) nevezett folyamat kiküszöböli az exponenciális számú szimbólum igényét. Így most csak T × ∣Act∣ × P × ∣O∣ szimbólumra van szükség.
A szimbólum felosztás önmagában lecsökkenti ugyan a szimbólumok számát, de a tudásbázisban szereplő axiómák számát nem csökkenti automatikusan. Azaz, ha minden klózban szereplő cselekvésszimbólumot egyszerűen csak három szimbólum konjunkciójára cserélnénk, a tudásbázis mérete nagyjából azonos maradna. A szimbólumfelosztás valóban csökkenti a tudásbázis méretét, mivel néhány szétbontott szimbólum feleslegessé válik bizonyos axiómákban, és elhagyható. Vegyük például a (11.1) egyenletben szereplő követő állapot axiómát, módosítva, hogy tartalmazza LAX-ot, és elhagyva a cselekvés előfeltételeket (melyeket külön előfeltétel axiómákkal fedünk le):
Ott(P1, JFK)1 ⇔ (Ott(P1, JFK)0 ∧ ¬Repül(P1, JFK, SFO)0 ∧ ¬Repül(P1, JFK, LAX)0)
∨ Repül(P1, SFO, JFK)0 ∨ Repül(P1, LAX, JFK)0
Az első feltétel szerint a P1 a JFK-n lesz, ha a 0. időpontban ott volt, és nem repült el egyetlen másik városba sem. A második azt mondja, hogy ott lesz, ha mindegy, hogy honnan, de a JFK-ra repül. A felosztási szimbólumok használatával, egyszerűen elhagyhatjuk azon argumentumokat, melyek értéke nem számít:
Ott(P1, JFK)1 ⇔ (Ott(P1, JFK)0 ∧ ¬Repül1(P1)0 ∧ Repül2(JFK)0) ∨ Repül1(P1)0
∧ Repül3(JFK)0
Vegyük észre, hogy az SFO és a LAX már nem szerepel az axiómában. Általánosabban a felosztási szimbólumoknak köszönhetően a követő állapot axiómák mérete függetlenné válik a repülőterek számától. Hasonló redukció történik az előfeltétel és a cselekvéskizárási axiómákkal (lásd 11.16. feladat). A korábban bemutatott 10 időlépés, 12 repülő és 30 reptér esetében a teljes cselekvéskizárási axóma mérete 583 millió klózról 9360 klózra csökken.
A módszernek egyetlen hátulütője van: a felosztási szimbólum reprezentáció nem engedi meg a párhuzamos cselekvéseket. Vegyük a Repül(P1, SFO, JFK)0 és a Repül(P2, JFK, SFO)0 párhuzamos cselekvéseket. A felosztott megadásra alakítva a
Repül1(P1)0 ∧ Repül2(SFO)0 ∧ Repül3(JFK)0 ∧
Repül1(P2)0 ∧ Repül2(JFK)0 ∧ Repül3(SFO)0
kifejezést kapjuk. Innentől már nem állapítható meg mi történt! Tudjuk, hogy P1 és P2 repült, de nem tudjuk azonosítani a járatok kiinduló és célállomásait. Ez annyit tesz, hogy egy teljes cselekvéskizárási axiómát kell használni, annak korábban jelzett hátrányaival.
A kielégíthetőségen alapuló tervkészítők nagyon nagy tervkészítési problémákat képesek kezelni – például a többtucatnyi dobozból álló kockavilág probléma 30 lépéses tervét. A propozíciós kódolás mérete, valamint a megoldás költsége nagymértékben problémafüggő, de a legtöbb esetben az ítéletlogikai axiómák t árolásához szükséges memóriaméret a szűk keresztmetszet. Ennek a kutatásnak egy érdekes eredménye, hogy a visszalépéses algoritmusok (mint a DPLL) gyakran hatékonyabbak voltak a tervkészítési problémák megoldásában, mint a lokális keresési algoritmusok (például a WALKSAT). Ennek oka, hogy az állításlogikai axiómák többsége Horn-klóz, ami egység terjesztéstechnikákkal kezelhető hatékonyan. Ez a megfigyelés hibrid algoritmusok kifejlesztéséhez vezetett, melyek a véletlen keresési, a hiba-visszaterjesztési és az egységterjesztési módszereket kombinálják.
[116] Figyeljük meg, hogy az előfeltétel axiómák felvétele azt jelenti, hogy nem kell a követő állapot axiómáknál a cselekvésekhez előfeltételeket felvennünk.
