Egységszaporítás
Az egységszaporítás vagy a Boolean korlátozás szaporítás (Boolean Constraint propagation, BCP) vagy az egy literál szabály (one literal rule, OLR) az automatizált tételbizonyítás olyan algoritmusa, amely képes egyszerűsíteni a (általában ítéletlogikai) klózok halmazát.
Definíció
[szerkesztés]Az eljárás egységklózokon alapul, azaz olyan klózokon, amelyek egyetlen literálból állnak, konjunktív normálformában. Mivel minden egyes klóznak teljesülnie kell, tudjuk, hogy ennek a literálnak igaznak kell lennie. Ha a klózok halmaza tartalmazza az egységklózt, a többi klózt a következő két szabály alkalmazásával egyszerűsítjük:
- minden klóz (kivéve magát az egységklózt), amely tartalmazza -t törlésre kerül (a klóz teljesül, ha is);
- minden olyan klózban, amely tartalmazza -t, ezt a literált töröljük ( ugyanis nem tud hozzájárulni az kielégíthetőséghez).
E két szabály alkalmazása egy új klózkészletet eredményez, amely egyenértékű a régivel.
Például a következő klózhalmaz egyszerűsíthető egységszaporítással, mert tartalmazza az klózt.
Mivel tartalmazza az literált, ez a klóz teljesen eltávolítható. Mivel tartalmazza az egységklózban szereplő literál tagadását, ez a literál eltávolítható a klózból. Az klóz nincs eltávolítva; így a kapott halmaz nem egyenértékű az eredetivel; ez a klóz eltávolítható, ha már más formában van tárolva (lásd a #Részleges modell használata szakaszt). Az egységszaporítás hatása a következőképpen foglalható össze.
( törölve) | (eltávolítva) | (változatlan) | (változatlan) | ||
Az így kapott klózok halmaza egyenértékű a fentiekkel. Az új egységklóz , amely az egységszaporítás eredménye, felhasználható az egységszaporítás egy további alkalmazásához, amely átalakítja a klózt -re.
Nézzünk még egy példát. A következő klózhalmaz egyszerűsíthető egységszaporítással, mert tartalmazza a klózt.
(eltávolítva) | ( törölve) | (változatlan) | (változatlan) | ||
Az így kapott klózok halmaza egyenértékű a fentiekkel. Az új egységklóz , amely az egységszaporítás eredménye, ezen már nem tudunk egységszaporítást végezni, így ebben az esetben marad a klózhalmaz.
Az egységszaporítás és a rezolúció
[szerkesztés]Az egységszaporítás második szabálya a rezolúció egy korlátozott formájának tekinthető, amelyben a két rezolvens közül az egyiknek mindig klóznak kell lennie. A rezolúcióhoz hasonlóan az egységszaporítás is helyes következtetési szabály, mivel soha nem hoz létre olyan új klózt, amelyet a régiek nem vonnak maguk után. Az egységszaporítás és a rezolúció közötti különbségek a következők:
- a rezolúció egy teljes cáfolási eljárás, míg az egységszaporítás nem az; más szóval, még ha a klózok egy halmaza ellentmondásos is, az egységszaporítás nem hozhat létre ellentmondást;
- két rezolvált klózt általában nem lehet eltávolítani, miután a generált klózt hozzáadták a halmazhoz; ezzel szemben az egységszaporításban részt vevő nem egységklóz eltávolítható, amikor az egyszerűsítése hozzáadódik a halmazhoz;
- a rezolúció általában nem tartalmazza az egységszaporításban használt első szabályt.
A rezolúciót tartalmazó hierarchiaszámítások modellezhetik az egyes szabályt alárendeléssel, a második szabályt pedig egy egységnyi rezolúciós lépéssel, majd ezt alárendeléssel.
Az egységszaporítás, amelyet ismételten alkalmaznak, amikor új egységklózokat generálnak, egy teljes kielégíthetőségi algoritmus a Horn-klózok halmazaira; ha kielégíthető, akkor egy minimális modellt is generál a halmazra: lásd Horn-kielégíthetőség.
Részleges modell használata
[szerkesztés]Az egység klózok, amelyek egy klózkészletben szerepelnek vagy abból származtathatók, egy modell részleges formájában tárolhatók (ez a részleges modell az alkalmazástól függően más literálokat is tartalmazhat). Ebben az esetben az egységszaporítás a részleges modell literáljai alapján történik, és az egységklózok eltávolításra kerülnek, ha a literáljuk szerepel a modellben. A fenti példában az egységklózt hozzá kell adni a részleges modellhez; a klóz egyszerűsítése ezután a fentiek szerint történne, azzal a különbséggel, hogy az egységklóz most eltávolításra került a halmazból. Az így kapott klózhalmaz a részleges modellben szereplő literálok érvényességének feltételezése mellett egyenértékű az eredetivel.
Bonyolultság
[szerkesztés]Az egységszaporítás közvetlen megvalósítása az ellenőrizendő halmaz teljes méretében négyzetes időigényű, amely az összes klóz méretének összege, ahol az egyes klózok mérete a bennük szereplő literálok száma.
Az egységszaporítás azonban lineáris idő alatt is elvégezhető, ha minden egyes változóhoz tároljuk azoknak a klózoknak a listáját, amelyekben az egyes literálok szerepelnek. A fenti halmaz például úgy ábrázolható, hogy az egyes klózokat a következőképpen számozzuk:
majd minden egyes változóhoz tárolja a klózok listáját, amelyek tartalmazzák a változót vagy negáltját:
Ez az egyszerű adatszerkezet a halmaz méretével lineárisan megegyező idő alatt építhető fel, és nagyon könnyen lehetővé teszi a változót tartalmazó összes klóz megtalálását. Egy literál egységszaporítása hatékonyan elvégezhető úgy, hogy csak a literál változóit tartalmazó klózok listáját vizsgáljuk át. Pontosabban, a teljes futási idő az egységszaporítás elvégzéséhez az összes egységklóz esetében lineárisan arányos a klózok halmazának méretével.
Lásd még
[szerkesztés]- Kürt kielégíthetőség
- Horn-Klóz
- Automatizált tételbizonyítás
- DPLL algoritmus
Jegyzetek
[szerkesztés]- .Dowling, William F. & Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming 1 (3): 267–284, DOI 10.1016/0743-1066(84)90014-1
- H. Zhang és M. Stickel (1996). Hatékony algoritmus az egységnyi terjedéshez. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics .
Fordítás
[szerkesztés]- Ez a szócikk részben vagy egészben az Unit propagation című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.