Wikipédia

Cikkjelölt:Konfliktusvezérelt klóztanulás

Az informatikában a konfliktusvezérelt klóztanulás ( CDCL ) a Logikai kielégítési probléma (SAT) megoldására szolgáló algoritmus. Adott egy logikai képlet, a SAT-probléma változók hozzárendelését kéri, hogy a teljes képlet igaz legyen. A CDCL SAT megoldók belső működését a DPLL megoldók ihlették. A fő különbség a CDCL és a DPLL között az, hogy a CDCL visszaugrása nem kronologikus.

A konfliktus-vezérelt klózok tanulását Marques-Silva és Sakallah (1996, 1999) [1] [2], valamint Bayardo és Schrag (1997) javasolta. [3]

Háttér szerkesztés

Logikai kielégítési probléma szerkesztés

 Bővebben: Logikai kielégítési probléma

A kielégítési probléma abban áll, hogy egy adott képlethez megfelelő hozzárendelést találunk konjunktív normál formában (CNF).

( ( nem A ) vagy ( nem C ) ) és ( B vagy C ),

vagy egy általános jelöléssel: [4]

 

ahol A, B, C logikai változók,  ,  ,  , és   litárlok, és   és   klózok.

 

mivel igazzá teszi az első tagmondatot (hiszen   igaz), valamint a második (mivel   igaz).

Ez a példa három változót használ ( A, B, C ), és mindegyikhez két lehetséges hozzárendelés (igaz és hamis) van. Tehát az egyiknek van   lehetősége. Ebben a kis példában a brute-force keresést használhatjuk az összes lehetséges hozzárendelés kipróbálásához, és ellenőrizhetjük, hogy megfelelnek-e a képletnek.

De realisztikus alkalmazásokban, amelyekben milliónyi változó és klóz található, a brute force keresés nem praktikus. A SAT-megoldó feladata, hogy hatékonyan és gyorsan megtalálja a kielégítő feladatot összetett CNF-képletek különböző heurisztikáinak alkalmazásával.

Egységkikötés szabály (egységterjesztés) szerkesztés

Ha egy nem kielégítő klóznak egy kivételével minden literálja vagy változója Hamis értékkel van kiértékelve, akkor a szabad literálnak igaznak kell lennie ahhoz, hogy a klóz igaz legyen. Például, ha az alábbi nem kielégítő klózot a következővel értékeljük ki   és   nekünk kell hogy legyen   a klóz érdekében   hogy igaz legyen.

Az egységklóz-szabály iterált alkalmazását egységterjesztésnek vagy Boole-kényszer-terjesztésnek (BCP) nevezik.

Felbontás szerkesztés

Vegyünk két kitételt   és   . A klóz  , amelyet a két klóz egyesítésével és mindkettő eltávolításával kapunk   és  , a két klóz oldójának nevezzük.

Algoritmus szerkesztés

A konfliktus-vezérelt klózok tanulása a következőképpen működik.

  1. Válasszon ki egy változót, és rendelje hozzá az igaz vagy hamis értéket. Ezt döntési állapotnak nevezik. Emlékezzen a feladatra.
  2. Alkalmazza a logikai kényszer propagációt (unit propagáció).
  3. Építsd meg az implikációs gráfot .
  4. Ha bármilyen konfliktus van
    1. Keresse meg az implikációs grafikonon azt a vágást, amely az ütközéshez vezetett
    2. Hozz létre egy új klózot, amely a konfliktushoz vezető hozzárendelések tagadása
    3. Nem kronologikusan visszalépni ("visszaugrás") a megfelelő döntési szintre, ahol az elsőként hozzárendelt, a konfliktusban érintett változót hozzárendelték
  5. Ellenkező esetben folytassa az 1. lépéstől, amíg az összes változóértéket hozzá nem rendeli.

Példa szerkesztés

A CDCL algoritmus vizuális példája: [4]

  •  
    Első elágazó változónál válasszuk az x1-et. A sárga kör tetszőleges döntést jelent.
  •  
    Most alkalmazza a unit propagációt, ami azt eredményezi, hogy x4-nek 1-nek kell lennie (azaz igaznak). A szürke kör a unit propagáció során kényszerített változó hozzárendelést jelent. Az így kapott gráfot implikációs gráfnak nevezzük.
  •  
    Tetszőlegesen válasszon másik elágazó változót, az x3-at.
  •  
    Alkalmazza a unit propagációt, és keresse meg az új implikációs gráfot.
  •  
    Itt az x8 és x12 változók 0-ra, illetve 1-re vannak kényszerítve.
  •  
    Válasszon egy másik elágazó változót, x2.
  •  
    Keresse meg az implikációs gráfot.
  •  
    Válasszon egy másik elágazási változót, az x7-et.
  •  
    Keresse meg az implikációs gráfot.
  •  
    Talált konfliktust!
  •  
    Find the cut that led to this conflict. From the cut, find a conflicting condition.
  •  
    Take the negation of this condition and make it a clause.
  •  
    Add the conflict clause to the problem.
  •  
    Non-chronological back jump to appropriate decision level, which in this case is the second highest decision level of the literals in the learned clause.
  •  
    Back jump and set variable values accordingly.

