<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY),
September</journal-title>
      </journal-title-group>
    </journal-meta>
    <article-meta>
      <title-group>
        <article-title>Optimal Fault-Tolerant Relay Node Positioning in Critical Wireless Networks via Artificial Intelligence</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Qian Matteo Chen</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Toni Mancini</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Igor Melatti</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Enrico Tronci</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Alberto Finzi</string-name>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Computer Science Dept., Sapienza University of Rome</institution>
          ,
          <country country="IT">Italy</country>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>Dept. Electrical Engin. and Information Tech., University of Naples Federico II</institution>
          ,
          <country country="IT">Italy</country>
        </aff>
      </contrib-group>
      <pub-date>
        <year>2020</year>
      </pub-date>
      <volume>25</volume>
      <issue>2020</issue>
      <fpage>41</fpage>
      <lpage>46</lpage>
      <abstract>
        <p>Radio communication networks in critical infrastructures like airports are often mission-critical, and must be adequately protected from external electromagnetic interference and attacks. Given the long distances involved and the need to use low-powered WiFi signals, intermediate relay nodes must be deployed on the field to ensure multi-hop reliable communication, also guaranteeing a sufficient degree of fault-tolerance. In this short paper, we introduce the problem and briefly review our recent approach to automatically synthesise a cost-optimal fault-tolerant relay network. Differently from ad-hoc or heuristic approaches, our tool-chain is entirely based on off-the-shelf Artificial Intelligence general-purpose reasoners, namely MILP, PB-SAT, and SMT/OMT solvers. We also show experimental results on large scenarios from the Leonardo da Vinci Airport in Rome, Italy.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Introduction</title>
    </sec>
    <sec id="sec-2">
      <title>Problem requirements</title>
      <p>The installation of relay nodes in a large critical area like an airport (the Monitored Area, MA), entails
the cost of the hardware (e.g., antennas and amplifiers), and the cost their actual deployment. The latter
may be quite relevant: for instance, deploying a relay node in an airport may require installing antennas
within a ground movement area, and this might yield additional costs to neutralise any impact on the
airport operations. In our setting, relay antennas are directional antennas, hence they are deployed in
arrays mounted on poles. Each antenna array is positioned at a given elevation from the ground (the
height of the poles). Antennas mounted on the same pole are pointed to different directions (among a
user-specified finite set of possible directions).</p>
      <p>Our problem amounts to decide where in the MA and with which orientation to deploy relay antennas
in order to satisfy all given requirements while minimising the overall deployment and hardware cost.</p>
      <p>The problem requirements are quite intricate, because several aspects must be taken into account.
First of all, since the MA might have a size of several squared kilometres, different regions might have
different ground elevation, and obstacles of various types (e.g., terminals, hangars) might exist. Thus,
radio visibility between points in the MA cannot be determined by simply considering their Euclidean
distance, but obstacles and terrain orography should be considered as well. Starting from MA orography
data from existing databases, we represent both the MA and obstacles as a set of convex polyhedra in
a Cartesian 3D bounded space. The MA may also include forbidden placement areas, i.e., areas (e.g.,
runways, taxiways, holding areas) where no relay node can be placed. Also, forbidden link areas may exist,
which represent regions of the MA that should not be traversed by radio transmission links (e.g., to avoid
interferences with other existing radio networks). Furthermore, the cost of deploying an antenna array is
not constant throughout the MA, as it might depend on several parameters (e.g., the accessibility of the
chosen point for maintenance). We represent forbidden placement, forbidden link areas, and areas with
different positioning costs using sets of convex polyhedra within our 3D Cartesian bounded space.</p>
      <p>
        Additional requirements need to be suitably addressed to make our computed solution acceptable. In
particular, radio visibility requirements, which define the conditions that must be met by the deployment
of pairs of directional relay antennas for their network links to be of satisfactory quality, need some
domain-specific reasoning: indeed, radio communication between two (oriented) antennas in points of the
MA must be considered impossible/unsatisfactory not only if the 3D Euclidean distance between them is
longer than a given threshold, but also if the presence of obstacles, buildings, or terrain elevation changes,
makes their prospective radio link suffer from excessive interference. This latter step requires so called
Fresnel-zone analysis [
        <xref ref-type="bibr" rid="ref24">24</xref>
        ].
      </p>
      <p>The remaining requirements are as follows. Fault tolerance requirements ask that the network to be
