Title: Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization
Authors: Kovasznai, Gergely 
Gajdár, Krisztián 
Kovacs, Laura 
Keywords: SAT; SMT; optimization; formal methods; cardinality constraint
Issue Date: 15-Apr-2020
Book Title: Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing 
Abstract: 
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.
URI: http://hdl.handle.net/20.500.12708/16308
http://dx.doi.org/10.34726/341
DOI: 10.34726/341
Organisation: E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
License: Urheberrechtsschutz 1.0
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:

File Description SizeFormat Existing users please Login
S37_revised.pdfaccepted version499.44 kBAdobe PDFEmbargoed until March 30, 2022    Request a copy
Show full item record

Page view(s)

71
checked on Feb 21, 2021

Download(s)

9
checked on Feb 21, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.