Horn-kielégíthetőség
A formális logikában a Horn-kielégíthetőség vagy a HORNSAT annak eldöntése, hogy az adott Horn-klózok adott halmaza kielégíthető vagy nem. Alfred Hornról nevezték el a Horn-kielégíthetőséget, ahogyan a Horn-klózokat is.
Alapvető fogalommeghatározások és terminológia
A Horn-klóz olyan klóz, amelyben legfeljebb egy pozitív literál van, amelyet a klóz fejének nevünk, valamint tetszőleges számú negatív literál, amelyek a klóz testét alkotják. A Horn-formula egy Horn-klózok konjunkciójából képzett tételes formula.
A Horn-kielégíthetőség problémája lineáris időben megoldható.[1] A számszerűsített Horn-formulák igazságának eldöntése szintén megoldható polinomiális idő alatt.[2] A Horn-kielégíthetőség polinomiális idejű algoritmusa az egységszaporítás szabályán alapul: ha a formula egyetlen literálból álló klózt tartalmaz (egységklóz), akkor az összes olyan klóz, amely tartalmazza -t (kivéve magát az egységklózt) eltávolítjuk, és minden olyan záradékot, amely tartalmazza -t, szintén eltávolítunk. A második szabály eredménye maga is lehet egy egységklóz, amelyet ugyanilyen módon szaporítunk. Ha nincsenek egységklózok, akkor a formula úgy teljesíthető, hogy az összes fennmaradó változót egyszerűen negáltra állítjuk. A formula kielégíthetetlen, ha ez a transzformáció ellentétes egységkifejezések párját és generálja. A Horn-kielégíthetőség valójában az egyik „legnehezebb” vagy „legkifejezőbb” probléma, amelyről tudjuk, hogy polinomiális idő alatt kiszámítható, abban az értelemben, hogy P-teljes probléma.[3]
Ez az algoritmus lehetővé teszi a kielégíthető Horn-formulák igazsághozzárendelésének meghatározását is: az egység klózban szereplő összes változót az adott egységklóznak megfelelő értékre állítjuk; az összes többi literált hamisra állítjuk. Az eredményül kapott hozzárendelés a Horn-formula minimális modellje, azaz az a hozzárendelés, amelyhez a változók minimális halmaza igaznak van rendelve, ahol az összehasonlítás a halmazbehatárolás segítségével történik.
Lineáris algoritmust használva az egységszaporításhoz, az algoritmus a képlet méretében lineáris.
A Horn-formulák osztályának általánosítása az átnevezhető-Horn-formulák osztálya, amely azon formulák halmaza, amelyek Horn-formába hozhatók egyes változóknak a megfelelő negációval való helyettesítésével. Az ilyen csere létezésének ellenőrzése lineáris idő alatt elvégezhető; ezért az ilyen formulák kielégíthetősége P-ben van, mivel megoldható úgy, hogy először elvégezzük ezt a cserét, majd ellenőrizzük a kapott Horn-formula kielégíthetőségét.[4][5] [6][7] A Horn-féle kielégíthetőség és az átnevezhető Horn-féle kielégíthetőség a kielégíthetőség két fontos, polinomiális időben megoldható alosztályának egyike; a másik ilyen alosztály a 2-SAT.
A Horn-féle kielégíthetőségi probléma feltehető többértékű logikákra is. Az algoritmusok általában nem lineárisak, de némelyikük polinomiális; lásd Hähnle (2001, 2003) munkáit egy áttekintésért.[8] [9]
Duális Horn SAT
A Horn SAT duális változata a duális Horn SAT, amelyben minden klóznak legfeljebb egy negatív literálja van. Az összes változó negálása a duális Horn SAT egy példányát Horn SAT-á alakítja át. Horn 1951-ben bebizonyította, hogy a duális Horn SAT P-ben van.
Lásd még
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, MR 0770156Sablon:Citation
- ↑ Sablon:Cite journal
- ↑ Sablon:Hivatkozás/Könyv
- ↑ Sablon:Cite journal.
- ↑ Sablon:Cite journal
- ↑ Sablon:Cite journal.
- ↑ Sablon:Cite journal
- ↑ Sablon:Hivatkozás/Könyv
- ↑ Sablon:Hivatkozás/Könyv