designed guarantees successful routing from each sensor to the gateway also in case of malfunctioning of
at most F ≥ 1 relay nodes. This is addressed by computing a relay node placement defining at least F + 1
distinct routes from each sensor to the gateway, with no distinct routes from the same sensor sharing a
relay node. Performance requirements ask that each sensor-to-gateway route in the designed network
consists of at most H ≥ 1 hops. Finally, network capacity requirements ask that the network is able to
convey the needed traffic from all the sensors to the gateway. This means that there is an upper bound to
the number of messages (from sensor nodes) that can be routed through a given radio link per second.
3</p>
    </sec>
    <sec id="sec-3">
      <title>Computing optimal fault-tolerant placement of relay nodes</title>
      <p>
        Given the intricate requirements outlined in Section 2, a possible approach to solve our problem is to
develop a specialised ad-hoc algorithm. However, such an approach would be costly and error-prone,
and proving optimality of the computed solution would be not easy. In [
        <xref ref-type="bibr" rid="ref14 ref49">49, 14</xref>
        ] we proposed a radically
different approach in three steps, where all steps extensively use standard AI reasoners to produce
correctby-construction outputs. This keeps the code-base at a minimum, greatly reduces the cost for ad-hoc
development and testing, and removes altogether the cost to obtain a proof of optimality of the final
solution. The main steps of our algorithm are as follows.
      </p>
      <p>MA discretisation. Starting from an input scenario (namely, the definition of the MA with associated
polyhedra for terrain elevation, obstacles, and forbidden placement areas), our algorithm discretises the
Optimal Fault-Tolerant Relay Node Positioning in Critical Wireless Networks via Artificial Intelligence43
MA into a number of cells (of user-specified size) where an array of relay antennas can indeed be deployed.</p>
      <p>
        Parallel computation of the radio visibility graph. A parallel pre-processing step is then
performed, in order to compute a data structure called radio visibility graph. Nodes of the graph define the set
of possible placements of poles (pole nodes) within the cells of the MA computed in the previous step, as
well as possible installations of directional antennas on such poles (antenna nodes). Undirected edges of the
graph define the possibility to establish reliable communication links between two antenna nodes installed
on different poles with any user-defined orientation (this includes Fresnel-zone analysis and avoidance of
forbidden link areas via constraint-based over-approximation [
        <xref ref-type="bibr" rid="ref23 ref43">23, 43</xref>
        ]), and the wired communication links
between each pole and locally-installed antennas. To compute the radio visibility graph, a set of helper
computational geometry problems similar to those in [
        <xref ref-type="bibr" rid="ref37">37</xref>
        ] are automatically generated as MILPs, and
solved in parallel on a High-Performance Computing (HPC) infrastructure.
      </p>
      <p>
        Generation and solving of the main optimisation problem. Our main optimisation problem
is automatically modelled as a 0/1 Linear Program (0/1-LP). Our developed tool performs suitable
optimisations of the problem formulation along the lines of [
        <xref ref-type="bibr" rid="ref11 ref38">11, 38</xref>
        ]. The obtained 0/1-LP is encoded into
the languages supported by several state-of-the art general-purpose reasoners based on different paradigms,
namely: MILP, PB-SAT, and SMT/OMT. Any such solver can then be used as a computational engine.
4
      </p>
    </sec>
    <sec id="sec-4">
      <title>Experimental results and scalability of the approach</title>
      <p>We experimented with several scenarios defining various areas of the Leonardo Da Vinci Airport in Rome,
Italy, whose areas range from 10 000 m2 to 50 km2. By varying the size of the cells, the maximum number
of hops H, and the fault tolerance degree F , we generated 366 0/1-LPs, with 309 to about 6 million
zero-one variables and 378 to about 8 million constraints.</p>
      <p>
        Such 0/1-LPs were generated in up to 500 seconds each on an HPC infrastructure with 64 nodes,
and have been solved using a portfolio of 8 state-of-the-art solvers of different kinds: MILP solvers IBM
CPLEX [
        <xref ref-type="bibr" rid="ref27">27</xref>
        ], GLPK [
        <xref ref-type="bibr" rid="ref2">2</xref>
        ], and Gurobi [
        <xref ref-type="bibr" rid="ref25">25</xref>
        ]; PB-SAT solvers MiniSAT+ [
        <xref ref-type="bibr" rid="ref19">19</xref>
        ] (based on the well-known SAT
solver MiniSAT [
        <xref ref-type="bibr" rid="ref18">18</xref>
        ], was one of the winners of the 2005 PB-SAT Evaluation [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ]), NAPS [
        <xref ref-type="bibr" rid="ref57">57</xref>
        ], and Sat4j
[
        <xref ref-type="bibr" rid="ref32">32</xref>
        ] (the last two won different tracks of the 2006 PB-SAT Competition [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ]); SMT/OMT solvers Z3 [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ]