Teljesség szerkesztés

A DPLL egy megbízható és teljes algoritmus a SAT számára. A CDCL SAT megoldói megvalósítják a DPLL-t, de megtanulhatnak új klózokat, és nem kronologikusan léphetnek vissza. A konfliktuselemzéssel végzett klóztanulás nem befolyásolja sem a megalapozottságot, sem a teljességet. Az ütközéselemzés a feloldási művelet segítségével azonosítja az új klózokat. Ezért minden tanult tagmondat kikövetkeztethető az eredeti és a többi tanult tagmondatból a feloldási lépések sorozatával. Ha cN az új tanult klóz, akkor ϕ akkor és csak akkor teljesíthető, ha ϕ ∪ {cN} is kielégíthető. Ezen túlmenően a módosított visszalépési lépés sem befolyásolja a megbízhatóságot vagy a teljességet, mivel a visszalépési információkat minden új tanult klózból kapjuk. [5]

Alkalmazások szerkesztés

A CDCL algoritmus fő alkalmazása a különböző SAT-megoldókban található, beleértve:

  • MiniSAT
  • Zchaff SAT
  • Z3
  • Glükóz [6]
  • ManySAT stb.

A CDCL algoritmus olyan erőssé tette a SAT-megoldókat, hogy hatékonyan használják azokat számos valós alkalmazási területen, mint például a mesterséges intelligencia tervezése, bioinformatika, szoftverteszt-minta generálása, szoftvercsomag-függőségek, hardver- és szoftvermodell-ellenőrzés és kriptográfia.

Kapcsolódó algoritmusok szerkesztés

A CDCL-hez kapcsolódó algoritmusok a Davis–Putnam algoritmus és a DPLL algoritmus . A DP algoritmus felbontás cáfolatokat használ, és lehetséges memóriaelérési problémája van. Míg a DPLL algoritmus megfelelő a véletlenszerűen generált példányokhoz, rossz a gyakorlati alkalmazásokban generált példányokhoz. A CDCL hatékonyabb megoldás az ilyen problémák megoldására, mivel a CDCL alkalmazása kevesebb állapottér-keresést biztosít a DPLL-hez képest.

Hivatkozott munkák szerkesztés

  1. ↑ J.P. Marques-Silva. GRASP-A New Search Algorithm for Satisfiability, Digest of IEEE International Conference on Computer-Aided Design (ICCAD), 220–227. o.. DOI: 10.1109/ICCAD.1996.569607 (1996. november 1.). ISBN 978-0-8186-7597-3 
  2. ↑ J.P. Marques-Silva (1999. május 1.). „GRASP: A Search Algorithm for Propositional Satisfiability”. IEEE Transactions on Computers 48, 506–521. o. DOI:10.1109/12.769433.  
  3. ↑ Roberto J. Bayardo Jr.. Using CSP look-back techniques to solve real world SAT instances, Proc. 14th Nat. Conf. on Artificial Intelligence (AAAI), 203–208. o. (1997) 
  4. ↑ a b In the pictures below, " " is used to denote "or", multiplication to denote "and", and a postfix " " to denote "not".
  5. ↑ Biere, Heule, Van Maaren, Walsh. Handbook of Satisfiability. IOS Press, 138. o. (2009. február 1.). ISBN 978-1-60750-376-7 
  6. ↑ Glucose's home page

Hivatkozások szerkesztés

  • Martin Davis (1960). „A Computing Procedure for Quantification Theory”. J. ACM 7, 201–215. o. DOI:10.1145/321033.321034.  
  • Martin Davis (1962. július 1.). „A machine program for theorem-proving”. Communications of the ACM 5, 394–397. o. DOI:10.1145/368273.368557.  
  • Matthew W. Moskewicz. Chaff: engineering an efficient SAT solver, Proc. 38th Ann. Design Automation Conference (DAC), 530–535. o. (2001) 
  • Lintao Zhang. Efficient conflict driven learning in a boolean satisfiability solver, Proc. IEEE/ACM Int. Conf. on Computer-aided design (ICCAD), 279–285. o. (2001) 
  • Presentation – "SAT-Solving: From Davis-Putnam to Zchaff and Beyond" by Lintao Zhang. (Several pictures are taken from his presentation)
A lap eredeti címe: „https://hu.wikipedia.org/w/index.php?title=Cikkjelölt:Konfliktusvezérelt_klóztanulás&oldid=26146056”