Solving the Identifying Code Set Problem with Grouped Independent Support

1 Introduction

Imagine that you are in charge of ensuring the fire-safety of a hotel. Your smoke detectors can sense a fire in the room in which they are placed immediately, and sense a fire in an adjacent room with a time delay. You realise that this means that you can detect every fire, even if you do not place a detector in every room. When you tell the hotel manager, they ask you to minimise the number of smoke detectors that you place. Additionally, they tell you to make sure that, even if as many as five fires break out in different rooms at the same time, you can uniquely identify these multiple rooms based on the set of smoke detectors that detect smoke. How many detectors do you need, and where do you place them?

The above situation is an example of a sensor placement problem. This well-studied problem has applications ranging from satellite deployment [Sen et al., 2019], to power grid monitoring [Padhee et al., 2020], to identifying criminals [Basu and Sen, 2021b] or spreaders of misinformation [Basu and Sen, 2021a], and is typically formulated on graphs. In the example above, nodes represent the hotel rooms, with edges between adjacent rooms.

Graphs are fundamental tools for modelling the interaction between objects. For many real-world computational problems, a node in a graph represents a resource object and an edge between two nodes models the ability for the corresponding objects to communicate. Resource objects are often abstractions of critical objects such as satellites, informants in crime networks, or servers. The critical nature of these objects necessitates reliable failure detection. For this, we often rely on sensors, placed strategically on certain nodes.

In this paper, we study a generalised version of the identifying code set (ICS) [Karpovsky et al., 1998] problem. In our version, a sensor placed in a node detects a failure that occurs in that node immediately, and detects failures in neighbouring nodes with a small time delay. A generalised identifying code set (GICS) is a set of nodes in which we must place a sensor such that any set of at most k simultaneous failures can be uniquely identified by the placed sensors. Conceptually, a GICS is a dominating set (i.e., a set of nodes such that each node is either in that set or is a neighbour of a node in that set) in an undirected graph, such that each subset of nodes with cardinality at most k can be uniquely identified by the sensors placed on the nodes this dominating set.

Existing methods for finding and minimising GICSes with one failure at a time, employ an integer-linear programming (ILP) encoding [Padhee et al., 2020; Basu and Sen, 2021a; Basu and Sen, 2021b]. A straightforward generalisation of this ILP formulation to support multiple simultaneous failures scales poorly with network size and the number of simultaneous failures. This explosion of the model size limits the applicability of ILP-based methods to small networks and support for only one node failure at a time.

The primary contribution of this work is a novel computational technique for solving GICS problems, with a much more compact encoding. Specifically, we propose the concept of grouped independent support (GIS) (an extension of independent support [Chakraborty et al., 2014b; Ivrii et al., 2016; Soos and Meel, 2022; Yang et al., 2022]), and show how we can reduce the problem of finding a GICS to the problem of finding a GIS. We then propose a new algorithm, called gismo, to compute a GIS.

The main benefit of this approach is that the more compact encoding enables us to solve GICS problems on much larger networks than the networks that can be solved by the state of the art. Indeed, our empirical analysis demonstrates that gismo is able to handle networks of up to 21363 nodes, while the ILP-based approach could not handle networks beyond 494 nodes, thus representing a ∼ 40× improvement in terms of the size of the networks. Furthermore, depending on the number of simultaneous failures, the instances that can be encoded by both methods are solved up to 520× faster by the GIS-based approach than by the ILP-based method. For the majority of those instances, the cardinality of the result returned by gismo was at most 10% larger than the cardinality returned by the ILP-based method.

A conceptual contribution is to expand the usefulness of the notion of independent support. The computation of independent supports has, to the best of our knowledge, so far only been used as a preprocessing step for model counting and uniform sampling [Chakraborty et al., 2014b; Ivrii et al., 2016; Lagniez et al., 2016; Lagniez et al., 2020; Yang et al., 2022; Soos and Meel, 2022]. We are the first to use the independent support for modelling and solving an NP-hard problem directly.