(which supports linear optimisation problems through νZ [
        <xref ref-type="bibr" rid="ref10">10</xref>
        ]) and OptiMathSat [
        <xref ref-type="bibr" rid="ref58">58</xref>
        ].
      </p>
      <p>
        Our experiments show (see [
        <xref ref-type="bibr" rid="ref14">14</xref>
        ] for our full experimental campaign) that all solvers were able to
solve real-world and hard instances of such an industry-relevant optimisation problem, consisting of a
remarkably high number of constraints. In more details, MILP solvers were able to solve, within our
time limit of 3 hours, the greatest number of and the largest instances (i.e., instances with up to around
2 million constraints), with CPLEX clearly being the top-performer, followed by Gurobi and GLPK.
PB-SAT solvers succeeded to solve instances with up to around half-a-million constraints (with Sat4j
being able to solve some of the largest instances, MiniSat+ immediately following, and NAPS lagging
behind). Noticeably, the performance of PB-SAT solvers are competitive to those of MILP solvers on
unsatisfiable instances. OMT solvers were able to solve fewer of the largest instances, with Z3 slightly
outperforming OptiMathSat. In general, OMT solvers seem to have harder time in finding an optimal
solution on satisfiable instances, and generally show better performance on unsatisfiable instances.
5
      </p>
    </sec>
    <sec id="sec-5">
      <title>Related work</title>
      <p>
        Although node placement in wireless sensor networks is a well-studied problem (e.g., the survey in [
        <xref ref-type="bibr" rid="ref64">64</xref>
        ]),
none of the available methods focuses on finding a cost-minimal placement while at the same time
guaranteeing network connectivity notwithstanding loss (faults) of up to a given number of relay nodes.
For example, [
        <xref ref-type="bibr" rid="ref55">55</xref>
        ] presents methods for optimal and robust (with respect to throughput degradation)
positioning of relay nodes. However, robustness in [
        <xref ref-type="bibr" rid="ref55">55</xref>
        ] is not the same as fault-tolerance in our setting.
Optimal positioning of relay nodes in a WiFi network (our setting) has been studied also in [
        <xref ref-type="bibr" rid="ref54">54</xref>
        ], where,
however, fault-tolerance (a key point in our setting), is not addressed. Other available approaches sacrifice
optimality and a priori guarantees, and perform some sorts of random placements of relay nodes (see
references in [
        <xref ref-type="bibr" rid="ref64">64</xref>
        ]) or employ heuristic methods (see, e.g., [
        <xref ref-type="bibr" rid="ref26 ref8">8, 26</xref>
        ]).
      </p>
      <p>
        Network traffic, congestion and interference have been analysed in [
        <xref ref-type="bibr" rid="ref33">33</xref>
        ] using MILP, while [
        <xref ref-type="bibr" rid="ref34">34</xref>
        ] focuses
on the transmission capacity of ad-hoc networks. The relationship between energy consumption of network
relay nodes and routing strategies is studied in [
        <xref ref-type="bibr" rid="ref13">13</xref>
        ] as a maximum flow problem, which is solved with a
combination of MILP and heuristic approaches. In our setting, we do not have energy problems, since
relays are connected to the electrical grid. Conversely, our main focus is to find a positioning of both
the relay nodes and antennas with minimal cost. Modelling obstacles for radio communication in a real
environment has been investigated in [
        <xref ref-type="bibr" rid="ref30">30</xref>
        ], and a 2D model for directional antennas is presented in [
        <xref ref-type="bibr" rid="ref20">20</xref>
        ].
Much of the current research has focused on routing through relay nodes with a known given position
(see, e.g., [
        <xref ref-type="bibr" rid="ref5 ref52 ref54 ref8">5, 54, 8, 52</xref>
        ]), whereas our setting is different, in that we have to compute at the same time the
position of the relay nodes as well as the routing strategy for each relay node. Finally, differently from
other works, our solution also defines the orientation of the antennas hosted by each relay node.
6
      </p>
    </sec>
    <sec id="sec-6">
      <title>Conclusions</title>
      <p>
        In this short paper we introduced the problem of computing a deployment for relay nodes in a wireless
network that minimises the relay node network cost while at the same time guaranteeing proper working
of the network even when some of the relay nodes (up to a given maximum number) become faulty
(fault-tolerance). For such a problem, we surveyed our recent approach [
        <xref ref-type="bibr" rid="ref14 ref49">49, 14</xref>
        ] which, in a few minutes of
