SAT representation of randomly deployed Wireless Sensor Networks
Csaba Bíró, Gábor Kusper, Tibor Radványi, Sándor Király, Péter Szigetváry, Péter Takács · 2015
Wireless sensor networks consist of numerous -mainly low-cost -sensors.These systems main purpose is to collect environmental data and transmit those measurements.Each sensor can communicate through broadcasting to other sensors in their broadcasting range.There are several requirements that a wireless sensor network should satisfy.One of the most important question is whether communication among all the sensor nodes is possible.In this paper we introduce two logical models that are suitable to represent wireless sensor networks.We generate SAT problems from the network communication model and the restrictions defining expected behavior, which are then analyzed with SAT solvers.The SAT solvers are used for model inspection.Whereby if a requirement is fulfilled, the SAT solver cannot find a substitution value for the function, otherwise the substitution value produced by the SAT solver appoints a counterexample.Current modern SAT solvers are capable to examine the satisfiability of SAT problems having thousands of variables, thus being able to decide even in huge sensor networks that the model fulfills the defined requirements (the degree of fault tolerance or power consumption, etc.)