The remainder of this paper is organised as follows. We briefly discuss notation and provide relevant definitions in Section 2, where we also provide a motivating example of a GICS problem. Then, we describe the current state of the art for solving GICS problems in Section 3. Section 4 describes GIS, the reduction from the GICS problem to the GIS problem, and gismo. We present an experimental evaluation of our implementation of gismo on a variety of networks in Section 5, and conclude in Section 6.

2 Preliminaries

We briefly introduce our notation, recall relevant concepts, and define the generalised identifying code set (GICS).

2.1 Definitions and Notation

Graphs. We consider an undirected, loop-free graph Γ = (V,E) on nodes V and edges E. We denote nodes with lower case letters u, v,w ∈ V . The distance between two nodes u and v is the number of edges on the shortest path between them, and is denoted by d(u, v). If d(u, v) = 1, we call the nodes u and v direct neighbours of each other. The neighbourhood function Nd(v) returns the set of nodes that are at a distance d from node v. We define the closed d-neighbourhood of a node v as N + d (v) = Nd(v) ∪ {v}. For a set of nodes U, we define the neighbourhood function Nd(U) = ⋃u∈U Nd(u), and define the closed neighbourhood of U, N + d (U), analogously.

Boolean satisfiability. We denote a set of Boolean variables with the capital letter X and denote individual Boolean variables with lowercase letters x, y, z ∈ X. We denote truth values with 1 (true) and 0 (false). A literal l is a variable (e.g., x) or its negation (e.g., ¬x). A disjunction of literals is called a clause. We say that a formula F is in conjunctive normal form (CNF) if it is a conjunction of clauses. A full assignment σ : X ↦→ {0, 1} assigns a truth value to each variable in X. We use σ(x) to denote the truth value that σ assigns to variable x. Given a subset Y ⊆ X, σ↓Y : Y ↦→ {0, 1} denotes the assignment projected onto Y , thus specifying the truth values that the variables in Y get under σ. Given a Boolean formula F(X), we call an assignment σ a solution or model of F(X) if F({x ↦→ σ(x) | x ∈ X}) |= 1. We denote the set of all models of F with Sol(F). Similarly, we denote the set of all models of F(X) projected on the subset Y ⊆ X as Sol↓Y (F). We call the variables X that appear in F the support of F. If a Boolean formula has at least one solution, we say that it is satisfiable. Otherwise, we call it unsatisfiable.

Minimality. Let T be a set of items, and let S ⊆ T be a subset. Given a set C of constraints on sets, we call S setminimal w.r.t. C if S satisfies all constraints in C and there exists no proper subset of S that also satisfies all those constraints. We call S a cardinality-minimal set if S is minimal, and there exists no S′ ⊆ T that is also minimal, but whose cardinality is strictly smaller than that of S.

Support of a set. We use calligraphic uppercase symbols to denote sets of sets of variables. We define the support of a set of sets of variables S as follows: sup (S) := ⋃Si∈S Si.

Signatures. Given an undirected, loop-free graph Γ := (V,E) with nodes V and edges E, and given a subset of nodes D ⊆ V . We define the signature of U ⊆ V as the following tuple: sU := 〈S0U , S1U 〉, where S0U := U ∩D and S1U := N + 1 (U) ∩D.

Generalised Identifying Code Set (GICS). Given a graph Γ := (V, E), a positive integer k ≤ |V | and D ⊆ V . We call D a generalised identifying code set (GICS) of Γ and k if, for all U,W ⊆ V with |U| ≤ k, |W| ≤ k and U ̸= W, it holds that sU ̸= sW. Hence, if D is a GICS of Γ and k, then the signatures of all subsets of V with cardinality at most k are unique. We call k the maximum identifiable set size.

The GICS problem. Given a Γ := (V,E) and k, the GICS problem asks to find a D ⊆ V such that D is a GICS of Γ and k, and |D| is minimised.

