Kovasznai, G., Gajdár, K., & Kovács, L. (2020). Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 85–91). IEEE. https://doi.org/10.34726/341
Wireless Sensor Networks (WSNs) serve as the
basis for Internet of Things applications. A WSN consists
of a number of spatially distributed sensor nodes, which
cooperatively monitor physical or environmental conditions.
In order to ensure the dependability of WSN functionalities, several reliability and security requirements have to be
fulfilled. In previous work, we applied OMT (Optimization
Modulo Theories) solvers to maximize a WSN’s lifetime, i.e.,
to generate an optimal sleep/wake-up scheduling for the sensor
nodes. We discovered that the bottleneck for the underlying
SMT (Satisfiability Modulo Theories) solvers was typically to
solve satisfiable instances. In this paper, we encode the WSN
verification problem as a set of Boolean cardinality constraints,
therefore SAT solvers can also be applied as underlying solvers.
We have experimented with different SAT solvers and also with
different SAT encodings of Boolean cardinality constraints.
Based on our experiments, the SAT-based approach is very
powerful on satisfiable instances, but quite poor on unsatisfiable
ones. In this paper, we apply both SAT and SMT solvers in a
portfolio setting. Based on our experiments, the MiniCARD+Z3
setting can be considered to be the most powerful one, which
outperforms OMT solvers by 1-2 orders of magnitude.
en
Projekttitel:
Symbolic Computation and Automated Reasoning for Program Analysis: 639270 (European Commission) Symbol Elimination in Reliable System Engineering: 842066 (European Commission)
