On Testing Containedness between Geometric Graph Classes using Second-order Quantifier Elimination and Hierarchical Reasoning

Abstract

We consider geometric graphs in terms of graph classes which are axiomatically described by logical formulae. Our general method to prove graph properties is to show that one graph class is contained in another one, thus, the subclass inherits all properties already known for the superclass. The methods we use for automatically proving such subclass relations are based on second-order quantifier elimination and hierarchical reasoning. As a proof of concept we apply our method to show in how far given specific geometric graph classes with vertices on a plane are planar drawings. Specifically the graph classes we consider here have been used in the context of algorithmic wireless network research.

Introduction

Classes of geometric graphs occurring in algorithmic wireless network research can be described using axioms over suitable theories. Such axioms typically refer to points in R2 (and possibly also their coordinates) and often describe geometrical conditions for the existence resp. non-existence of edges.

In this paper we devise methods for checking containedness between graph classes (our focus here are graph classes that can be described with universally quantified axioms). If containedness cannot be proved, the methods we use allow us to generate counterexamples.

Checking containedness is in so far of interest, as it provides a general tool to check graph properties resulting from distributed graph algorithms. For example, showing containedness of the class of graphs resulting from such an algorithm with respect to the class of planar graphs implies that the algorithm produces planar graphs as well. Though in this paper we focus on containedness and planarity as a proof of concept, by bridging two very different disciplines, this work is intended to provide a general future pioneering direction for the design of local distributed algorithms in the context of wireless networks and in graphs in general (such algorithms are used, for example, to route messages [ 12 ] or Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). control the network topology [ 13 ]). The approach we propose (and the tools we use for this) can be a good instrument in theoretical graph and network theory, which would allow the user to test whether certain generalizations of concept are problematic and to locate possible problems with the general formalizations. A typical example we consider is the formalization of a distance between two points: We can assume that graphs have vertices which are points in R2 and the distance between points is the Euclidean distance, but we might also use abstract metric spaces or cost functions for the edges.

Testing containedness of graph classes has been studied by the authors of this paper in recent work. In [ 5 ], formulae representing necessary and sufficient conditions for containedness between certain types of graph classes were derived by hand. In [ 11,10 ] possibilities for combining symbol elimination methods were proposed and applied to (parametric) entailment problems, and used e.g. for checking inclusion between graph classes. In this paper, we propose automated methods for checking inclusion without the manual component in [ 5 ]; for this we rely on methods introduced in [ 11 ]. We are not aware of other similar approaches to the area of computational (geometric) graph theory. Existing approaches use a logical representation of graphs based on monadic second order logic [ 3 ] or higher order theorem provers like Isabelle/HOL [ 1 ]. Our approach is orthogonal: it relies on methods for second-order quantifier elimination which allow a reduction of many problems to satisfiability modulo a suitable theory for which state of the art SMT solvers can be used; the procedure is sound and our approach allows us to identify situations in which completeness can be guaranteed. Structure of the paper. In Sect. 2, we introduce concepts from geometric graph theory. In Sect. 3 we introduce the theoretical tools for our work. In Sect. 4, using concrete examples, we demonstrate the feasibility and strength of our approach for showing containedness and planarity of geometrically described graphs. In Sect. 5 we present conclusions and plans for future work. 2

Graph Classes Related to Planarity Conditions

In the following we consider graphs with vertices in a set X, which can be the set of points in the Euclidean space R2 (or, in some cases, the set of points in an abstract metric space (X, d)). We present a type of graph classes which can be proved to be plane drawings (i.e. planar graphs which are drawn on the plane in such a way that edges do not intersect). We model such graph classes by using a unary predicate V and a binary predicate E, such that for every element x ∈ X, V (x) is true if x is a vertex of the graph and E(x, y) is true if x, y are vertices and there is an edge between x and y. We consider undirected graphs without self-loops. Such properties can be described by the axioms K0: K0 = {∀x(¬E(x, x)), We consider the following classes of graphs.

∀x, y E(x, y) → E(y, x), The class P of plane drawings can be described using the axiom: (P) ∀u, v, w, x : E(w, x) ∧ πP (u, v, w, x) → ¬E(u, v) ∀x, y E(x, y) → V (x) ∧ V (y)}. where πP (u, v, w, x) is a predicate which is true iff w and x are in different half planes defined by the line uv passing through u and v, and u and v are in different half planes defined by the line wx passing through w and x.1 We can express this either using analytic geometry or (if d is a metric) by the following formula: πP(u, v, w, x) := V (u) ∧ V (v) ∧ V (x) ∧ V (w) ∧ u 6= v ∧ w 6= x∧