Independent Support. Given a Boolean formula F(X) and a set I ⊆ X, we call I an independent support [Chakraborty et al., 2014b] of F iff, for two solutions σ1 and σ2, the following holds: (σ1↓I = σ2↓I) ⇒ (σ1↓X = σ2↓X).

The concept of independent support was introduced in 2014 [Chakraborty et al., 2014a], born from the observation that the truth values assigned to variables in solutions to a formula, can often be defined by the truth values of other variables. Hence, this property is referred to in the literature as definability [Lagniez et al., 2016; Soos and Meel, 2022]. Tools for computing minimal independent supports include Arjun [Soos and Meel, 2022] and B+E [Lagniez et al., 2016; Lagniez et al., 2020].

Until now, independent supports have only been computed as a preprocessing step for counting and sampling [Chakraborty et al., 2014a; Lagniez et al., 2016; Lagniez et al., 2020; Chakraborty et al., 2014b; Ivrii et al., 2016; Soos and Meel, 2022; Yang et al., 2022]. In Section 4, we present a generalisation of the independent support of a Boolean formula, and show how we can use that to find solutions to the GICS problem. To the best of our knowledge, we are the first to lift computing independent supports out of the preprocessing domain, turning it into a tool for modelling and solving NP-hard problems directly.

Padoa's Theorem. Let F(Z,A) be a Boolean formula on Boolean variables Z ∪ A, with Z ∩ A = ∅. We can use Padoa's theorem [Padoa, 1901] to check if a variable z ∈ Z is defined by the other variables in Z. Let ˆ Z be a fresh set of variables, such that ˆ Z := {ˆ zi | zi ∈ Z}, and let F (Z ↦→ ˆ Z,A) be the formula in which every zi ∈ Z is replaced by its corresponding ˆ zi ∈ ˆ Z. We assume w.l.o.g. that Z := {z1, . . . , zm}, with m = |Z|. For 1 ≤ i ≤ m, Padoa's theorem now defines the following formula:

Intuitively, this formula asks if there exist at least two solutions to F(Z,A), σ1 and σ2, such that σ1↓Z and σ2↓Z differ only in their value for zi. If yes, then Eq. (1) is satisfiable. If no, then Eq. (1) is unsatisfiable.

2.2 Motivating Example

We model the sensor placement example from Section 1 as follows. First, we model the hotel as a graph Γ := (V,E), where the nodes V represent rooms and two nodes u, v are connected by an edge (u, v) if the corresponding rooms are adjacent. Smoke detectors have a green light if they do not detect smoke, and have a red light if they do. All smoke detectors have a green light at t0 -1. We assume that at time t0 a fire can break out in at most k different rooms (k = 5 in the example in Section 1), and that after t0, no more fires break out. If there is a smoke detector placed in room v, and a fire breaks out in room v at time t0, the smoke detector in room v detects the smoke at t0, whereupon its detection light turns from green to red immediately, and remains red. A smoke detector placed in room u ∈ N1(v) detects the smoke from the fire in room v at t1 = t0 + 1. If its light was not yet red at time t0, the light of the sensor in room u turns from green to red at time t1. Hence, at time t1 a sensor placed in room v ∈ V is red iff there is a fire in at least one room in N + 1 (v).

For a set of rooms U ⊆ V , we now have sU = 〈S0U , S1U 〉, where S0U represents the set of detectors whose lights turn red at t0 if fires break out in all rooms in U at t0, while S1U represents the set of detectors whose lights are red at t1 = t0 +1. The GICS problem asks in which set of nodes D ⊆ V to place a smoke detector, such that D is a GICS of Γ and k, and |D| is minimised.

Example 1. Figure 1 shows an example of five rooms, where we have chosen k = 1. We show a GICS for this example that places a sensor in rooms a and c, i.e., D := {a, c}. The table shows the signature for each subset U ⊆ V with |U| ≤ 1. Note that each signature is unique, each non-empty subset has a non-empty signature, and that neither a nor c can be removed from D without destroying these two properties. This particular GICS has cardinality 2, which is the smallest possible cardinality for this network with k = 1.