computation on a small parallel infrastructure, produces a 0/1-LP formulation of an optimisation problem
that can be straightforwardly given as input to different classes of standard AI solvers, in particular: MILP,
PB-SAT and SMT/OMT. Our experimental results using 8 among the state-of-the-art MILP, PB-SAT
and SMT/OMT solvers show that we can compute in a few hours (hence, within a fully acceptable time
given our application domain) an optimal placement of relay nodes in areas of up to 50 squared kilometres
(i.e., the area of a medium-large airport) with a precision of a few hundred metres.
      </p>
      <p>
        In future work we aim at experimenting with additional solving technologies like, e.g., Constraint
Programming (see, e.g., [
        <xref ref-type="bibr" rid="ref6">6</xref>
        ]), Constraint Answer Set Programming (see, e.g., [
        <xref ref-type="bibr" rid="ref53">53</xref>
        ]) as well as hybrid
(e.g., [
        <xref ref-type="bibr" rid="ref31">31</xref>
        ]) and decomposition-based approaches (e.g., [
        <xref ref-type="bibr" rid="ref56">56</xref>
        ]), also by exploiting our experience in other
mission-critical application domains, e.g., smart grids (see, e.g., [
        <xref ref-type="bibr" rid="ref40 ref50">40, 50</xref>
        ]) and network vulnerability analysis
[
        <xref ref-type="bibr" rid="ref48">48</xref>
        ]. Also, in order to further increase the size of the areas we can manage, we plan to approach our
problem with iterative improvement techniques like local search and meta-heuristic methods (see, e.g.,
[
        <xref ref-type="bibr" rid="ref21 ref63">21, 63</xref>
        ]) specially suited for large instances (e.g., [
        <xref ref-type="bibr" rid="ref39">39</xref>
        ]), of course sacrificing optimality guarantees. Finally,
we aim at reducing the need of linear constraint over-approximations by exploiting our simulation-based
approaches (e.g., [
        <xref ref-type="bibr" rid="ref36 ref41 ref46 ref62">62, 41, 46, 36</xref>
        ]) driven by intelligent search (e.g., [
        <xref ref-type="bibr" rid="ref12 ref42 ref44 ref45 ref47 ref59">42, 45, 44, 47, 12, 59</xref>
        ]).
