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ó

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 $l$ egységklózt, a többi klózt a következő két szabály alkalmazásával egyszerűsítjük:

1. minden klóz (kivéve magát az egységklózt), amely tartalmazza $l$-t törlésre kerül (a klóz teljesül, ha $l$ is);
2. minden olyan klózban, amely tartalmazza $\neg l$-t, ezt a literált töröljük ($\neg l$ 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 $a$ klózt.

$\{a\vee b,\neg a\vee c,\neg c\vee d,a\}$

Mivel $a\vee b$ tartalmazza az $a$ literált, ez a klóz teljesen eltávolítható. Mivel $\neg a\vee c$ tartalmazza az egységklózban szereplő literál tagadását, ez a literál eltávolítható a klózból. Az $a$ 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.

$\{$	$a\vee b,$	$\neg a\vee c,$	$\neg c\vee d,$	$a$	$\}$
	( $a$ törölve)	(eltávolítva)	(változatlan)	(változatlan)
$\{$		$c,$	$\neg c\vee d,$	$a$	$\}$

Az így kapott klózok halmaza $\{c,\neg c\vee d,a\}$ egyenértékű a fentiekkel. Az új egységklóz $c$, 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 $\neg c\vee d$ klózt $d$-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 $\neg a$ klózt.

$\{a\vee b,\neg a\vee c,\neg c\vee d,\neg a\}$

$\{$	$a\vee b,$	$\neg a\vee c,$	$\neg c\vee d,$	$\neg a$	$\}$
	(eltávolítva)	( $\neg a$ törölve)	(változatlan)	(változatlan)
$\{$	$b,$		$\neg c\vee d,$	$\neg a$	$\}$

Az így kapott klózok halmaza $\{b,\neg c\vee d,\neg a\}$ egyenértékű a fentiekkel. Az új egységklóz $b$, amely az egységszaporítás eredménye, ezen már nem tudunk egységszaporítást végezni, így ebben az esetben $\{b,\neg c\vee d,\neg a\}$ marad a klózhalmaz.

Az egységszaporítás és a rezolúció

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:

1. 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;
2. 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;
3. 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

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 $a$ 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 $a$ 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

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:

$\{1:a\vee b,2:\neg a\vee c,3:\neg c\vee d,4:a\}$

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:

$a:1\ 2\ 4$

$b:1$

$c:2\ 3$

$d:3$

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

• Kürt kielégíthetőség
• Horn-Klóz
• Automatizált tételbizonyítás
• DPLL algoritmus

Jegyzetek

• .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

• 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.