∃m(d(u, m) + d(m, v) = d(u, v) ∧ d(w, m) + d(m, x) = d(w, x)) The class G of Gabriel graphs [ 2 ] is axiomatized by K0 together with: (G)

∀u, v E(u, v) ↔ πG(u, v) where πG(u, v) expresses the fact that u and v are vertices and every vertex different from u and v lies outside of the minimal circle passing through u and v. If m(u, v) is the middle of the segment uv, we can express this by: πG(u, v) := V (u) ∧ V (v) ∧ u 6= v ∧

∀w w 6= u ∧ w 6= v ∧ V (w) → d(m(u, v), w) > d(m(u, v), u) .

We define superclasses G→ and G← of G: G→ is defined by only keeping the ”→” implication in (G), and G← by only keeping the ”←” implication. The class R of relative neighborhood graphs [ 9 ] is described by K0 and: (R)

∀u, v E(u, v) ↔ πR(u, v) where πR is defined by:

πR(u, v) := V (u)∧V (v)∧u 6= v∧∀w (V (w) → d(u, w) ≥ d(u, v)∨d(w, v) ≥ d(u, v)). We can define superclasses R→ and R← of R: R→ is defined by only keeping the ”→” implication in (R), and R← by only keeping the ”←” implication. We model such graph classes using a logical language and consider extensions of the theory of real numbers and of theories modeling the points with additional functions symbols (V , E, distances, etc.). In [ 11 ] we proved that the properties of theory extensions occurring in this context allow us to define sound, complete and terminating proof procedures. We present a summary of the theoretical results and then several examples. 3

Theories and Theory Extensions

We assume that basic notions in (many-sorted) first-order logic such as signature Π, Π-structure, theory, satisfiability, unsatisfiability and entailment, possibly w.r.t. a theory are known.

Let Π0=(Σ0, Pred) be a signature, and T0 be a “base” theory with signature Π0. We consider extensions T := T0∪K of T0 with new function symbols Σ (extension functions) whose properties are axiomatized using a set K of (universally closed) clauses in the extended signature Π = (Σ0 ∪ Σ, Pred), such that each clause in K contains function symbols in Σ. Especially well-behaved are the Ψ -local theory 1 For the existence of these lines it is necessary that u 6= v and w 6= x. If, for instance, the vertex w is located on the line through u and v, but not equal to u or v, it is located in both half planes; hence, in this case the segments uv and wx intersect. extensions, i.e. theory extensions T0 ⊆ T0 ∪ K in which for every finite set G of ground ΠC -clauses (containing an additional set C of constants) it holds that

T0 ∪ K ∪ G |= ⊥ if and only if T0 ∪ K[ΨK(G)] ∪ G is unsatisfiable, where, for every set G of ground ΠC -clauses, K[ΨK(G)] is the set of instances of K in which the terms starting with a function symbol in Σ are in ΨK(G) = Ψ (est(K, G)), (where est(K, G) is the set of ground terms starting with a function in Σ occurring in G or K). Ψ -local extensions can be recognized by showing that certain partial models embed into total ones [ 14,8 ].