Acknowledgements This work was partially supported by: Italian Ministry of University and Research
under grant “Dipartimenti di eccellenza 2018–2022” of the Department of Computer Science of Sapienza
University of Rome; INdAM “GNCS Project 2019”.
      </p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          [1] Pseudo-boolean competition
          <year>2005</year>
          ,
          <year>2005</year>
          . http://www.cril.
          <source>univ-artois.fr/PB05.</source>
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          <article-title>[2] GLPK (GNU linear programming kit</article-title>
          ),
          <year>2012</year>
          . http://www.gnu.org/software/glpk.
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          [3] Pseudo-boolean competition
          <year>2016</year>
          ,
          <year>2016</year>
          . http://www.cril.
          <source>univ-artois.fr/PB16.</source>
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          [4]
          <string-name>
            <given-names>C.</given-names>
            <surname>Alcaraz</surname>
          </string-name>
          and
          <string-name>
            <given-names>S.</given-names>
            <surname>Zeadally</surname>
          </string-name>
          .
          <article-title>Critical infrastructure protection: Requirements and challenges for the 21st century</article-title>
          .
          <source>Int J Crit Infr Prot</source>
          ,
          <volume>8</volume>
          ,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          [5]
          <string-name>
            <given-names>A.</given-names>
            <surname>Amis</surname>
          </string-name>
          , et al.
          <article-title>Max-Min D-cluster formation in wireless ad hoc networks</article-title>
          .
          <source>In IEEE INFOCOM 2000</source>
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          [6]
          <string-name>
            <given-names>K.</given-names>
            <surname>Apt</surname>
          </string-name>
          .
          <article-title>Principles of Constraint Programming</article-title>
          . Cambridge U.P.,
          <year>2003</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          [7]
          <string-name>
            <given-names>C.</given-names>
            <surname>Barrett</surname>
          </string-name>
          and
          <string-name>
            <given-names>C.</given-names>
            <surname>Tinelli</surname>
          </string-name>
          .
          <article-title>Satisfiability modulo theories</article-title>
          .
          <source>In Handbook of Model Checking</source>
          ,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          [8]
          <string-name>
            <given-names>E.</given-names>
            <surname>Biagioni</surname>
          </string-name>
          and
          <string-name>
            <given-names>G.</given-names>
            <surname>Sasaki</surname>
          </string-name>
          .
          <article-title>Wireless sensor placement for reliable and efficient data collection</article-title>
          .
          <source>In HICSS-36. IEEE</source>
          ,
          <year>2003</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          [9]
          <string-name>
            <given-names>A.</given-names>
            <surname>Biere</surname>
          </string-name>
          , et al., eds.
          <source>Handbook of Satisfiability</source>
          , vol.
          <volume>185</volume>
          .
          <string-name>
            <surname>IOS</surname>
          </string-name>
          ,
          <year>2009</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          [10]
          <string-name>
            <given-names>N.</given-names>
            <surname>Bjørner</surname>
          </string-name>
          , et al. νZ
          <article-title>- An optimizing SMT solver</article-title>
          .
          <source>In TACAS</source>
          <year>2015</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>9035</volume>
          . Springer,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          [11]
          <string-name>
            <given-names>L.</given-names>
            <surname>Bordeaux</surname>
          </string-name>
          , et al.
          <article-title>A unifying framework for structural properties of CSPs: Definitions, complexity, tractability</article-title>
          .
          <source>JAIR</source>
          ,
          <volume>32</volume>
          ,
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          [12]
          <string-name>
            <given-names>A.</given-names>
            <surname>Calabrese</surname>
          </string-name>
          , et al.
          <article-title>Generating T1DM virtual patients for in silico clinical trials via AI-guided statistical model checking</article-title>
          .
          <source>In RCRA</source>
          <year>2019</year>
          , CEUR W.P., vol.
          <volume>2538</volume>
          .
          <string-name>
            <surname>CEUR</surname>
          </string-name>
          ,
          <year>2019</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          [13]
          <string-name>
            <given-names>M.</given-names>
            <surname>Cardei</surname>
          </string-name>
          and
          <string-name>
            <given-names>D.</given-names>
            <surname>Du</surname>
          </string-name>
          .
          <article-title>Improving wireless sensor network lifetime through power aware organization</article-title>
          .
          <source>Wireless Netw</source>
          ,
          <volume>11</volume>
          (
          <issue>3</issue>
          ),
          <year>2005</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          [14]
          <string-name>
            <given-names>Q.</given-names>
            <surname>Chen</surname>
          </string-name>
          , et al.
          <article-title>MILP, pseudo-boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks</article-title>
          .
          <source>Fundam Inform</source>
          ,
          <year>2020</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          [15]
          <string-name>
            <given-names>M.</given-names>
            <surname>Conforti</surname>
          </string-name>
          , et al.
          <source>Integer Programming</source>
          . Springer,
          <year>2014</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          [16]
          <string-name>
            <given-names>A.</given-names>
            <surname>Davis</surname>
          </string-name>
          and
          <string-name>
            <given-names>H.</given-names>
            <surname>Chang</surname>
          </string-name>
          .
          <article-title>Airport protection using wireless sensor networks</article-title>
          .
          <source>In IEEE HST</source>
          <year>2012</year>
          . IEEE,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          [17] L. de Moura and
          <string-name>
            <given-names>N.</given-names>
            <surname>Bjørner</surname>
          </string-name>
          . Z3:
          <article-title>An efficient SMT solver</article-title>
          .
          <source>In TACAS</source>
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          [18]
          <string-name>
            <given-names>N.</given-names>
            <surname>Eén</surname>
          </string-name>
          and
          <string-name>
            <given-names>N.</given-names>
            <surname>Sörensson</surname>
          </string-name>
          .
          <article-title>An extensible SAT-solver</article-title>
          .
          <source>In SAT</source>
          <year>2003</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>2919</volume>
          . Springer,
          <year>2004</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          [19]
          <string-name>
            <given-names>N.</given-names>
            <surname>Eén</surname>
          </string-name>
          and
          <string-name>
            <given-names>N.</given-names>
            <surname>Sörensson</surname>
          </string-name>
          .
          <article-title>Translating pseudo-boolean constraints into SAT</article-title>
          .
          <source>JSAT</source>
          ,
          <volume>2</volume>
          ,
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref20">
        <mixed-citation>
          [20]
          <string-name>
            <given-names>D.</given-names>
            <surname>Ganesan</surname>
          </string-name>
          , et al.
          <article-title>Power-efficient sensor placement and transmission structure for data gathering under distortion constraints</article-title>
          .
          <source>ACM TOSN</source>
          ,
          <volume>2</volume>
          (
          <issue>2</issue>
          ),
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref21">
        <mixed-citation>
          [21]
          <string-name>
            <given-names>F.</given-names>
            <surname>Glover</surname>
          </string-name>
          and G. Kochenberger, eds.
          <source>Handbook of Metaheuristics</source>
          , vol.
          <volume>57</volume>
          . Springer,
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref22">
        <mixed-citation>
          [22]
          <string-name>
            <given-names>K.</given-names>
            <surname>Gopalakrishnan</surname>
          </string-name>
          , et al.
          <article-title>Cyber security for airports</article-title>
          .
          <source>Int J Traffic Transp Engin</source>
          ,
          <volume>3</volume>
          (
          <issue>4</issue>
          ),
          <year>2013</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref23">
        <mixed-citation>
          [23]
          <string-name>
            <given-names>G.</given-names>
            <surname>Gottlob</surname>
          </string-name>
          , et al.
          <article-title>Conditional constraint satisfaction: Logical foundations and complexity</article-title>
          .
          <source>In IJCAI 2007</source>
          .
          <year>2007</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref24">
        <mixed-citation>
          [24]
          <string-name>
            <given-names>Y.</given-names>
            <surname>Guo</surname>
          </string-name>
          and
          <string-name>
            <given-names>S.</given-names>
            <surname>Barton</surname>
          </string-name>
          . Fresnel Zone Antennas. Springer,
          <year>2002</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref25">
        <mixed-citation>
          [25]
          <string-name>
            <surname>Gurobi</surname>
            <given-names>optimizer</given-names>
          </string-name>
          ,
          <year>2018</year>
          . http://www.gurobi.com.
        </mixed-citation>
      </ref>
      <ref id="ref26">
        <mixed-citation>
          [26]
          <string-name>
            <given-names>A.</given-names>
            <surname>Hashim</surname>
          </string-name>
          , et al.
          <article-title>Optimal placement of relay nodes in wireless sensor network using artificial bee colony algorithm</article-title>
          .
          <source>J Netw Comp Appl</source>
          ,
          <volume>64</volume>
          ,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref27">
        <mixed-citation>
          <source>[27] IBM ILOG CPLEX Optimization Studio V12.8.0</source>
          ,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref28">
        <mixed-citation>
          [28]
          <string-name>
            <given-names>J.</given-names>
            <surname>Karlof</surname>
          </string-name>
          .
          <article-title>Integer programming: theory and practice</article-title>
          .
          <source>CRC</source>
          ,
          <year>2005</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref29">
        <mixed-citation>
          [29]
          <string-name>
            <given-names>Y.</given-names>
            <surname>Kim</surname>
          </string-name>
          , et al.
          <article-title>Resilient end-to-end message protection for large-scale cyber-physical system communications</article-title>
          .
          <source>In SmartGridComm</source>
          <year>2012</year>
          . IEEE,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref30">
        <mixed-citation>
          [30]
          <string-name>
            <given-names>A.</given-names>
            <surname>Krause</surname>
          </string-name>
          , et al.
          <article-title>Near-optimal sensor placements: Maximizing information while minimizing communication cost</article-title>
          .
          <source>In IPSN 2006. ACM</source>
          ,
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref31">
        <mixed-citation>
          [31]
          <string-name>
            <given-names>P.</given-names>
            <surname>Laborie</surname>
          </string-name>
          .
          <article-title>An update on the comparison of MIP, CP and hybrid approaches for mixed resource allocation and scheduling</article-title>
          .
          <source>In CPAIOR</source>
          <year>2018</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>10848</volume>
          . Springer,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref32">
        <mixed-citation>
          [32]
          <string-name>
            <given-names>D. Le</given-names>
            <surname>Berre</surname>
          </string-name>
          and
          <string-name>
            <given-names>A.</given-names>
            <surname>Parrain</surname>
          </string-name>
          .
          <article-title>The Sat4j library, release 2.2</article-title>
          . JSAT,
          <volume>7</volume>
          ,
          <year>2010</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref33">
        <mixed-citation>
          [33]
          <string-name>
            <given-names>Y.</given-names>
            <surname>Lee</surname>
          </string-name>
          , et al.
          <article-title>Optimization of AP placement and channel assignment in wireless LANs</article-title>
          .
          <source>In LCN</source>
          <year>2002</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref34">
        <mixed-citation>
          [34]
          <string-name>
            <given-names>J.</given-names>
            <surname>Li</surname>
          </string-name>
          , et al.
          <article-title>Capacity of ad hoc wireless networks</article-title>
          .
          <source>In MOBICOM 2001. ACM</source>
          ,
          <year>2001</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref35">
        <mixed-citation>
          [35]
          <string-name>
            <given-names>G.</given-names>
            <surname>Lykou</surname>
          </string-name>
          , et al.
          <article-title>Defending airports from UAS: A survey on cyber-attacks and counter-drone sensing technologies</article-title>
          .
          <source>Sensors</source>
          ,
          <volume>20</volume>
          (
          <issue>12</issue>
          ),
          <year>2020</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref36">
        <mixed-citation>
          [36]
          <string-name>
            <given-names>F.</given-names>
            <surname>Maggioli</surname>
          </string-name>
          , et al.
          <article-title>SBML2Modelica: Integrating biochemical models within open-standard simulation ecosystems</article-title>
          .
          <source>Bioinformatics</source>
          ,
          <volume>36</volume>
          (
          <issue>7</issue>
          ),
          <year>2020</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref37">
        <mixed-citation>
          [37]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          .
          <article-title>Now or Never: Negotiating efficiently with unknown or untrusted counterparts</article-title>
          .
          <source>Fundam Inform</source>
          ,
          <volume>149</volume>
          (
          <issue>1-2</issue>
          ),
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref38">
        <mixed-citation>
          [38]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Evaluating ASP and commercial solvers on the CSPLib</article-title>
          . Constraints,
          <volume>13</volume>
          (
          <issue>4</issue>
          ),
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref39">
        <mixed-citation>
          [39]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Combinatorial problem solving over relational databases: View synthesis through constraint-based local search</article-title>
          .
          <source>In SAC 2012. ACM</source>
          ,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref40">
        <mixed-citation>
          [40]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Demand-aware price policy synthesis and verification services for smart grids</article-title>
          .
          <source>In SmartGridComm</source>
          <year>2014</year>
          . IEEE,
          <year>2014</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref41">
        <mixed-citation>
          [41]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Computing biological model parameters by parallel statistical model checking</article-title>
          .
          <source>In IWBBIO</source>
          <year>2015</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>9044</volume>
          . Springer,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref42">
        <mixed-citation>
          [42]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>SyLVaaS: System level formal verification as a service</article-title>
          .
          <source>In PDP 2015. IEEE</source>
          ,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref43">
        <mixed-citation>
          [43]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>User flexibility aware price policy synthesis for smart grids</article-title>
          .
          <source>In DSD 2015. IEEE</source>
          ,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref44">
        <mixed-citation>
          [44]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Anytime system level verification via parallel random exhaustive hardware in the loop simulation</article-title>
          .
          <source>Microprocessors and Microsystems</source>
          ,
          <volume>41</volume>
          ,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref45">
        <mixed-citation>
          [45]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>SyLVaaS: System level formal verification as a service</article-title>
          .
          <source>Fundam Inform</source>
          ,
          <fpage>1</fpage>
          -
          <lpage>2</lpage>
          ,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref46">
        <mixed-citation>
          [46]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>On minimising the maximum expected verification time</article-title>
          .
          <source>Inf Proc Lett</source>
          ,
          <volume>122</volume>
          ,
          <year>2017</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref47">
        <mixed-citation>
          [47]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Computing personalised treatments through in silico clinical trials. A case study on downregulation in assisted reproduction</article-title>
          .
          <source>In RCRA</source>
          <year>2018</year>
          , CEUR W.P., vol.
          <volume>2271</volume>
          .
          <string-name>
            <surname>CEUR</surname>
          </string-name>
          ,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref48">
        <mixed-citation>
          [48]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>An efficient algorithm for network vulnerability analysis under malicious attacks</article-title>
          .
          <source>In ISMIS 2018</source>
          . Springer,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref49">
        <mixed-citation>
          [49]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Optimal fault-tolerant placement of relay nodes in a mission critical wireless network</article-title>
          .
          <source>In RCRA</source>
          <year>2018</year>
          , CEUR W.P., vol.
          <volume>2271</volume>
          .
          <string-name>
            <surname>CEUR</surname>
          </string-name>
          ,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref50">
        <mixed-citation>
          [50]
          <string-name>
            <given-names>T.</given-names>
            <surname>Mancini</surname>
          </string-name>
          , et al.
          <article-title>Parallel statistical model checking for safety verification in smart grids</article-title>
          .
          <source>In SmartGridComm</source>
          <year>2018</year>
          . IEEE,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref51">
        <mixed-citation>
          [51]
          <string-name>
            <given-names>J.</given-names>
            <surname>Marques-Silva</surname>
          </string-name>
          and
          <string-name>
            <given-names>S.</given-names>
            <surname>Malik</surname>
          </string-name>
          .
          <article-title>Propositional SAT solving</article-title>
          .
          <source>In Handbook of Model Checking</source>
          ,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref52">
        <mixed-citation>
          [52]
          <string-name>
            <given-names>S.</given-names>
            <surname>Meguerdichian</surname>
          </string-name>
          , et al.
          <article-title>Coverage problems in wireless ad-hoc sensor networks</article-title>
          .
          <source>In IEEE INFOCOM</source>
          <year>2001</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref53">
        <mixed-citation>
          [53]
          <string-name>
            <given-names>V.</given-names>
            <surname>Mellarkod</surname>
          </string-name>
          , et al.
          <article-title>Integrating answer set programming and constraint logic programming</article-title>
          .
          <source>Ann Math Artif Intell</source>
          ,
          <volume>53</volume>
          (
          <issue>1-4</issue>
          ),
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref54">
        <mixed-citation>
          [54]
          <string-name>
            <given-names>R.</given-names>
            <surname>Prasad</surname>
          </string-name>
          and
          <string-name>
            <given-names>H.</given-names>
            <surname>Wu</surname>
          </string-name>
          .
          <article-title>Gateway deployment optimization in cellular Wi-Fi mesh networks</article-title>
          .
          <source>J Netw</source>
          ,
          <volume>1</volume>
          (
          <issue>3</issue>
          ),
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref55">
        <mixed-citation>
          [55]
          <string-name>
            <given-names>L.</given-names>
            <surname>Qiu</surname>
          </string-name>
          , et al.
          <article-title>Optimizing the placement of integration points in multi-hop wireless networks</article-title>
          .
          <source>In ICNP 2004</source>
          , vol.
          <volume>4</volume>
          . IEEE,
          <year>2004</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref56">
        <mixed-citation>
          [56]
          <string-name>
            <given-names>R.</given-names>
            <surname>Rahmaniani</surname>
          </string-name>
          , et al.
          <article-title>The Benders decomposition algorithm: A literature review</article-title>
          .
          <source>Eur J Op Res</source>
          ,
          <volume>259</volume>
          (
          <issue>3</issue>
          ),
          <year>2017</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref57">
        <mixed-citation>
          [57]
          <string-name>
            <given-names>M.</given-names>
            <surname>Sakai</surname>
          </string-name>
          and
          <string-name>
            <given-names>H.</given-names>
            <surname>Nabeshima</surname>
          </string-name>
          .
          <article-title>Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers</article-title>
          .
          <source>IEICE Trans Inf Syst</source>
          ,
          <fpage>E98</fpage>
          -D, No.
          <volume>6</volume>
          ,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref58">
        <mixed-citation>
          [58]
          <string-name>
            <given-names>R.</given-names>
            <surname>Sebastiani</surname>
          </string-name>
          and
          <string-name>
            <given-names>P.</given-names>
            <surname>Trentin. OptiMathSAT</surname>
          </string-name>
          :
          <article-title>A tool for Optimization Modulo Theories</article-title>
          . JSAT,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref59">
        <mixed-citation>
          [59]
          <string-name>
            <given-names>S.</given-names>
            <surname>Sinisi</surname>
          </string-name>
          , et al.
          <article-title>Optimal personalised treatment computation through in silico clinical trials on patient digital twins</article-title>
          .
          <source>Fundam Inform</source>
          ,
          <year>2020</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref60">
        <mixed-citation>
          [60]
          <string-name>
            <given-names>O. N.</given-names>
            <surname>Skrypnik</surname>
          </string-name>
          .
          <source>Radio Navigation Systems for Airports and Airways</source>
          . Springer,
          <year>2019</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref61">
        <mixed-citation>
          [61]
          <string-name>
            <given-names>D.</given-names>
            <surname>Stacey</surname>
          </string-name>
          .
          <source>Aeronautical Radio Communication Systems and Networks</source>
          . Wiley,
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref62">
        <mixed-citation>
          [62]
          <string-name>
            <given-names>E.</given-names>
            <surname>Tronci</surname>
          </string-name>
          , et al.
          <article-title>Patient-specific models from inter-patient biological models and clinical records</article-title>
          .
          <source>In FMCAD 2014. IEEE</source>
          ,
          <year>2014</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref63">
        <mixed-citation>
          [63]
          <string-name>
            <given-names>P.</given-names>
            <surname>Van Hentenryck</surname>
          </string-name>
          and
          <string-name>
            <given-names>L.</given-names>
            <surname>Michel</surname>
          </string-name>
          .
          <article-title>Constraint-Based Local Search</article-title>
          . MIT,
          <year>2009</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref64">
        <mixed-citation>
          [64]
          <string-name>
            <given-names>M.</given-names>
            <surname>Younis</surname>
          </string-name>
          and
          <string-name>
            <given-names>K.</given-names>
            <surname>Akkaya</surname>
          </string-name>
          .
          <article-title>Strategies and techniques for node placement in wireless sensor networks: A survey</article-title>
          .
          <source>Ad Hoc Netw</source>
          ,
          <volume>6</volume>
          (
          <issue>4</issue>
          ),
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>