Várterész, MagdaLengyel, Zoltán2006-06-192006-06-1920052006-06-19http://hdl.handle.net/2437/117Azon algoritmusok, melyek hatékonyan képesek kezelni a valós életben felmerülő Boole-függvényeket, egyre népszerűbbek a nagymértékben integrált (VLSI) rendszerek számítógéppel támogatott tervezése és hitelesítése területén. Az egyik ilyen algoritmus-csoportba a bináris döntési diagramokat (BDD-ket) előállító és manipuláló algoritmusok tartoznak. Ilyen algoritmusok egy másik osztálya a SAT-fejtők 1 csoportja , melyről dolgozatomban csak érintőlegesen esik szó. A BDD-k, pontosabban annak egy szűkebb csoportja, a redukált rendezett BDD-k (OBDD-k) gyakran kerülnek előtérbe rendszerek szintézisénél és hitelesítésénél felmerülő problémák terjedelmes megoldásterének bemutatásakor. A BDD egy irányított körmentes gráf (DAG), melynek irányított élei egy-egy változó értékelését jelölik. Habár a BDD-kben az utak száma exponenciális függvénye a csúcsok és élek számának, azaz a gráf méretének, ezen gráfok olyan algoritmusok segítségével manipulálhatóak, melyek a bejárás során az BDD minden csúcsán és élén legfeljebb egyszer haladnak át, ezáltal a futásidő a gráf aktuális méretével polinomiális arányban növekszik. Azonban egy BDD előállítása során, napjaink algoritmusait használva, jelentősen megnő, majd általában csökken a BDD csúcsainak száma, mely exponenciális tár és futásidőt igényel. A SAT fejtők és a BDD-k közös tulajdonsága, hogy az ítéletváltozók sorrendje különösen fontos szerepet játszik az algoritmusok hatékonyságában. Különféle BDD rendezési módszerek léteznek, melyek között vannak statikus valamint dinamikus megközelítések. Erről bővebben a 3.2. fejezetben lesz szó. A BDD-k szerepének felfedezése óta több jelentős programcsomag is készült, mint például a CUDD vagy a BuDDy csomagok. Ezekről csak röviden ejtünk szót a 4. fejezet bevezetőjében.38329855 bytesapplication/pdfhuno_restrictionBDDOBDDdöntési diagramokCADVISICADBMCModell-ellenőrzés