7.6. Hatékony ítéletkalkulus következtetés
Ebben a szakaszban az ítéletkalkulus következtetés két hatékony családját írjuk le, amelyek a modellellenőrzésen alapulnak: az egyik megközelítés a visszalépéses keresésen alapul, a másik a hegymászó keresésen. Ezek az algoritmusok az ítéletkalkulus „technológiájának” részei. Ez a szakasz átlapozható a fejezet első olvasásakor.
Az algoritmusok, amelyeket leírunk, a kielégíthetőséget ellenőrzik. Már megfigyeltük a kapcsolatot egy logikai mondatot kielégítő modell megtalálása és egy kényszerkielégítési probléma megoldásának megtalálása között, így talán nem meglepő, hogy a két algoritmus család igen hasonlít az 5.2. alfejezetben bemutatott visszalépéses algoritmusokra és az 5.3. alfejezet lokális keresési algoritmusaira. Ezek az algoritmusok azonban rendkívül fontosak saját maguk jogán is, mert számos kombinatorikai probléma a számítástechnikában visszavezethető egy ítéletkalkulus mondat kielégíthetőségének ellenőrzésére. A kielégíthetőségi algoritmusok terén elért bármilyen haladás általánosságban is óriási hatással van a képességeinkre a komplexitás kezelésében.
Az első algoritmus, amit megnézünk Martin Davis és Hilary Putnam (1960) jelentős konferenciacikke alapján, az úgynevezett Davis–Putnam-algoritmus. Ez az algoritmus valójában egy változata annak, amelyet Davis, Logemann és Loveland (1962) publikált, így DPLL-nek fogjuk hívni szerzőik neveinek kezdőbetűi alapján. A DPLL bemenetként egy konjunktív normál formájú mondatot vesz – a klózok egy halmazát. Mint a VISSSZALÉPÉSES-KERESÉS vagy az IK-VONZAT?, ez is alapvetően rekurzív, mélységi felsorolását végzi a lehetséges modelleknek. Az algoritmus három továbbfejlesztést tartalmaz az IK-VONZAT? egyszerű sémájához képest:
-
Korai leállás: Az algoritmus észreveszi, ha egy mondat már biztos igaz vagy hamis, még részben elkészült modell alapján is. Egy klóz igaz, ha bármelyik literál igaz, még akkor is, ha a többi literálnak még nincs igazság értéke. Ennélfogva a mondatot mint egészet igaznak ítélhetjük, még mielőtt a modell teljes volna. Például az (A ∨ B) ∧ (A ∨ C) igaz, ha A igaz, függetlenül B és C értékétől. Hasonlóan, egy mondat hamis, ha bármelyik klóz hamis, ami akkor fordul elő, ha ennek a klóznak minden literálja hamis. Ismételten, ez a modell teljessé válásánál sokkal korábban is előfordulhat. A korai leállás a keresési tér egész részfáinak átvizsgálását kerüli el.
-
Tiszta szimbólum heurisztika: Egy tiszta szimbólum (pure symbol) egy olyan szimbólum, amely mindig ugyanolyan „előjellel” szerepel minden klózban. Például a következő három mondatban, (A ∨ ¬B), (¬B ∨ ¬C) és az A szimbólum tiszta, mivel csak a pozitív literálja jelenik meg, a B tiszta, mivel csak a negatív literálja jelenik meg, és C nem tiszta. Könnyű belátni, hogyha egy mondatnak van modellje, akkor létezik tiszta szimbólumokat tartalmazó modellje is, amelyben a tiszta szimbólumok értéke úgy van megválasztva, hogy literáljai igazak legyenek, hiszen így egyetlen klózt sem teszünk hamissá. Vegyük észre, hogy egy szimbólum tisztaság tulajdonságának meghatározásakor az algoritmus figyelmen kívül hagyhatja azokat a klózokat, amelyekről már tudjuk, hogy igazak a modell eddigi konstruálása alapján. Például ha a modellünk tartalmazza a B = hamis hozzárendelést, akkor a (¬B ∨ ¬C) klóz már igaz, és C tisztává válik, mert csak a (C ∨ A)-ban jelenik meg.
-
Egységklóz heurisztika: Az egységklózt már definiáltuk korábban, mint egy olyan klózt, amelynek egy literálja van. A DPLL esetében, ez azt jelenti, hogy egy kivételével minden literál hamis értéket kapott a modellben. Például ha a modell tartalmazza a B = hamis hozzárendelést, akkor a (B ∨ ¬C) egység klózzá válik, mivel ekvivalens a (Hamis ∨ ¬C)-vel, azaz a ¬C-vel. Természetesen ahhoz, hogy ez a klóz igaz legyen, C-nek hamis értéket kell adni. Az egységklóz heurisztika elvégzi ezeket a hozzárendeléseket, mielőtt elágazna a maradékon. Egy fontos konzekvenciája ennek a heurisztikának, hogy bármely, már a tudásbázisban található literálra vonatkozó (cáfolat általi) bizonyítási kísérlet azonnal sikeres lesz (7.16. feladat). Vegyük észre azt is, hogy értéket adva egy egységklózhoz újabb egységklózt hozhatunk létre. Például amikor C-nek hamis értéket adunk, akkor a (C ∨ A) egységklózzá válik, ami az igaz A-hoz való hozzárendelését eredményezi. Ezt az „egymást követő” kikényszerített hozzárendelések sorozatát egységterjesztésnek (unit propagation) nevezik. Hasonlít a folyamat a Horn-klózokkal történő előrefelé láncolásra, és valóban, abban az esetben ha a CNF formájú kifejezés csak Horn-klózokat tartalmaz, akkor a DPLL lényegében lemásolja az előrefelé láncolást (lásd 7.17. feladat).
7.16. ábra - A DPLL algoritmus ítéletkalkulus mondatok kielégíthetőségének ellenőrzése. A
TISZTA-SZIMBÓLUM-KERESÉS és az EGYSÉG-KLÓZ-KERESÉS eljárásokat a szövegben elmagyaráztuk; mindkettő egy szimbólummal vagy nullával tér vissza, és a szimbólumhoz hozzárendelendő igazságértékkel. Mint az IT-VONZAT? eljárás, ez is részleges modelleken dolgozik.
A DPLL algoritmust mutatja a 7.16. ábra. Az ábrán a lényeges elemeket tartalmazó vázat adtuk meg, ami bemutatja magát a keresési folyamatot. Nem szerepel az adatstruktúra leírása, amelyet fenn kell tartani, hogy a keresési lépéseket hatékonyan lehessen elvégezni, sem azoknak a trükköknek a leírása, amelyeket a teljesítmény fokozása céljából az alapalgoritmushoz hozzá lehet adni: klóztanulás, változó választási heurisztika és a véletlenszerű újraindítások technikája. Ha ezeket is beépítjük az algoritmusba, akkor a DPLL az egyik leggyorsabb kielégíthetőségi algoritmus, antikvitása ellenére is. A CHAFF implementáció millió változós hardververifikációs problémák megoldására szolgált.
Számos lokális keresés algoritmust láttunk már a könyvben, beleértve a HEGYMÁSZÓ algoritmust 4.3.1. szakasz - Hegymászó keresés részben és a SZIMULÁLT-LEHŰTÉS-t 4.3.2. szakasz - Szimulált lehűtés részben. Ezek az algoritmusok alkalmazhatók közvetlenül is kielégíthetőségi problémákra, feltéve, hogy megfelelő kiértékelő függvényt választunk. Mivel a cél egy olyan hozzárendelés megtalálása, amely kielégít minden klózt, megfelel számunkra egy olyan kiértékelő függvény választása, amely a kielégítetlen klózok számát számolja. Valóban, ez pontosan az a mérték, amit a MIN-KONFLIKTUS algoritmus használt kényszerkielégítési problémáknál 5.3. szakasz - Lokális keresés kényszerkielégítési problémáknál részben. Minden ilyen algoritmus a teljes hozzárendelések terében végez lépéseket, cserélgetve egy-egy lépésben egy-egy szimbólum igazságértékét. A tér rendszerint számos lokális minimumot tartalmaz, amelyekből a meneküléshez a véletlenszerű lépések különféle formái szükségesek. Az utóbbi években nagyon sokat foglalkoztak azzal a kérdéssel, hogy hogyan lehet egy jó egyensúlyt találni a mohóság és a véletlenszerűség között.
Az egyik legegyszerűbb és leghatékonyabb algoritmus, amely ezen munkák között felbukkant a WALKSAT (7.17. ábra). Minden iterációban az algoritmus vesz egy kielégítetlen klózt és egy szimbólumot a klózból, amelynek értékét ellenkezőre cseréli. Az értéket cserélő szimbólum kiválasztása a következő két módszer közül – véletlenszerűen választva – az egyikkel történik: (1) a „min-konfliktus” lépés, amely minimalizálja a kielégítetlen klózokat az új állapotban, és a (2) „véletlen-bejárás”, amely véletlenszerűen választja a szimbólumot.
7.17. ábra - A
WALKSAT algoritmus, kielégíthetőségének ellenőrzése véletlenszerűen cserélgetetett változó értékekkel. Számos változata ismert az algoritmusnak.
Működik-e egyáltalán a WALKSAT? Az egyértelmű, hogy ha visszaad egy modellt, akkor a bemeneti mondat valóban kielégíthető. Mi van akkor, ha kudarccal tér vissza? Sajnos ebben az esetben nem tudjuk megmondani, hogy a mondat kielégíthetetlen vagy az algoritmus számára több időt kellene hagyni a keresésre. Megpróbálhatjuk beállítani a max_csere értékét végtelenre. Erre az esetre könnyű megmutatni, hogy a WALKSAT végül vissza fog adni egy modellt (ha létezik ilyen), feltéve, hogy a p valószínűségre igaz a p > 0. Ez azért van így, mert mindig létezik egy olyan cserélési sorozat, amely elvezet egy kielégítő hozzárendeléshez, és előbb-utóbb a véletlen bejárás lépések elő fogják állítani ezt a sorozatot. Persze ha a max_csere végtelen, és a mondat kielégíthetetlen, akkor az algoritmus soha nem fog leállni!
Ezek az eredmények azt sugallják, hogy a lokális keresési algoritmusok, mint a WALKSAT, akkor a leginkább hasznosak, ha feltételezhetjük, hogy létezik megoldás – mint például a 3. és 5. fejezetben tárgyalt problémáknak általában van megoldásuk. Viszont a lokális keresés nem képes detektálni a kielégíthetetlenséget, amely szükséges a maga után vonzás kérdésének az eldöntéséhez. Például egy lokális keresést alkalmazó ágens nem tudja megbízhatóan bizonyítani, hogy egy négyzet biztonságos a wumpus világban. Ehelyett azt tudja mondani, hogy „Egy órája gondolkodom a kérdésen, és nem tudtam olyan lehetséges világot találni, amiben a négyzet nem biztonságos.” Ha a lokális keresés algoritmus általában igazán gyors egy modell megtalálásában, ha létezik ilyen, akkor az ágenst tekinthetjük igazolhatónak, feltételezve, hogy a kudarc a kielégíthetetlenséget jelzi. Ez természetesen nem azonos egy bizonyítással, és az ágensnek kétszer is meg kell gondolnia, mielőtt erre bízza az életét.
Most megnézzük, hogyan is teljesít a DPLL és a WALKSAT a gyakorlatban. Minket elsősorban a nehéz problémák érdekelnek, mert a könnyű problémák megoldhatóak bármely régi algoritmussal is. Az 5. fejezetben láttunk néhány meglepő felfedezést bizonyosfajta problémákkal kapcsolatban. Például az n-királynő probléma – amely igen kemény feladat volt a visszalépéses keresés számára – triviálisan egyszerűnek bizonyult az olyan lokális keresési módszerek számára, mint például a min-konfliktus. Ennek az az oka, hogy a megoldások nagyon sűrűn oszlanak el a hozzárendelések terében, és bármely kezdeti hozzárendeléshez garantáltan találhatunk egy megoldást a közelben. Tehát az n-királynő könnyű probléma, mert alulhatározott (underconstrained).
Amikor konjunktív normál formában levő kielégíthetőségi problémákat tekintünk, alulhatározott probléma az, amelyben viszonylag kevés a változókat korlátozó klóz szerepel. Például itt van egy véletlenszerűen létrehozott[71] 3-CNF mondat öt szimbólummal és öt klózzal:
(¬D ∨ ¬B ∨ C) ∧ (B ∨ ¬A ∨ ¬C) ∧ (¬C ∨ ¬B ∨ E) ∧ (E ∨ ¬D ∨ B) ∧ (B ∨ E ∨ ¬C)
A 32 lehetséges hozzárendelésből 16 modellje a mondatnak, így átlagosan csak két véletlenszerű találgatásra van szükség egy modell megtalálásához.
Akkor melyek a nehéz problémák? Feltételezhető, hogyha növeljük a klózok számát, miközben a szimbólumok számát rögzítve tartjuk, a problémát erősebben határozottá tesszük, és a megoldás megtalálása egyre nehezebbé válik. Legyen m a klózok száma és n a szimbólumok száma. A 7.18. (a) ábra mutatja annak a valószínűségét, hogy egy véletlenszerűen választott 3-CNF mondat kielégíthető-e a klóz/szimbólum arány (m/n) függvényében rögzített n = 50 mellett. Ahogy vártuk, kis m/n aránynál a valószínűség közel van 1-hez, és nagy m/n aránynál közel van a 0-hoz. A valószínűség viszonylag élesen esik le az m/n = 4,3 értéknél. Azok a CNF mondatok, amelyek közel vannak ehhez a kritikus ponthoz (critical point), „alig kielégíthetőnek” vagy „alig kielégíthetetlennek” jellemezhetők. Ez volna az, ahol a nehéz problémák vannak?
A 7.18. (b) ábra mutatja a DPLL és a WALKSAT futási időit ennek a pontnak a környezetében, csak a kielégíthető problémákat véve figyelembe. Három dolog tiszta: először is, a kritikus pont körüli problémák sokkal nehezebbek, mint a többi probléma. Másodszor, a DPLL igen hatékony még a legnehezebb problémákra is – átlagosan néhány ezer lépést tesz, összehasonlítva az igazságtábla felsorolás 250 ≈ 1015 számú lépésigényével. Harmadszor, a WALKSAT a teljes tartományban sokkal gyorsabb, mint a DPLL.
Természetesen ezek az eredmények csak a véletlenszerűen generált problémákra vonatkoznak. A valós problémáknak nem feltétlenül hasonló a struktúrájuk – a pozitív és negatív állítások aránya, a klózok közti kapcsolatok sűrűsége, és egyéb más vonatkozások – mint a véletlen problémáknak. Mégis, a gyakorlatban a WALKSAT és az ehhez kapcsolódó, hasonló algoritmusok nagyon jók valós problémák megoldásában is – gyakran ugyanolyan jók, mint az adott feladatra készített legjobb speciális célú algoritmus. Több ezer szimbólumot és milliónyi klózt tartalmazó problémákat megoldókkal szokás kezelni, mint amilyen a CHAFF. Ezek a megfigyelések azt sugallják, hogy a min-konfliktus és a véletlen bejárás algoritmusok valamilyen kombinációja általános célú képességet biztosít a legtöbb szituáció elemzéséhez, ahol kombinatorikai következtetés szükséges.
7.18. ábra - (a) A grafikon a klóz/szimbólum arány függvényében annak valószínűségét mutatja, hogy n = 50 mondat közül véletlenszerűen választott 3-CNF mondat kielégíthető-e. (b) A grafikon a DPLL és a
WALKSAT algoritmusok futási időinek középértékét mutatja 100 kielégíthető 3-CNF mondaton n = 50 mellett, a kritikus m/n arány melletti szűk sávban.
[71] Minden klóz három véletlenszerűen kiválasztott szimbólumot tartalmaz, amelyek 50% valószínűséggel negáltak.