In local theory extensions hierarchical reasoning is possible: Assume that T0 ⊆ T1 = T0 ∪ K is a Ψ -local theory extension. We can reduce the problem of checking the satisfiability of any finite set G of ground clauses w.r.t. T0 ∪ K to a satisfiability test w.r.t. T0 as follows: For any finite set G of ΠC -ground clauses, T0 ∪ K ∪ G is satisfiable iff T0 ∪ K[ΨK(G)] ∪ G is satisfiable. Let K0 ∪ G0 ∪ Def be obtained from K[ΨK(G)] ∪ G by introducing, in a bottom-up manner, new constants ct ∈ C for subterms t=f (c1, . . . , cn) where f ∈Σ and ci are constants, together with definitions ct=f (c1, . . . , cn) (included in Def) and replacing the corresponding terms t with the constants ct in K and G.

Theorem 1 ([ 14 ]) Let K be a set of clauses. Assume that T0 ⊆ T1 = T0 ∪ K is a Ψ -local theory extension and let G be a finite set of ΠC -ground clauses. Let K0 ∪G0 ∪Def be obtained from K[ΨK(G)]∪G as explained before. Then T1 ∪G |=⊥ n iff T0 ∪K0 ∪G0 ∪Con0 |=⊥, where Con0={ ^ ci≈di → c≈d | ff ((cd11,,......,,cdnn))≈≈cd∈∈DDeeff }. i=1 Chains of extensions. We can also consider chains of theory extensions:

T0 ⊆ T1 = T0 ∪ K1 ⊆ T2 = T0 ∪ K1 ∪ K2 ⊆ · · · ⊆ Tn = T0 ∪ K1 ∪ ... ∪ Kn in which each theory is a local extension of the preceding one. For a chain of n local extensions a satisfiability check w.r.t. the last extension can be reduced (in n steps) to a satisfiability check w.r.t. T0. This iterated instantiation procedure has been implemented in H-PILoT [ 7 ] – the only restriction needed in this case is that at each step the clauses reduced so far need to be ground. 4

Examples

In this section, we demonstrate the power of hierarchical reasoning and quantifier elimination for automatically proving graph properties. We show here as a proofof-concept that the methods described in Section 3 can be used to prove the planarity of specific Euclidean graph classes.2 For determining the concrete proof tasks for testing containment of graph classes we used a form of abstraction that allowed us to use SCAN [ 6 ] for second-order quantifier elimination (Section 4.1). The proof tasks are then solved (Section 4.2) using the hierarchical reduction

2 Informations on the tests we made are available under

https://userpages.uni-koblenz.de/∼sofronie/tests-graphs-2021. method described in Theorem 1. This method is implemented in H-PILoT [ 7 ] for the case when Ψ is the identity. For a proof task of the form T0 ∪ K ∪ G, H-PILoT computes T0 ∪ K[G] ∪ G, performs the hierarchical reduction described in Theorem 1 constructing the formula T0 ∪ K0 ∪ G0 ∪ Con0, and calls a prover for the base theory (for instance Z3 or Redlog) and outputs the answer of the selected prover3. (In general, chains of theory extensions are considered and the instantiation procedure is iterated.) 4.1

Second-order Quantifier Elimination for Class Inclusion We present some simple examples in which second-order quantifier elimination allows us to determine constraints on abstract predicates used in the description of the classes under which inclusions hold. We analyze the type of axioms considered in Sect. 2 using a binary predicate E for the edges and (abstract) predicates representing additional conditions.

Example 1. Consider the classes C1 and C2, described by axioms of the form AxCi : ∀u, v E(u, v) ↔ πi(u, v)

