key: cord-0440833-uovhtaxb authors: Eppstein, David; Goodrich, Michael T.; Liu, James A.; Matias, Pedro A. title: Tracking Paths in Planar Graphs date: 2019-08-15 journal: nan DOI: nan sha: ae40de95e3ca8b257f206f447f177468350e3acb doc_id: 440833 cord_uid: uovhtaxb We consider the NP-complete problem of tracking paths in a graph, first introduced by Banik et. al. [3]. Given an undirected graph with a source $s$ and a destination $t$, find the smallest subset of vertices whose intersection with any $s-t$ path results in a unique sequence. In this paper, we show that this problem remains NP-complete when the graph is planar and we give a 4-approximation algorithm in this setting. We also show, via Courcelle's theorem, that it can be solved in linear time for graphs of bounded-clique width, when its clique decomposition is given in advance. Motivated by applications in surveillance and monitoring, Banik et. al. [3, 2] introduced the problem of tracking paths in a graph. In essence, the goal is to uniquely determine the simple path traversed by a moving subject or object, based on a sequence of vertices sampled from that path. Examples of surveillance applications include the following: (i) vehicle tracking in road networks; (ii) habitat monitoring; (iii) intruder tracking and securing large infrastructures; (iv) tracing back of illicit Internet activities by tracking data packets. Another application would be to determine the nodes in a network that have been compromised by a spreading infection, given an incomplete transmission history of a pathogen. This information can be helpful in identifying and attenuating the negative impact caused by biological and non-biological infectious agents, such as: Highly-contagious diseases (e.g. Severe Acute Respiratory Syndrome) which could lead to epidemics [13] . Fake news and hate speech being disseminated in social networks, as well as violations of privacy (e.g. sharing without permission highly sensitive content owned by a user, such as intimate pictures). Computer viruses, which spread throughout servers scattered across the Internet Essentially, an entry-exit pair (s , t ) (see Figure 1) ) with respect to a cycle C represents two alternative s − t paths and, thus, requires tracking at least one of its branches. We say that (s , t ) is tracked with respect to C if and only if C \{s , t } contains a tracker. In addition, C is tracked if and only if there is no entry-exit pair with respect to C that is untracked. If a cycle contains either (i) 3 trackers or (ii) s or t and 1 tracker in a non-entry/non-exit vertex, then it must be tracked. We say that these cycles are trivially tracked. An alternative characterization of a tracking set, first given by Banik et al [2] , is the following. The overall idea for the approximation algorithm builds on the following two ideas: 1. The cardinality of the optimal solution cannot be much smaller than the number of faces in the graph. 2. The average number of trackers per face does not need to be very large. The first idea gives us a lower bound on OPT , the cardinality of an optimal solution. The second gives us an upper bound on ALG, the cardinality of our approximation algorithm. We consider the following reduction, which takes care of disconnected components, or components that are "attached" to the graph by a cut vertex that is not in an s − t path. While there exists an edge or vertex that does not participate in any s − t path, remove it from the graph. Lemma 5. After Reduction 1, every simple cycle in the graph contains at least one entry-exit pair. This holds for non-planar graphs as well. Proof. Let C by some simple cycle in the graph. After Reduction 1, there must exist an s − t path that shares an edge with C. The first and last vertices on this path that belong to C correspond to an entry-exit pair. In an embedded undirected planar graph G that results from Reduction 1, OPT ≥ (|F | − 1)/2, where F is the set of faces of G. (a) Tracker on x (red) is inactive due to the violation of Condition (i). Tracker on x (red) is inactive due to the violation of Condition (ii). Notice that x is entry for exit vertices u and v (with respect to C), therefore C needs another tracker. On a high level, the proof of Lemma 6 is done by keeping a set of "active" trackers while reconstructing a planar embedding E of G: we start, as a base case, with any simple s − t path in E and iteratively add faces to it until it matches E. Given a fixed, optimal tracking set T * , the addition of each face requires either (i) adding a new tracker from T * to the active set, or (ii) deactivating an active tracker, rendering it useless for distinguishing paths on future faces. As a consequence, each tracker charges at most two faces: the one adding the tracker and the one deactivating it. This demonstrates that |T * | ≥ (|F | − 1)/2. Let outer(E τ ) be the set of outer-edges of our planar reconstructing embedding E τ at time τ . At time τ = 0, our embedding corresponds to an s−t path and, for all 0 ≤ τ ≤ |F |−1, we add exactly one face C from E to E τ , by connecting two vertices u and v in outer(E τ ) with a simple path p (see Figure 8 in the appendix). In doing so, we erase an u − v path p in outer(E τ ), so we have that outer(E τ +1 ) = outer(E τ ) \ p ∪ p. In the end, E |F | = E. By Lemma 5, there is at least one entry-exit pair in E with respect to face C, so any tracking set must contain a tracker on some vertex of C. During the reconstruction process, we maintain a list of trackers in sets A and A , such that (A ∪ A ) ⊆ T * , where A contains active trackers and A contains inactive ones. A tracker in vertex v is active at time τ if and only if it meets both of the following conditions: Intuitively, an active tracker can be used to track future faces, although no more than one (see below). An inactive tracker, on the other hand, either cannot be used to track future faces (Condition (i)), or its corresponding vertex is entry/exit for some future face (Condition (ii)), in which case we require yet another tracker on that face (see Figure 2 ). Condition (ii) is necessary for dealing with embeddings of G where at least one of s and t is not in the outer face. First, we argue that each time we add a face during the reconstruction process described above, we either (i) need to increase the number of active trackers (by adding it to either A or A ), or (ii) we can get away by re-using and, therefore, deactivating an active tracker. We assume for the rest of the argument that t is on the outer face, because such a planar embedding is always possible to construct. Let C be the face added a time τ by connecting vertices u and v in outer(E τ ), as specified above. In addition, let T * be any optimal solution (i.e. |T * | = OPT ). We consider two cases, depending on the existence of a tracker in C at time τ : By Lemma 5, there exists a vertex x ∈ C such that x ∈ T * . We place a tracker on x. If x ∈ outer(E τ +1 ) we add x to A, otherwise we add it to A . Let y ∈ C ∩ A be a vertex of C with a tracker. We again consider two cases: (i) y / ∈ {u, v}. Then, y ∈ outer(E τ ) but y / ∈ outer(E τ +1 ), which amounts to moving y from A to A . (ii) y ∈ {u, v}. If (u, v) is an entry-exit pair with respect to C, or if the tracker in y is not active, then there exists x ∈ C \ {u, v} such that x ∈ T * . Similarly to Case 1, we place a tracker on x , which corresponds to adding x either to A or A . Otherwise, the tracker in y is active and (u, v) is not an entry-exit pair with respect to C. Let us assume without loss of generality that y = u. Then, the addition of C deactivates the tracker in u by definition of active tracker (Condition (ii) is now violated), so we move u from A to A . Every tracker in A is charged by at most two faces: one for adding an active tracker to A and another for deactivating it and moving it to A . Therefore, |F |−1 ≤ |A|+2|A |. Since |A| + |A | ≤ |T * |, it follows that |F | − 1 ≤ 2OPT . A tight example for the lower bound on OP T is illustrated in Section 3.1. We say that an undirected planar graph is reduced if it cannot be further reduced by Reduction 1 or any of the following reductions. While there exist two adjacent vertices of degree 2, remove one of them (and its edges) and add an edge connecting its neighbors. Reduction 3. While there exists vertex v / ∈ {s, t} of degree 2 in a 3-cycle, place a tracker on v and remove it and its edges from the graph. Reduction 4. While there exist non-adjacent vertices u, v / ∈ {s, t} of degree 2 in a 4-cycle, place a tracker on either u or v and remove it and its edges from the graph. Reductions 2, 3 and 4 can be applied interchangeably and in any order until none of them is applicable, but we will see that they need to be carried out after Reduction 1. Fortunately, we will not be required to re-apply Reduction 1 after performing the remaining reductions. We denote the degree of a vertex v by deg(v), where the underlying graph can be determined from its context. Proof. Trivial by Definition 1. Claim 8. Reductions 2, 3 and 4 maintain the property that every cycle in G contains at least one entry-exit pair (see Lemma 5) . Proof. Reductions 2, 3 and 4 only erase faces and vertices of degree 2, which cannot be in entry-exit pairs (by Claim 7), so every simple cycle of the graph still contains an entry-exit pair. Reduction 2 is safe and can be done in polynomial time, if done after Reduction 1. Proof. By Lemmas 4, 9, 10 and 11, Reductions 1-4 are safe, so let us assume without loss of generality that G is reduced. Then, every cycle of G of 5 or more vertices is trivially tracked, because it must contain at least 3 vertices of degree at least 3 (by Reduction 2). Similarly, every 3-or 4-cycle must contain at least 3 vertices of degree at least 3 by Reduction 2 and Reductions 3 and 4 (respectively). Proof. Notice that each tracker added during Reductions 3 and 4 is associated with the removal of one face from G. Therefore, it is enough to show that the lemma holds with respect to a reduced graph G. Let us partition consist of the vertices of degree 2 and degree at least 3, respectively (notice that there cannot be vertices of degree 1). The lemma statement follows from Lemma 13 and the fact that |F | ≥ |V ≥3 | 2 + 2. This inequality can be derived by plugging in the inequality 2|E| ≥ 3|V ≥3 | + 2|V 2 | in Euler's formula for planar graphs: |V | − |E| + |F | = 2, where E is the set of edges of G. A tight example is illustrated in Section 3.1. Proof of Theorem 3. By Lemmas 6 and 14, Algorithm A is a 4-approximation to Planar-Tracking. We show that Planar-Tracking is NP-hard, by reducing from Planar-3-sat, a special version of the satisfiability problem, shown to be NP-complete by Lichtenstein [17]. In 3-sat, we are given a set X = {x 1 , . . . , x p } of variables and a 3-CNF formula φ, where each clause in φ is a disjunction of exactly three distinct literals with respect to X . The goal is to find a boolean assignment to all variables in X that satisfies φ. Consider the bipartite graph with a vertex for each clause C in φ and each variable x i ∈ X , and edges (x i , C) if and only if C contains x i or its negation x i . Lichtenstein [17] showed that Planar-3-sat, the subset of instances of 3-sat whose underlying bipartite graph is planar, remains NP-complete. In particular, the definition of Planar-3-sat requires that a cycle can be drawn connecting all of the variables while maintaining planarity. Later, Knuth and Raghunatan [16] exploited this condition to show that we can always draw the underlying bipartite graph of a Planar-3-sat instance in a rectilinear fashion without crossings (example in Figure 10a ): variables are arranged in a horizontal line and clauses are horizontal line segments with vertical legs to represent the literals present in the clause. Vertical legs attach to the appropriate variables and are labeled red for negated literals and blue, otherwise. In particular, a given clause is drawn completely above or below the line of variables. We convert a planar rectilinear drawing D of an instance of Planar-3-sat, with formula φ and a set X of variables, into a planar drawing G corresponding to the instance of Planar-Tracking. The reduction is straightforward: The union of all the variable and clause gadgets constitutes G (see example in Figure 10 in the appendix). Details of each gadget are given below. For simplicity, we avoid introducing too many subscripts and we rely on pictures to describe the gadgets. Each variable gadget is linked with the next one by setting t i = s i+1 , to form a horizontal chain of gadgets, where s = s 1 and t = t p . For convenience, we force trackers in all the s i (except s), by drawing edges between the α (β ) of a variable gadget and the α (β) of the next variable gadget in the chain. We refer to the resulting drawing as the spine. There are exactly two minimum tracking sets associated with the variable gadget with source s i and destination t i . One of them corresponds to a true assignment of x i and the other one to a false assignment. Both of them require tracking the vertices in R = {α, α , β, β , µ 1 , µ mi }, as well as the remaining µ k . In addition, the true assignment tracks the even-indexed h k and odd-indexed l k , while the false assignment tracks the odd-indexed h k and even-indexed l k . This requires 2m i + 4 trackers in total. Lemma 15. The true and false assignments are the only minimum tracking sets. Clause gadget. Let C = ( a ∨ b ∨ c ) be a clause in φ with literals corresponding to variables x a , x b , x c ∈ X . Its gadget, depicted in Figure 6 , is a face F C consisting of: literal vertex α from x a 's gadget, corresponding to literal a ; adjacent literal vertices β 1 , β 1 , β 2 , β 2 , β 3 from x b 's gadget, corresponding to literals alternating between b and b ; literal vertex γ from x c 's gadget, corresponding to literal c ; edges (α, γ), (α, β 1 ), (β 3 , γ) and the edges from x b 's gadget connecting all of the β k and β k . We can increase the lengths of the variable gadgets to any polynomial that provides enough literal vertices for all clauses. Since D is planar, there are no crossings between clauses. We also impose the following restrictions: 1. α cannot be one of {h 1 , l ma }; this ensures that the only faces in x a 's gadget that do not require 3 trackers do not become untracked. We apply the equivalent restriction to β 1 , β 3 and γ. 2. The α k /α k , (see Figure 6 ) cannot belong to any other clause gadget; these correspond to the 4 literal vertices following α in x a 's gadget and reserving them ensures that non-clause faces, between nested clauses, are tracked. We apply the equivalent restriction to the γ k /γ k . 3. All literal vertices in a clause need to be on the same side of the spine; this restriction is trivial because D is rectilinear, but it simplifies the analysis. Theorem 17. There exists a polynomial time reduction from Planar-3-sat to Planar-Tracking. It remains to show that Planar-Tracking is in NP; Banik et. al. [2] prove this in the more general case of Tracking. We show that Tracking can be solved in linear time when the input graph has bounded clique-width, by applying Courcelle's theorem [7, 8, 10 ], a powerful meta-theorem that establishes fixed-parameter tractability of any graph property that is expressible in monadic second order logic. Clique-width, first introduced by Courcelle et. al. [9] and revisited by Courcelle and Olariu [12] , is an important graph parameter that, intuitively, measures the closeness of a graph to a cograph -a graph with no induced 4-vertex paths. It is closely related to tree-width, another influential graph parameter that measures closeness of a graph to a tree and that was first introduced by Bertelé and Brioschi [4] and later rediscovered by Halin [15] and Robertson and Seymour [22] . While both parameters are determined based on specific hierarchical decompositions of a graph, the clique-width is strictly more powerful in the sense that the class of graphs of bounded clique-width includes all graphs of bounded tree-width, but not vice-versa. Details on the relationship between these parameters can be bound in Courcelle and Engelfriet [8] . Graphs of bounded clique-width include series-parallel graphs, outerplanar graphs, pseudoforests, cographs, distance-hereditary graphs, etc. MSO 1 vs MSO 2 . Second order logic extends first order logic, by allowing quantification over relations (of any fixed arity) on the elements of the domain of discourse. Monadic second order logic itself only allows quantification over unary relations (subsets of the domain of discourse) and, in the logic of graphs, it comes in two flavors: MSO 1 and MSO 2 . The only distinction between these is that the latter allows edges to be elements of the domain of discourse (and thus be quantified over), while the former does not. Besides the quantifiers (∀ and ∃) and the standard logic operations ¬, ∧, ∨, →, both logics include predicates for equality (=) and relation membership (∈). In addition, MSO 1 includes a predicate (∼) that determines vertex adjacency and MSO 2 includes a predicate for vertex-edge incidence. MSO 2 is, by definition, strictly more expressive, for example: Hamiltonicity can be expressed using MSO 2 , but not using MSO 1 . Details on the distinction between the two logics can be found in [8] . Courcelle's theorem. Courcelle et. al. [7, 10] showed that any graph property expressed in MSO 1 and MSO 2 is FPT under clique-width and tree-width (respectively). More specifically, they showed that any MSO 1 -, MSO 2 -expressible property can be tested in f (k, l) · n and g(k , l ) · (n + m) time (respectively) for graphs of clique-width k and tree-width k , where: f and g are computable functions, l and l are the lengths of the logic formulas, n is the number of vertices and m is the number of edges. The result for MSO 2 became known as Courcelle's theorem and it is also valid in optimization problems with linear evaluation functions [11] . Later, Courcelle, Makowsky and Rotics [10] extended these results for MSO 1 . However, while it is possible to construct tree decompositions of width k in linear time [6] , there is no FPT algorithm for finding clique decompositions of clique-width k > 3. Fortunately, it is possible to construct a clique decomposition of width exponential in k in cubic time [20] . In this section, we will take advantage of the latter. We give an alternative definition for tracking set that is easier to express using the logic of graphs. tracking set if and only if there is no s − t simple path P st = P ss ∪ P s t ∪ P t t for s , t ∈ V and corresponding s − s , s − t and t − t paths, such that: 1. There exists an alternative s − t simple path P s t = P s t and 2. T ∩ (P s t ∪ P s t ) ⊆ {s , t }. Remark 20. Definitions 2 and 19 are equivalent. In the logic formulas presented below, we use lowercase letters to quantify over vertices and uppercase letters to quantify over sets of vertices. We use s and t as free variables and, for convenience, we also use set intersection (∩), union (∪) and containment (⊆), without explicitly expressing these operations using MSO 1 . The first two lines of the above equivalence establish that P , Q and R form an s − t path. The last line restricts s and t to be an entry-exit pair with respect to the cycle Q ∪ Q (see Figure 7) and, in addition, establishes that the cycle Q ∪ Q is not tracked. The primitive HasPath(X, a, b) , whose input consists of a set X ⊆ V and vertices a, b ∈ V , verifies the existence of a simple path between a and b that only uses vertices in X. We define it as follows: Remark 21. HasPath(X, a, b) is correctly expressed under MSO 1 and it correctly verifies that there exists an a − b path using only vertices in X. Remark 22. IsTrackingSet is correctly expressed under MSO 1 and it correctly verifies that the given subset of vertices is a tracking set. Theorem 23. Tracking (G, s, t) can be solved in polynomial time if G has bounded cliquewidth. Moreover, if a clique decomposition of bounded width is given, it can be solved in linear time. Proof. This follows directly from Remarks 20 to 22 and the linear time algorithm given by Courcelle [10] for any optimization problem on graphs of bounded clique-width, whose decomposition is given in advance. We showed that Planar-Tracking is NP-complete and we give a 4-approximation algorithm. We also show that, for graphs of bounded-clique width, Tracking can be solved in linear time by applying Courcelle's theorem, as long as its clique decomposition is given in advance. A natural direction of future study would be to improve the approximation ratio of Planar-Tracking or establish constant approximation factors for graphs of larger genus or, more generally, for Tracking. Another open question is to establish the difficulty of Tracking on directed graphs: on one side planar directed acyclic graphs are not known to be NP-hard and, on the other side, it is not known whether its general or planar versions are in NP. Finally, it would be interesting to find efficient algorithms for graphs of bounded tree-width or clique-width without resorting to the finite automaton approach used in Courcelle's theorem. Proof. See proof in [2] . Proof. Banik et. al. [2, Lemma 16] showed that having three adjacent vertices of degree 2 is redundant. Here, we extend their proof and show that we can also get rid of the second adjacent vertex of degree 2. Let u and v be the two adjacent vertices of degree 2, and let u be the other neighbor of u. Notice that v, u are not adjacent, otherwise the u, v edge would then not belong to an s − t path and thus be removed by Reduction 1. Hence, no parallel edges are added to the graph after this reduction. We argue that this reduction is safe by showing that there exists a minimum tracking set that does not include u and v simultaneously. Take any minimum tracking set T that includes u and v. We can always move the tracker from u to u ; this remains a tracking set, because u immediately follows or precedes u on any s − t path. This can only decrease T 's cardinality. This reduction can be done in O(poly(n)) time, by repeatedly checking for the existence of adjacent vertices of degree 2. ∈ {s, t} be the vertex of degree 2 in the triangle ∆vs t (see Figure 9b ). Then, it must be the case that s and t form an entry-exit pair. This follows from (i) the fact that there exists an entry-exit pair in ∆vs t (by Lemma 5) and (ii) the fact that v cannot be in an entry-exit pair (by Claim 7). Then, by Definition 2, any feasible solution must place a tracker on v. Therefore v and its edges can be removed, since it is not a cut-vertex, and it is not in any entry-exit pair, so that its removal does not eliminate an untracked cycle. Clearly, this reduction can be done in O(poly(n)) time. Lemma 27. Reduction 4 is safe and can be done in polynomial time, if done after Reduction 1. ∈ {s, t} be the two vertices of degree 2 that connect the same pair of vertices s and t . Similarly to the proof of Lemma 10, s and t must form an entry-exit pair. So, by Definition 2, any feasible solution must place a tracker in either u or v. By symmetry, we can track and remove u and its edges. Therefore, Reduction 4 is safe by Claim 7 and the facts that u is neither a cut-vertex nor in an entry-exit pair. To prove Lemma 15, we first prove a couple of helpful lemmas and make a few observations: Each vertex in R belongs to a triangle, such that the other two vertices form an entry-exit pair, so must be tracked. Each square face, besides the two including h 2 and l mi−1 , requires 3 tracked vertices. Two adjacent vertices cannot both be untracked. Lemma 28. The true/false assignments of x i correspond to tracking sets with respect to x i 's gadget with source s i and destination t i . Proof. In a true/false assignment of x i , every face of the gadget is trivially tracked, except the faces including s i /t i (which are clearly tracked) and the faces including h 2 and l mi−1 . Though the latter faces may only contain 2 trackers (depending on x i 's truth value and/or m i 's parity), they are nevertheless tracked because one of these trackers cannot be in an entry-exit pair. The remaining cycles, i.e. the ones which are not faces, are also trivially tracked: since these cycles must have size at least 6, they must contain 3 trackers given the observation that no adjacent vertices are untracked. Lemma 29. In a minimum tracking set, each column has exactly 2 trackers. Proof. Since the true/false assignments achieve this property, we only have to show that each column requires at least two trackers. Assume that a minimum tracking set has only one tracker in column 1 < k < m i ; it must be on µ k . Then all vertices on columns k − 1, k + 1 must be tracked. For the average number of trackers per column to be at most 2, the number of trackers per column must be an alternating sequence of . . . 3, 1, 3, 1, . . . , with column 1 and/or column m i only having 1 tracker, which contradicts the square face property. Lemma 30. The true and false assignments are the only minimum tracking sets. Proof. Assume that some µ k is not tracked in a minimum tracking set, for 1 < k < m i . By Lemma 29, we only have to show that this causes a column to have 3 trackers. If k = m i − 1 then column m i must have three trackers. Otherwise, µ k+1 , h k+1 , h k+2 must be tracked, since they share a square face with µ k . If l k+1 is tracked we are done, otherwise, l k+2 must be tracked. Additionally, µ k+2 must be tracked, either by the square face property, or in the case where k = m i − 2, because it is in R. Then, column k + 2 has 3 trackers. Now, if all the µ k are tracked, then the only minimum tracking sets are the true and false assignments, by the observation that two adjacent vertices cannot both be untracked and Lemma 28. Lemma 31. Clause C is satisfied if and only if its corresponding gadget face F C is tracked. Proof. The entry-exit (β 1 , β 2 ) is the only one, with respect to F C , that is tracked if and only if C is satisfied. The remaining entry-exit pairs are tracked by either a β k or a β k . Theorem 17. There exists a polynomial time reduction from Planar-3-sat to Planar-Tracking. Proof. Let (G, G) be an instance of Planar-Tracking that results from applying the transformation described above to an instance (φ, D) of Planar-3-sat, where G and D are the underlying planar embeddings. We show that φ is satisfiable if and only if G has a tracking set of size T = ( (⇐) Choose the truth assignment of each variable according to the given tracking set. The implication follows from Lemma 15 and the fact that if some clause in φ was not satisfied, then its gadget face would have been untracked, a contradiction. (⇒) Place T trackers on the literal vertices that correspond to the satisfiable truth assignment of every variable and on all non-literal vertices (except s and t). We show that this corresponds to a tracking set by arguing that every cycle C in G is tracked. We distinguish between two cases: Case 1: C contains no clause edges. Then C is tracked by (almost) the same argument given in Lemma 28 that shows that a truth assignment of x i corresponds to a tracking set with respect to x i 's gadget. Notice that, because of Restriction 1, clause edges are only added to faces that require 3 trackers, so this does not change the argument for the faces which do not require 3 trackers. The only differences are: (i) the addition of the edges that force trackers in every s i , which only helps the argument, and (ii) the fact that C may span multiple variable gadgets, in which case C must traverse at least 3 trackers on the non-literal vertices between two variable gadgets. Case 2: C contains clause edges. Notice that, by construction of G, C must have at least one spine edge. If C corresponds to a clause face, then it must be tracked by Lemma 16. Otherwise, we show that C contains at least 3 trackers and, thus, is trivially tracked. Let us think of C as alternating non-empty paths of two types: clause paths, which only contain clause edges and spine paths, which only contain spine edges. To avoid dealing with complex cycles, we observe that each spine path in C must contain at least 1 tracker; this follows from the fact at least one of the 2 vertices sharing a spine edge must have a tracker (see variable gadget). Thus, let us assume that C contains no more than 2 spine/clause paths, or otherwise C immediately contains 3 trackers. Notice that if one of the spine paths spans 2 or more variable gadgets, then it must traverse at least 3 trackers on the non-literal vertices between two variable gadgets. Since every clause in φ contains exactly 3 distinct literals and C is simple, the only cases where none of the spine paths span multiple variable gadgets are the following: (a) Example of a Planar-3-sat instance drawn in a rectilinear fashion with clauses A = (x1 ∨ x2 ∨ x3), B = (x1 ∨ x4 ∨ x5), C = (x2 ∨ x3 ∨ x4), D = (x1 ∨ x2 ∨ x5). Example of a Planar-Tracking instance. The orange vertices ensure that no cycle is untracked (see Figure 6 ). Illustration of a Planar-3-sat instance (above) and the corresponding Planar-Tracking instance associated with the reduction described in Section 4 (below). (i) C contains exactly 2 clause paths in different sides of the spine. Then, the 2 spine paths connecting the two sides of the spine must traverse 2 trackers each (see variable gadget). Therefore, C contains at least 4 trackers. (ii) C contains exactly 2 clause paths on the same side of the spine, which both start or both end at the same variable gadget, one nested in the other. Then, by Restriction 2 one of the spine paths contains at least 6 vertices, half of which must be tracked. The Mathematical Theory of Infectious Diseases and its Applications. Charles Griffin & Company Ltd, High Wycombe A polynomial sized kernel for tracking paths problem Tracking paths Nonserial Dynamic Programming Survey of target tracking protocols using wireless sensor network A linear-time algorithm for finding tree-decompositions of small treewidth The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach Handle-rewriting hypergraph grammars