3 RelatedWork

Several methods have been proposed for solving a variant of the identifying code set problem that only considers a maximum identifiable set size of k = 1, and only requires the S1U s to be unique. A common approach [Sen et al., 2019; Padhee et al., 2020; Basu and Sen, 2021a; Basu and Sen, 2021b] models the problem as an integer-linear program (ILP), to be solved with a mixed-integer programming (MIP) solver. We adapted the method from [Padhee et al., 2020; Basu and Sen, 2021b] such that it can model the unique identification of k > 1 simultaneous events. The number of linear constraints in this encoding grows as O ((|V | k )2), which is prohibitively large for all but the smallest of networks, especially if k > 1. We refer the reader to the extended version of this paper for the details on this ILP encoding and its size.

4 Approach

In this section, we discuss our novel approach to solving the GICS problem, which uses an encoding whose size does not explode, but rather grows polynomially with the problem size and k. We first introduce the grouped independent support (GIS), an extension of independent support [Chakraborty et al., 2014a; Ivrii et al., 2016], then show how we can reduce finding a GICS to finding a GIS, and finally propose an algorithm for finding a GIS of minimised cardinality: gismo.

4.1 Grouped Independent Support (GIS)

We define grouped independent support (GIS) as follows:

Definition 1. Given a formula F(Z,A), with Z ∩ A = ∅ and a partitioning G of Z into non-empty sets, such that sup (G) = Z. The subset I ⊆ G is a grouped independent support of ⟨F(Z,A), G⟩ if the following holds:

Intuitively, this means that if all solutions projected on to Z = sup (G) are unique, then all solutions projected onto sup (I) ⊆ sup (G) are unique, and vice versa. The '→' in Eq. (2) means that, for all solutions to F(Z,A), the truth values of the variables in sup (G) \ sup (I) are defined by the truth values of the variables in sup (I). Note that GIS is a generalisation of independent support, since finding an independent support corresponds to finding a GIS where all the groups have cardinality 1.

Observe that the problem of checking whether a given set I is a grouped independent support is in co-NP. In contrast, checking whether an assignment satisfies ILP constraints is in polynomial time. Therefore, a priori, it is natural to wonder if it is worth reducing GICS to a (potentially) computationally harder problem. We pursue such a reduction in the hope that the reduction may come at the gain of smaller problem encodings. In the remainder of this section, we show that such a gain is indeed possible.

4.2 AReduction fromGICS to GIS

We now present a reduction from finding a GICS to finding a GIS, using the example problem from Section 2.2. Let X := {xv | v ∈ V } and Y := {yv | v ∈ V } be sets of Boolean variables such that xv = 1 and yv = 1 iff a sensor placed in room v has a red light at time t0 and t1, respectively. We capture this in the following Boolean formula:

Additionally, we must require that at most k fires break out at the same time, which we do with the following formula (recall that if a fire breaks out at time t0 in room v, the light of a sensor placed in room v turns red at t0):

Converting these constraints to CNF and conjoining them, we obtain the following formula in CNF:

where A is a (possibly empty) set of auxiliary variables needed for the CNF encoding of the cardinality constraint. Additionally, we define one group for each node in the network: G := {Gv := {xv, yv} | v ∈ V }.

Now, we can find a GICS by encoding the problem into CNF according to Eq. (5), finding a GIS, and then extracting the sensor set as: D := {v | Gv ∈ I}.

Lemma 1. Given a loop-free, undirected network Γ := (V, E) on nodes V and edges E, a maximum identifiable set size 0 < k ≤ |V |, and given a GIS of Eq. (5) I ⊆ G with groups G := {Gv := {xv, yv}}. The set D := {v ∈ V | Gv ∈ I} is a GICS of Γ.

