Wikipédia

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 szerkesztés

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 szerkesztés

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 szerkesztés

Jegyzetek szerkesztés

  1. ↑ 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 0770156
  2. ↑ Buning (1995). „Resolution for Quantified Boolean Formulas”. Information and Computation 117 (1), 12–18. o, Kiadó: Elsevier. DOI:10.1006/inco.1995.1025.  
  3. ↑ Stephen Cook. Logical foundations of proof complexity. Cambridge University Press, 224. o. (2010). ISBN 978-0-521-51729-4 
  4. ↑ Lewis (1978). „Renaming a set of clauses as a Horn set”. Journal of the ACM 25 (1), 134–135. o. DOI:10.1145/322047.322059.  .
  5. ↑ Aspvall (1980). „Recognizing disguised NR(1) instances of the satisfiability problem”. Journal of Algorithms 1 (1), 97–103. o. DOI:10.1016/0196-6774(80)90007-3.  
  6. ↑ Hébrard (1994). „A linear algorithm for renaming a set of clauses as a Horn set”. Theoretical Computer Science 124 (2), 343–350. o. DOI:10.1016/0304-3975(94)90015-9.  .
  7. ↑ Chandru (2005). „On renamable Horn and generalized Horn functions”. Annals of Mathematics and Artificial Intelligence 1 (1–4), 33–47. o. DOI:10.1007/BF01531069.  
  8. ↑ Reiner Hähnle.szerk.: Dov M. Gabbay, Franz Günthner: Advanced many-valued logics, Handbook of philosophical logic, 2nd, Springer, 373. o. (2001). ISBN 978-0-7923-7126-7 
  9. ↑ Reiner Hähnle.szerk.: Melvin Fitting, Ewa Orłowska: Complexity of Many-valued Logics, Beyond two: theory and applications of multiple-valued logic. Springer (2003). ISBN 978-3-7908-1541-2 

Fordítás szerkesztés

  • Ez a szócikk részben vagy egészben a Horn-satisfiability 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.

További irodalom szerkesztés

A lap eredeti címe: „https://hu.wikipedia.org/w/index.php?title=Horn-kielégíthetőség&oldid=25888335”