SAT reprezentációk vezeték nélküli szenzorhálózatokhoz
Biró Csaba
<>
Eszterházy Károly Főiskola
Kusper Gábor
<>
Eszterházy Károly Főiskola
Cikkünkben bemutatunk néhány, a vezeték nélküli szenzorhálózatok reprezentálására alkalmas logikai modellt. A vezeték nélküli szenzorhálózatok nagyszámú, elsősorban olcsó szenzorokból állnak. Ezen rendszerek elsődleges célja a környezetből érkező adatok gyűjtése és továbbítása. Az egyes szenzorok üzenetszórással képesek kommunikálni a szórási tartományukon belüli szenzorokkal. Egy vezeték nélküli szenzorhálózatoknak számos követelménynek kell eleget tennie. Az egyik legfontosabb kérdés, hogy a szenzorok közötti (mindenki-mindenkivel) kommunikáció lehetséges-e? A szenzorhálózat modelljéből és a megszorításokból SAT problémákat generálunk, majd azt SAT solver segítségével ellenőrizzük. A mai modern SAT solver-ek képesek akár több ezer változóból álló SAT problémák kielégíthetőségének vizsgálatára, így nagy szenzorhálózatok esetében is képesek rövid idő alatt eldönteni, hogy a modell a definiált követelményrendszernek (pl. hibatűrés foka, energiafelhasználás) eleget tesz-e.