We prove this lemma in the extended version, by proving that there is a bijective relationship between the elements of the set of signatures of all U ⊆ V with |U| ≤ k and the set of projected solutions Sol↓sup(I) (Fk). Intuitively, we show that the highlighted columns in Table 1 encode the signatures in the table in Fig. 1, and vice versa. Each solution to Fk in Eq. (5) corresponds to selecting a set U ⊆ V with |U| ≤ k as the set of nodes with failures. By Definition 1, σU↓sup(I) ̸= σW↓sup(I) for sets U,W ∈ V with |U|, |W| ≤ k. Therefore, a GIS I guarantees unique signatures for all such U,W. Hence, the uniqueness requirement is implicitly required by the semantics of GIS, and we do not need to encode it explicitly.

We can prove the following lemma by simple analysis of Eq. (5) and techniques for encoding cardinality constraints into CNF [Sinz, 2005; Philipp and Steinke, 2015], and refer the reader to the extended version of this paper for that proof:

The above lemma highlights the potential exponential gains in encoding from GIS-based approach. While the ILP-based approach would lead to encodings with O ((|V | k )2) constraints, our GIS-based approach requires only O (k · |V | + |E|) clauses.

4.3 Finding a GIS with gismo

Algorithm 1 shows our algorithm for finding a GIS. On a high level, the algorithm iterates over all groups of variables and uses Padoa's theorem to determine if at least one of the variables in each variable group is not defined by other variables outside the group. If this is the case, the group must be part of a GIS. We now describe gismo in more detail.

Recall Padoa's theorem from Section 2.1. By choosing Z := sup (G) = X ∪ Y , we can define ψ for Eq. (5). If, for an 1 ≤ i ≤ m, ψ (Z,A, ˆ Z, zi) is unsatisfiable, then we know the following: if a partial assignment σ↓Z\{zi} can be extended to σ↓Z, then there is only one possible value that zi can take in σ↓Z such that σ is a model of Eq. (5). Hence, if ψ is unsatisfiable, then for each σ, the truth value of zi is defined by the truth values of the variables Z \ {zi}.

In Algorithm 1, we use Padoa's theorem as follows. We introduce a fresh set of indicator variables E = {ei | zi ∈ Z} (Line 1), and define the following formula (Line 2):

In Line 3, we introduce Q, the set of candidate variables that could be in the support of the GIS I that is returned by gismo. We initialise I with ∅.

Algorithm 1 The gismo algorithm.

Input: Formula F(Z,A) with partitioning of Z into G, a time limit τ.

Output: GIS I ⊆ G.

The 'for'-loop that starts at Line 5 in Algorithm 1 iterates over the groups in partition G. In each iteration, we define the set C, which contains the variables for which we want to check if they define the variables in the group G that is considered in that iteration. By design, the set C ∪ G is an independent support of F(Z,A). In the 'for'-loop that starts at Line 9, we test for each variable z ∈ G if that variable is defined by the variables in C, and thus if C is an independent support. If z is not defined by the variables in C (and hence ψ is satisfiable), we know that, given the current C, z is needed to define all solutions, and thus that C is not an independent support of F(Z,A). Hence, we add z's entire group to the GIS I (in Line 13). If all variables in G are defined by the variables in C, then C is an independent support and none of the variables in G are needed to define all solutions, so G is not added to I, and not considered again.

At the start of each iteration of the outer 'for'-loop, Q ∪ sup (I) is a set of variables that define the variables in Z \ (Q∪ sup (I)). During the execution of the algorithm, more and more groups of variables are removed from Q, and some groups are added to I, if that is deemed necessary for Q ∪ sup (I) to still define the variables in Z \ (Q ∪ sup (I)). At the end of the algorithm, Q is empty, and hence all groups in I contain variables that are necessary for defining the variables in Z \ sup (I). Hence, the I returned by the algorithm is a GIS for ⟨F(Z,A), G⟩. Recall that D is a GICS, and that in our reduction, each group corresponds to a node. Therefore, intuitively, gismo starts with D = V , and then removes nodes from D until no nodes can be removed without removing the GICS-ness of D.