i = 1, 2 We know that C1 ⊆ C2 iff AxC1 ∧ ¬AxC2 is unsatisfiable. We have: AxC1 ∧ ¬AxC2 ≡ ∀u, v (E(u, v) ↔ π1(u, v)) ∧ ∃u, v(E(u, v) ∧ ¬π2(u, v)) ∨ ∀u, v (E(u, v) ↔ π1(u, v)) ∧ ∃u, v(¬E(u, v) ∧ π2(u, v)) We used SCAN to eliminate the predicate symbol E and obtained: ∃E(∀u, v E(u, v) ↔ π1(u, v) ∧ ∃u, v (E(u, v) ∧ ¬π2(u, v))) ≡ ∃u, v(π1(u, v) ∧ ¬π2(u, v)) ∃E(∀u, v E(u, v) ↔ π1(u, v) ∧ ∃u, v (¬E(u, v) ∧ π2(u, v))) ≡ ∃u, v(¬π1(u, v) ∧ π2(u, v)). Hence, C1 ⊆ C2 iff ∃u, v(π1(u, v) ∧ ¬π2(u, v)) ∨ (¬π1(u, v) ∧ π2(u, v)) is false w.r.t. T . This is the case iff ∀u, v(π1(u, v) ↔ π2(u, v)) is true w.r.t. T . It is easy to see that these conditions are also equivalent to C2 ⊆ C1 and to C1 = C2. Example 2. Let C be a class of graphs described by axioms AxC and P the class of plane drawings, described by the axiom AxP, where:

AxC : AxP :

∀u, v E(u, v) ↔ πC(u, v) ∀u, v, w, x E(w, x) ∧ πP(u, v, w, x) → ¬E(u, v).

C ⊆ P iff AxC ∧ ¬AxP |=T ⊥. AxC ∧ ¬AxP is equivalent to:

∀u, v (E(u, v) ↔ πC(u, v)) ∧ ∃u, v, w, x(E(w, x) ∧ πP(u, v, w, x) ∧ E(u, v)). We used SCAN to eliminate the predicate symbol E, and obtained: ∃E(AxC ∧ ¬AxP) ≡ ∃u, v, w, x(πP(u, v, w, x) ∧ πC(w, x) ∧ πC(u, v)). Thus, C ⊆ P iff πP(a, b, c, d) ∧ πC(c, d) ∧ πC(a, b) is unsatisfiable w.r.t. T . 3 The answer can only be trusted if all theory extensions in the chain are local (or have complete finite instantiation and we ensure, when preparing the input for H-PILoT, that all necessary instances are considered). Remark 1 If we consider the class C→ (described by axiom AxC→ obtained by only taking the direct implication in AxC) and use SCAN we obtain: ∃E(AxC→ ∧ ¬AxP) ≡ ∃u, v, w, x(πP(u, v, w, x) ∧ πC(w, x) ∧ πC(u, v)). Therefore C ⊆ P iff C→ ⊆ P.

Example 3. C→ ⊆ D→ iff ∀u, v(E(u, v) → πC(u, v)) ∧ ∃a, b(E(a, b) ∧ ¬πD(a, b)) is unsatisfiable w.r.t. T . Using e.g. SCAN we prove that this is the case iff πC(a, b) ∧ ¬πD(a, b) |=T ⊥ i.e. iff ∀x, y(πC(x, y) → πD(x, y)) is valid w.r.t. T . For the type of axioms considered above, SCAN terminated and returned relatively simple first-order formulae. In [ 4 ] a method for computing weakest sufficient conditions for a formula F based on second-order elimination techniques is presented; situations are identified under which conditions generated this way are first-order formulae. These results might be useful when analyzing more general graph classes. 4.2

Using Hierarchical Reasoning for Checking Class Inclusion Let T be a theory used for formalizing points, distance and vertices, with two sorts p (points, uninterpreted) and num (reals, interpreted). The concrete form of this theory depends on the model for the set of points and distances we choose. If we model the Euclidian plane with the Euclidean distance, T can be defined starting from the combination of a theory of points P and the theory R of real numbers, using a chain of theory extensions: (E)

P ∪ R ⊆ P ∪ R ∪ Freex,y ⊆ T = P ∪ R ∪ Freex,y ∪ Tde where x and y are the coordinate functions and Tde is the axiom stating that the Euclidean distance between points u, v is d(u, v) = p(x(u)−x(v))2+(y(u)−y(v))2. If we model arbitrary metric spaces (X, d), T is the extension: (M ) P ∪ R ⊆ T = P ∪ R ∪ Tdm where Tdm are the axioms of a metric. All these extensions are local: in (E) we have extensions with free function symbols and definitional extensions [ 14 ]; in [ 11 ] we proved that the axioms of a metric define a Ψ -local extension of P ∪ R. Example 4. We analyze the relation between the classes G→ and R→: AxG→ : ∀u, v (E(u, v) → πG(u, v))