The time limit τ in Line 12 is given in a maximum number of conflicts that the SAT solver may encounter before giving up. If the SAT solver reaches τ before it determines the (un)satisfiability of ψ, then ψ is treated as satisfiable. Hence, in practice it may happen that G is defined by the variables in C, but is nevertheless added to I.

We refer the reader to the extended version of this paper for the proof of the following lemma:

Lemma 3. Given an input formula F(Z, A) with group partitioning G such that sup (G) = Z, Algorithm 1 returns a GIS I of ⟨F(Z,A), G⟩.

If the call to CHECKSAT(ψ, τ ) never times out, gismo returns a set-minimal GIS of the input formula and partition. The cardinality of that GIS is potentially larger than the cardinality-minimal solution that is guaranteed by the ILP encoding proposed by [Padhee et al., 2020].

Note the similarity of gismo to the algorithm for high-level minimal unsatisfiable core extraction presented in [Nadel, 2010]. Indeed, finding a set-minimal independent support can be reduced to finding a group-oriented (or high-level) minimal unsatisfiable subset [Ivrii et al., 2016].

We illustrate gismo with an example, based on the problem in Example 1. To aid our discussion, we provide a truth table containing all solutions to Eq. (5) for the problem in Example 1, in Table 1.

Example 2. Let X := {xa, . . . , xe}, Y := {ya, . . . , ye}, and G := {Ga := {xa, ya}, . . . , Ge := {xe, ye}}. Let k = 1, and let F1(Z, A) be defined as in Eq. (5), with Z = sup (G).

After initialisation, Q = sup (G) and I = ∅. Let us assume that the algorithm now selects group Ge as the first group to test. This causes both Q and C to be updated to {xa, ya, . . . , xd, yd}, and ξ := exa ∧ eya ∧ . . . ∧ exd ∧ eyd . Let us assume that the algorithm first tests ye ∈ Ge for definability, constructing ψ := ϕ ∧ ξ ∧ ye ∧ ¬ˆ ye and checking for satisfiability. We inspect Table 1 to check if ψ is satisfiable. As we can see in the table, there are no two rows that agree on the truth values of variables {xa, ya, . . . , xd, yd}, but differ in their truth values of variable ye. Hence, ψ is unsatisfiable, and the algorithm moves to the second iteration of the inner 'for'-loop to perform the same test for variable xe, finding again that ψ is unsatisfiable.

The algorithm concludes that all variables in Ge are defined by the variables in C, and moves on to test the next group. Let us assume that the algorithm tests group Gd next. It finds that Gd also does not belong in the GIS, and moves on to group Gc. Now we have Q = C := {xa, ya, xb, yb}, ξ := exa ∧ eya ∧ exb ∧ eyb , and ψ := ϕ ∧ ξ ∧ yc ∧ ¬ˆ yc.

Let us assume that the algorithm first checks yc ∈ Gc. Inspecting Table 1, we find that there are no two rows that agree on their truth values for xa, ya, xb and yb, but disagree on their truth value for yc. Hence, ψ is unsatisfiable, and the algorithm moves on to test xc.

The rows {c} and {e} in Table 1 agree on their truth values for xa, ya, xb and yb, but disagree on their value for xc. Consequently, ψ is satisfiable, and we update I := {Gc}.

Let us assume that in the next iteration, the algorithm checks group Gb. It finds that, for both xb and yb, ψ is unsatisfiable, so Gb is discarded and not added to the GIS. In the final iteration, we have Q := ∅, C := {xc, yc} and ξ := exc ∧ eyc . It is easy to see from Table 1 that ψ := ϕ∧ξ∧xa∧¬ˆxa is satisfiable (inspect rows {b} and {e}), and thus the algorithm updates and returns I := {Ga, Gc}.

5 Experiments

In this section we describe our experiments aimed at evaluating the performance of gismo, comparing it to the state-ofthe-art ILP-based method.

5.1 Experimental Setup

Solving methods. We evaluate a method that encodes the problem into the CNF in Eq. (5) and then solves it by finding a GIS with gismo. In this section, we refer to this method as 'gismo'. We compare the performance of gismo to an ILPbased approach, as discussed in Section 3. We use pbpbs, based on initials of authors [Padhee et al., 2020], to refer to the ILP-based approach. We refer the reader to the extended version of this paper for details on implementation.

Software. Our implementation of gismo uses SAT solver CryptoMiniSat [Soos et al., 2009] version 5.11.7 (the latest version, last updated in December 2022) to determine the satisfiability of ψ in Line 12 in Algorithm 1. We implemented the scripts for encoding networks into CNF (Eq. (5)) or ILP (Section 3) with Python 3.5, using PBLib [Philipp and Steinke, 2015] for the CNF encoding of the cardinality constraint. We solved the ILPs with CPLEX 12.8.0.0. 1

Hardware. We ran our experiments on a high-performance cluster, where each node is equipped with two Intel E5-2690 v3 CPUs, each with 12 cores and 96 GB RAM, running at 2.60 GHz, under Red Hat Enterprise Linux Server 6.10.

Experimental parameters. We allow gismo and pbpbs each one core, 3600 CPU s and 4 GB RAM to encode and solve each (network, k) combination. For gismo we set a time limit of τ = 5000 conflicts for the call to CryptoMiniSat in Line 12. For CPLEX we use the default settings. The running times we report are all user time measured in CPU s.

Problem instances. Our benchmark set comprises 50 undirected networks obtained from the Network Repository [Rossi and Ahmed, 2015] and from the IdentifyingCodes GitHub repository [Basu and Sen, 2021b]. 2 , including grid-like networks, such as road networks and power networks, and social networks, such as collaboration networks and crime networks. Their sizes vary from 10 to 1 087 562 nodes and 14 to 1 541 514 edges, and their median degrees vary from 1 to 78.

1 Available at www.ibm.com/analytics/cplex-optimizer.

2 Available at https://networkrepository.com and https://github. com/kaustav-basu/IdentifyingCodes.

5.2 Research Questions

The experiments in this section are aimed at answering the following main research questions:

• Q1 How many instances are solved by pbpbs and gismo?
• Q2 How do the solving times of pbpbs and gismo scale with k and |V |?
• Q3 How does the number of clause in the CNF encoding scale with k and |V |?
• Q4 How do the cardinalities of the solutions returned by pbpbs and gismo compare?

In summary, we find that gismo solves nearly 10× more problem instances than pbpbs within the time limit of 3600 seconds per problem instance. The instances that can be encoded by both methods are solved up to 520× faster by gismo than by pbpbs, depending on k. On these instances, we find that the solution returned by gismo is at most 60% larger than that returned by pbpbs, but that most instances, the cardinality of the solution returned by gismo is less than 10% larger. We find that the size of the CNF in Eq. (5) scales polynomially with |V | and k. The largest problem that could be encoded and solved by pbpbs has 494 nodes. The largest problem that could be encoded and solved by gismo has 21363 nodes; a ∼ 40-fold improvement.

5.3 Experimental Results

In the remainder of this section, we describe our experimental results and answer our research questions.

Q1: Number of solved instances. We report the number of solved instances by gismo and pbpbs for the 9 tested values of k in Table 2. An instance is solved if the solving method terminates before the timeout time. In the case of pbpbs, this means that the returned solution is cardinalityminimal. In the case of gismo, this means that the solution is (close to) 3 set-minimal. Overall, gismo solved 289 of the 450 problem instances, while pbpbs solved only 36 out of 450. Hence, the gismo solves over 8 times as many problem instances as pbpbs. We now delve into the internals of gismo and pbpbs: gismo was able to encode the GICS problem into CNF (Eq. (5)) for each value of k for 49 of the 50 networks. The largest network it could encode into CNF has 227320 nodes and 814134 edges. We find that gismo returned a GIS for most of these CNFs. On the other hand, pbpbs was able to encode at most 11 of the 50 benchmarks into an ILP, which was for k = 1 (it performed worse as k increased). The largest network that it could encode has 494 nodes and 1080 edges. For larger values of k, pbpbs's ability to encode the networks drops rapidly, being only able to encode and solve 2 out of the 50 networks for k ≥ 4. These two networks are the smallest in our benchmark set, with only 10 an 14 nodes.