AxR→ : ∀u, v (E(u, v) → πR(u, v)).

By Example 3, G→ ⊆ R→ iff πG(u, v) ∧ ¬πR(u, v) is unsatisfiable w.r.t. T , and R→ ⊆ G→ iff πR(u, v) ∧ ¬πG(u, v) is unsatisfiable w.r.t. T , where the predicates πG and πR are described (for an arbitrary distance function d) by: πG(u, v) := V (u) ∧ V (v) ∧ u 6= v∧

∀w w 6= u ∧ w 6= v ∧ V (w) → d(m(u, v), w) > d(m(u, v), u) .

πR(u, v) := V (u) ∧ V (v) ∧ u 6= v ∧ ∀w (V (w) → d(u, w) ≥ d(u, v) ∨ d(w, v) ≥ d(u, v)) where m(u, v) is the middle point of the segment uv. If u and v are considered to be constants then both the extension of T with a function V satisfying condition πG(u, v), and the extension of T with a function V satisfying condition πR(u, v) can be proved to be local. We therefore can use H-PILoT for the proof tasks. We first consider the case where d is the Euclidean distance. Then we analyze this problem for the more general case where d is an arbitrary metric. Case 1: d is the Euclidean distance. We check both inclusions. (i) To prove that R→ ⊆ G→ holds, it is sufficient to show that πR(u, v)∧¬πG(u, v) is unsatisfiable. The formula obtained after Skolemization and simplification from ¬πG(u, v) is a ground formula; the coordinates of the middle m of uv can be computed as usual; we add conditions: x(p) 6= x(q) ∨ y(p) 6= y(q) for p, q ∈ {u, v, w, m}. H-PILoT derives unsatisfiability, i.e. proves that R→ ⊆ G→.4 (ii) For proving that G→ 6⊆ R→ we show that πG(u, v) ∧ ¬πR(u, v) is satisfiable. H-PILoT gives the answer satisfiable and produces the following model: u = (1, 0), v = (7, −8), w = (−1, −5), m = (4, −4).

Case 2: d is an arbitrary metric. We again check for both directions of containment whether the corresponding formula holds (assuming that we have distinct vertices). For d we have the metric axioms, proved to be Ψ -local in [ 11 ]. For the direction πR(u, v) → πG(u, v) H-PILoT answers satisfiable and returns the following model (impossible in the Euclidean space):

d(u, v) = 6, d(u, m) = 3, d(v, m) = 3, d(u, w) = 6, d(v, w) = 5, d(w, m) = 3. Thus, the containment R→ ⊆ G→ is true in the Euclidean space, but not for arbitrary metric spaces. For the direction πG(u, v) → πR(u, v) we also get a model describing a situation which cannot occur in the Euclidean space. Example 5. We show that G→ ⊆ P. By Example 2, this holds iff πP(u, v, w, x) ∧ πG(w, x) ∧ πG(u, v) is unsatisfiable. With the encoding with the Euclidean distance H-PILoT did not terminate after 3 minutes. If d is an arbitrary metric then H-PILoT returns ”unsatisfiable” (after 102.62 s.), which shows that G→ ⊆ P. By Example 4, R→ ⊆ G→ ⊆ P, hence, by Remark 1, G ⊆ P and R ⊆ P. We thus proved that the class G of Gabriel graphs and the class R of relative neighborhood graphs are subclasses of the class P of plane drawings. 5

Conclusions and Future Work

We demonstrated by example that hierarchical reasoning and quantifier elimination is a powerful tool to analyze properties of graph classes defined by general and Euclidean metrics. In subsequent work, we intend to investigate many more graph properties, e.g., spanner properties (Euclidean, topological, energy), and degree limitation. These concepts are of interest for algorithm design in wireless graph models but also on graphs in general. Furthermore, we plan to significantly expand the set of graph classes that can be analyzed with our tool set.