Q2: Solving time. Table 2 compares the PAR-2 scores 4 of gismo to those of pbpbs. The gismo method is up to ∼ 6

3 Because of the time limit τ in Line 12 of Algorithm 1.

4 The PAR-2 score is a penalised average runtime. It assigns a runtime of two times the time limit for each benchmark the tool timed out on, or ran out of memory on.

|V |

Figure 2: Number of clauses in the CNF encoding as a function of the number of nodes in the input network.

times faster than pbpbs, in terms of PAR-2 scores, for smaller values of k and 2× faster for larger values of k. Since pbpbs often times out during encoding phase (due to the blow-up of the size of the encoded formula), we also a provide comparison, in Table 3, for the instances for which the encoding phase of pbpbs did not time out and for which the underlying ILP solver did not timeout either, which was the case for all instances for which the encoding did not time out. It is worth remarking that all such instances were solved by gismo as well. Here, we find that gismo is up to 593.18/1.14 ≈ 520× faster than pbpbs in terms of median solving time. Overall, our results that gismo achieves significant performance improvements over pbpbs, in terms of running time.

Q3: Model size. Figure 2 shows that the number of clauses in the CNF encoding scales polynomially with the number of variables in the instance. The oscillations in the plot can be explained by the |E|-contribution to the CNF size (Lemma 2). Our benchmark set contains both social networks (with high median degrees) and grid-like networks (with low median degrees), and hence with different densities. Figure 3 shows typical examples of how the number of clauses in the CNF encoding grows with increasing k.

Q4: Solution quality. We compared the quality of solutions returned by pbpbs and gismo over the 36 instances that pbpbs could solve. In particular, we computed the ratio r := |I|/|DILP |, wherein I is the set computed by gismo, while DILP is the set computed by pbpbs. In our experiments, we found that 1 ≤ r ≤ 1.6, but for the majority of instances we found r < 1.1. Furthermore, 4 out of 36 instances had a ratio r = 1. Hence, even in our naive implementation, the cardinalities of our solutions are almost as good as the minimum cardinality guaranteed by pbpbs.

6 Conclusion

In this paper, we focused on the problem of generalised identifying code set (GICS) problem which, given an input network, aims to find a set of nodes in which to place sensors in order to uniquely detect node failures, and where the number of placed sensors must be minimised. We first identified the primary bottleneck of the prior state-of-the-art approach based on an ILP encoding: the blowup in the encoding size. To address this shortcoming, we introduced grouped independent support (GIS) and reduced the GICS problem to the problem of finding a GIS of a Boolean formula. Relying on the fact that algorithms for finding a minimised independent support are fast in practice, we designed and implemented an algorithm, gismo, that finds a minimised, though not necessarily cardinality-minimal, grouped independent support. Our empirical evaluation demonstrates that gismo achieves significant performance improvements over the prior state-ofthe-art technique in terms of running time, while producing solutions that tend to be close to cardinality-minimal.

Acknowledgements

This work was supported in part by National Research Foundation Singapore under its NRF Fellowship Programme [NRF-NRFFAI1-2019-0004], Ministry of Education Singapore Tier 2 grant MOE-T2EP20121-0011, and Ministry of Education Singapore Tier 1 Grant [R-252-000-B59-114]. The computational work for this article was performed on resources of the National Supercomputing Centre, Singapore www.nscc.sg. One of the authors (Sen) acknowledges the support of the National University of Singapore during his sabbatical at NUS. We thank Mate Soos for his help in debugging, Kaustav Basu for providing benchmark problems, and anonymous reviewers for their constructive feedback.