4 The full test where all instances are considered is available under

https://userpages.uni-koblenz.de/∼sofronie/tests-graphs-2021.

References

1. Mohammad Abdulaziz , Kurt Mehlhorn, and Tobias Nipkow . Trustworthy graph algorithms (invited talk) . In Peter Rossmanith , Pinar Heggernes, and JoostPieter Katoen, editors, Proc. 44th Int. Symposium on Mathematical Foundations of Computer Science (MFCS 2019 ), volume 138 of LIPIcs , pages 1 : 1 - 1 : 22 . Schloss Dagstuhl - Leibniz-Zentrum fu¨r Informatik, 2019 .

2. Prosenjit Bose , Pat Morin, Ivan Stojmenovi´c, and Jorge Urrutia. Routing with Guaranteed Delivery in Ad Hoc Wireless Networks . Wireless Networks , 7 ( 6 ): 609 - 616 , nov 2001 .

3. Bruno Courcelle . The expression of graph properties and graph transformations in monadic second-order logic . In Grzegorz Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations , Volume 1 : Foundations, pages 313 - 400 . World Scientific, 1997 .

4. Patrick Doherty , Witold Lukaszewicz, and Andrzej Szalas . Computing strongest necessary and weakest sufficient conditions of first-order formulas . In Bernhard Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001 , pages 145 - 154 . Morgan Kaufmann, 2001 .

5. Hannes Frey and Lucas Bo¨ltz. Automatically testing containedness between geometric graph classes defined by inclusion, exclusion and transfer axioms . In Proceedings of the 33rd Canadian Conference on Computational Geometry , CCCG 2021 , pages 127 - 138 , 2021 .

6. Dov M. Gabbay and Hans Ju¨rgen Ohlbach. Quantifier elimination in second-order predicate logic . In Bernhard Nebel, Charles Rich, and William Swartout, editors, Principles of Knowledge Representation and Reasoning (KR92) , pages 425 - 435 . Morgan Kaufmann, 1992 . Also published as a Technical Report MPI-I-92-231 , Max- Planck-Institut fu¨r Informatik, Saarbru¨cken, and in the South African Computer Journal , 1992 .

7. Carsten Ihlemann and Viorica Sofronie-Stokkermans . System description: HPILoT . In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2- 7 , 2009 . Proceedings, LNCS 5663 , pages 131 - 139 . Springer, 2009 .

8. Carsten Ihlemann and Viorica Sofronie-Stokkermans . On hierarchical reasoning in combinations of theories . In Ju¨rgen Giesl and Reiner Ha¨hnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173 , pages 30 - 45 . Springer, 2010 .

9. Brad Karp and H. T. Kung . GPSR: Greedy perimeter stateless routing for wireless networks . In Proceedings of the 6th Annual International Conference on Mobile Computing and Networking , pages 243 - 254 , 2000 .

10. Dennis Peuter , Philipp Marohn , and Viorica Sofronie-Stokkermans. Symbol elimination for parametric second-order entailment problems (with applications to problems in wireless network theory) . CoRR , https://arxiv.org/abs/2107.02333, 2021 .

11. Dennis Peuter and Viorica Sofronie-Stokkermans . Symbol elimination and applications to parametric entailment problems . In Boris Konev and Giles Reger, editors, Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021 , Proceedings, LNCS 12941 , pages 43 - 62 . Springer, 2021 .

12. Asmaa Rady , El-Sayed M. El-Rabaie , Mona Shokair , and Nariman Abdel-Salam. Comprehensive survey of routing protocols for mobile wireless sensor networks . Int. J. Commun. Syst. , 34 ( 15 ), 2021 .

13. Pallavi Singla and Amit Munjal . Topology control algorithms for wireless sensor networks: A review . Wirel. Pers. Commun. , 113 ( 4 ): 2363 - 2385 , 2020 .

14. Viorica Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions . In Robert Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Proceedings, LNCS 3632 , pages 219 - 234 . Springer, 2005 .