Relational Approximation of Maximum Independent Sets (Extended Abstract) Insa Stucke Institut für Informatik, Christian-Albrechts-Universität zu Kiel, Germany ist@informatik.uni-kiel.de 1 Introduction Previous work has shown that relation algebra (as introduced in [14] and fur- ther developed in [9,12,13,15], for example) is well suited for computational problems on many discrete structures. In particular, adjacency or incidence re- lations can be used to model graphs and special relations like vectors and points to represent subsets of vertices or edges, as shown in [12]. We develop and formally verify a relational program for approximating maximum independent sets in undirected and loop-free graphs. Formal pro- gram verification means to show with mathematical rigor that the program is correct with respect to a formal problem specification, in our case we comply with the assertion-based Floyd-Hoare-approach. At the end, the most interesting task is to prove the desired approximation bound. Of course, therefore we need knowledge about cardinalities of relations. In [7] a characterisation of a cardinality operation is developed and further con- sequences of it were proved. Based on this cardinality operation we not only prove the approximation bound but also facts about the cardinalities of vectors and points in a calculational, algebraic manner only. 2 Relation-Algebraic Preliminaries In this section we recall the fundamentals of relation algebra based on the het- erogeneous approach of [12,13]. Set-theoretic relations form the standard model of relation algebras. We assume the reader to be familar with the basic opera- tions on set-theoretic relations, viz. RT (transposition), R (complementation), R ∪ S (union), R ∩ S (intersection), R;S (composition), the predicates R ⊆ S (inclusion) and R = S (equality), and the special relations O (empty relation), L (universal relation) and I (identity relation). The Boolean operations, the inclu- sion and the constants O and L form Boolean lattices. The theoretical framework for this and many other results concerning re- lations is that of a (heterogeneous) relation algebra in the sense of [12,13], with typed relations as elements. Thus, we write R : X ↔ Y to express that X is the source, Y is the target. The type of R is denoted by X ↔ Y . As constants and operations of a relation algebra we have those of set-theoretic relations, where we frequently overload the symbols O, L and I, i.e., avoid the binding of types 54 I. Stucke to them. If necessary we use indices as e.g., LXY for L with type X ↔ Y . The axioms of a relation algebra are (1) the axioms of a Boolean lattice for all relations of the same type under the Boolean operations, the inclusion, empty relation and universal relation, (2) the associativity of composition and that identity relations are neutral ele- ments with respect to composition, (3) that Q;R ⊆ S, QT ;S ⊆ R and S;RT ⊆ Q are equivalent, for all relations Q, R and S (with appropriate types), (4) that R 6= O implies L;R;L = L, for all relations R and all universal relations (with appropriate types). In [12] the laws of (3) are called the Schröder rules and (4) is called the Tarski rule. In the relation-algebraic proofs of this paper we will mention only applica- tions of (3), (4) and ‘non-obvious’ consequences of the axioms. Furthermore, we will assume that complementation and transposition bind stronger than com- position, composition binds stronger than union and intersection and that all expressions and formulae are well-typed. Furthermore, we call a relation R irreflexive if R ⊆ I, symmetric if R = RT and a mapping if R is univalent, i.e., RT ;R ⊆ I, and total, i.e., R;L = L (for more details, see e.g., [12,13]). A vector is a relation v with v = v;L. For v : X ↔ Y the condition v = v;L means that v can be written in the form v = Z × Y with a subset Z of X. Then we say that v models the subset Z of X. Since for this purpose the target of a vector is irrelevant, we use the specific singleton set 1 as target. Moreover, a point p is a vector with p;pT ⊆ I and L;p = L. In the set-theoretic case and if the point p : X ↔ Y is of the specific form p = P × Y with P ⊆ X these three conditions mean that p contains exactly one element. In the remainder we use the following point axiom of [4] which holds for set-theoretic relations, where Pv := {p | p ⊆ v ∧ p is point} for all vectors v. S Axiom 2.1 For all sets X we have LX11 = p∈PL p. X1 1 Additionally we have the following lemma which states that this property can be generalised for arbitrary vectors (see [4]). S Lemma 2.1 If v : X ↔ 1 is a vector, then v = p∈Pv p. t u 3 Cardinality of Relations In [7] Kawahara discusses the cardinality of set-theoretic relations. The main re- sult is a characterisation of the cardinalities of relations. Considering the prop- erties of this characterisation as axiomatic specification of the cardinality oper- ation | · | this leads to the following definition: Definition 3.1 For all relations R we denote its cardinality by |R|. The following axi- oms specify the meaning of the cardinality operation, where Q, R and S are arbitrary relations with appropriate types: Relational Approximation of Maximum Independent Sets 55 (C1) If R is finite, then |R| ∈ N and |R| = 0 iff R = O. (C2) |R| = |RT |. (C3) If R and S are finite, then |R ∪ S| = |R| + |S| − |R ∩ S|. (C4) If Q is univalent, then |R ∩ QT ;S| ≤ |Q;R ∩ S| and |Q ∩ S;RT | ≤ |Q;R ∩ S|. (C5) |I11 | = 1. In (C1) and (C3) the relations in question are assumed to be finite so that the cardinality |R| can be regarded as a natural number, in (C2) and (C4) the nota- tion |R| = |S| (respectively |R| ≤ |S|) is equivalent to the fact that there exists a bijection between R and S (respectively an injection from R to S) and (C5) says that the identity relation on the singleton set 1 consists of precisely one pair. Throughout this paper we assume in case of an expression |R| the sets of R’s type to be finite and thereby |R| ∈ N. Based on the above axioms in [7] a lot of laws for the cardinality operation are derived in a purely calculational manner. For example, from the axioms (C1) and (C3) we get the monotonocity of the cardinality operation, i.e., that R ⊆ S implies |R| ≤ |S|. Another fact we use in the remainder is following (see [7]): Lemma 3.1 If R : X ↔ Y is univalent and S : Y ↔ Z is a mapping, then |R;S| = |R|. t u Next, we consider the cardinality of points of type X ↔ 1 and vectors by us- ing only the mentioned cardinality axioms and the presented consequences of them. The next lemma states that a point in deed contains exactly one element. Lemma 3.2 If p : X ↔ 1 is a point, then |p| = 1. Proof. Using cardinality axioms (C2) and (C5) and Lemma 3.1 (I11 is univalent and pT : 1 ↔ X is a mapping), we have the folliwng calculation: |p| = |pT | = |I11 ;pT | = |I11 | = 1.  This lemma allows to show that the cardinality of a vector with target 1 equals the cardinality of the set of all points it contains: Lemma 3.3 For all v : X ↔ 1 we have |v| = |Pv |. Proof. Because of Lemma 2.1, cardinality axioms (C3) and (C1) (the points of Pv are pair-wise disjoint) and Lemma 3.2 we obtain the claim by [ X |v| = | p| = |p| = |Pv |.  p∈Pv p∈Pv 4 Approximation of Maximum Independent Sets In this section we use the notions and results of the previous sections to for- mally verify a relational version of the approximation algorithm of Wei for maximum independent sets (see [16]). 56 I. Stucke We assume an undirected and loop-free graph g = (X, E) to be given, where the set X of vertices is non-empty and finite. We model g by an adjacency relation R : X ↔ X, that is defined by (x, y) ∈ R iff {x, y} ∈ E, for all x, y ∈ X. Due to this definition R is irreflexive and symmetric. The relation R is taken as input for the relational program we want to show as correct. Since the approximation bound depends on the degrees of the vertices, we additionally assume that the maximum degree of g is k ∈ N. This causes to the conjunction of the following three formulae as pre-condition Pre(R, k): R⊆I R = RT k = max{|R;p| | p ∈ PLX11 } An independent set (or stable set) of g is a set of vertices S such that {x, y} ∈ / E, for all x, y ∈ S. It can be easily derived that a vector s : X ↔ 1 models an independent set with respect to the adjacency relation R iff R;s ⊆ s. We want to show that our program has approximation bound k + 1. So, the post-condition Post(R, k, s) is the conjunction of the following two formulae: R;s ⊆ s ∀ t : X ↔ 1 • R;t ⊆ t ⇒ |t| ≤ |s|(k + 1) In the remainder of this section we show that with respect to these specifications the following relational program is totally correct: s, v := O, OX11 ; while v 6= L do (W) let p = point(v); s, v := s ∪ p, v ∪ p ∪ R;p od We use the operation point that selects deterministically a point such that point(v) ⊆ v for all non-empty vectors v. The typing rules of the relational operations in combination with the initialisation of v by OX11 leads to the typing s, v, p : X ↔ 1 and also X ↔ 1 as type of the constant L of the guard of the loop. The vector v is used to collect the vertices contained in the present indepentend set, that is modeled by the vector s, and also their neighbours. In the remainder the conjunction of the following two formulae is used as loop invariant Inv(R, k, s, v): (1) (R ∩ v;v T );s ⊆ s (2) R;s ∪ s = v Here formula (1) is a generalisation of the formula R;s ⊆ s of the post-condition Post(R, k, s) and formula (2) is simply an auxiliary formula saying that v mod- els the union of the set modeled by s with its neighbours. We now prove the four proof obligations of assertion-based verification with respect to the above speficied pre- and post-condition. We start with the estab- lishment of the loop invariant by the initialisation of s and v. Lemma 4.1 If R : X ↔ X and k ∈ N with Pre(R, k), then Inv(R, k, O, O). t u We omit the trivial proof. With the next lemma we prove the maintainence of the loop invariant. Relational Approximation of Maximum Independent Sets 57 Lemma 4.2 Given R : X ↔ X, s, v : X ↔ 1 and k ∈ N such that Inv(R, k, s, v) and v 6= L, we have Inv(R, k, s ∪ p, v ∪ p ∪ R;p), for all p ∈ Pv . Proof. First, we verify that the first formula of the loop invariant holds for the T new values of s and v, i.e., that (R ∩ (v ∪ p ∪ R;p);(v ∪ p ∪ R;p) );(s ∪ p) ⊆ s ∪ p. It is easy to see that showing the following four inclusions is sufficent: T (R ∩ (v ∪ p ∪ R;p);(v ∪ p ∪ R;p) );s ⊆ s T (R ∩ (v ∪ p ∪ R;p);(v ∪ p ∪ R;p) );s ⊆ p T (R ∩ (v ∪ p ∪ R;p);(v ∪ p ∪ R;p) );p ⊆ s T (R ∩ (v ∪ p ∪ R;p);(v ∪ p ∪ R;p) );p ⊆ p. Because of (2) we have R;s ⊆ v and s ⊆ v and, moreover, because of p ⊆ v we have R;s ⊆ p and s ⊆ p. Furthermore, we get R;s ⊆ p ⇐⇒ RT ;p ⊆ s ⇐⇒ R;p ⊆ s using one of the Schröder rules in the first and the second formula of the pre- condition in the second step. With these auxiliary facts the second and third of the above inclusions follow immediately. Since the point p is injective and R is irreflexive due to the first formula of the pre-condition, we obtain R;p ⊆ p, such that the last of the above inclusions holds. Verifying the first inclusion is more comprehensive since the following three inclusions have to be proved: (R ∩ (v ∪ p ∪ R;p);v T );s ⊆ s (R ∩ (v ∪ p ∪ R;p);pT );s ⊆ s (R ∩ (v ∪ p ∪ R;p);pT ;RT );s ⊆ s We omit the proofs of these inclusions since they are very similar to these of the previous inclusions. The maintenance of the second formula of the loop invariant is easy to prove, since by using (2) we get R;(s∪p)∪(s∪p) = R;s∪R;p∪s∪p = v ∪p∪R;p. t u For the third proof obligation we verify the error-free termination of the pro- gram (W). A consequence of the guard of the loop is that each call of the partial operation point is defined. For this reason and the assumed finiteness of the set X, it suffices to show that the loop terminates, i.e., that v is strictly enlarged by each execution of the body of the loop. Lemma 4.3 If v : X ↔ 1 with v 6= L, we have v ⊂ v ∪ p ∪ R;p, for all p ∈ Pv . Proof. Since v ⊆ v ∪ p ∪ R;p holds obviously, we show v 6= v ∪ p ∪ R;p by contradiction. We start with v = v ∪ p ∪ R;p ⇐⇒ p ∪ R;p ⊆ v =⇒ p ⊆ v. The last inclusion and the assumption p ⊆ v imply p = O, but this contradicts the fact that points are non-empty. t u 58 I. Stucke Finally, we consider the last proof obligation, i.e., that if v = L holds, then the loop invariant implies the post-condition. Therefore, we also need the pre- condition, in particular the maximum-degree condition, for the proof. Lemma 4.4 Given R : X ↔ X, k ∈ N and s, v : X ↔ 1 such that Pre(R, k), v = L and Inv(R, k, s, v), we have Post(R, k, s). Proof. Formula (1) of the loop invariant Inv(R, k, s, v) and v = L yield R;s ⊆ s, which is the first formula of Post(R, k, s). To verify the second formula of Post(R, k, s), let t : X ↔ 1 be an arbitrary vector such that R;t ⊆ t. Then we can calculate as follows: |t| ≤ |LX11 | t : X ↔ 1 , monotonicity cardinality = |v| since v = LX11 = |R;s ∪ s| formula (2) of Inv(R, k, s, v) ≤ |R;s| S + |s| cardinality axiom (C3) = |R; p∈Ps p| + |s| by Lemma 2.1 S = |s| + | p∈Ps R;p| P ≤ |s| + p∈Ps |R;p| Ps finite, cardinality axiom (C3) P ≤ |s| + p∈Ps k second formula of Pre(R, k) = |s| + k|s| by Lemma 3.3 = (k + 1)|s|  5 Conclusion and Future Work By modelling graphs via adjacency relations we developed a relational pro- gram based on Wei’s algorithm for approximating maximum independent sets in graphs. Therefore, we used vectors and points to model subsets of the ver- tices. Based on Kawahara’s characterisation of the cardinality of relations and further consequences of it we were able to prove facts about their cardinality. In the following, we proved the correctness of the developed program by classical reasoning about the specified pre- and postconditions and loop-invariant. Es- pecially the approximation bound was proved in a purely calculational manner by using Kawahara’s and our results about the cardinality of relations. As future work we plan an exhaustive investigation of the cardinatily op- eration. We hope to come upon useful laws which can be applied, for exam- ple, in the context of correctness proofs of further approximation algorithms. Due to the positive experiences we gained with theorem prover with regard to program verification, we plan an embedding of the cardinality operation in existing libraries for relation algebra as for Isabelle/HOL (see [1]) or Coq (see [10]). Acknowledgement. I thank P. Höfner and, in particular, R. Berghammer for drawing my attention to this particular research topic and valuable discussions and comments. Relational Approximation of Maximum Independent Sets 59 References 1. Armstrong, A., Foster, S., Struth, G., Weber, T.: Relation algebra. Archive of Formal Proofs, 2014. http://afp.sf.net/entries/Relation_Algebra.shtml 2. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to algorithms. The MIT Press (1990) 3. Francez, N.: Program verification. Addison-Wesley (1992) 4. Furusawa, H.: Algebraic formalisations of fuzzy relations and their representation theorems. Ph.D. thesis, Department of Informatics, Kyushu University (1998) 5. Gries, D.: The science of programming. Springer (1981) 6. Höfner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning. LNAI, vol. 5195, pp. 50- 66. Springer (2008) 7. Kawahara, Y.: On the cardinality of relations. In: Schmidt, R.A. (ed.): Relations and Kleene Algebra in Computer Science. LNCS, vol. 4136, pp. 251-265. Springer (2006) 8. Maddux, R.: Relation algebras. In: Brink, C., Kahl, W., Schmidt, G. (eds.): Relational Methods in Computer Science. Advances in Computing Science, pp. 22-38. Springer (1997) 9. Maddux, R.: Relation algebras. Studies in Logic and the Foundations of Mathemat- ics, vol. 150. Elsevier (2006) 10. Pous, D.: Relation algebra and KAT in Coq. http://perso.ens-lyon.fr/damien.pous/ra/ 11. Schmidt, G., Ströhlein, T.: Relation algebras: Concept of points and representability. Discrete Mathematics 34, 83-97 (1985) 12. Schmidt, G., Ströhlein, T.: Relations and graphs, Discrete mathematics for computer scientists, EATCS Monographs on Theoretical Computer Science. Springer (1993) 13. Schmidt, G.: Relational mathematics. Encyclopedia of Mathematics and its Applica- tions, vol. 132. Cambridge University Press (2010) 14. Tarski, A.: On the calculus of relations. Journal of Symbolic Logic 6, 73-89 (1941) 15. Tarski, A., Givant, S.: A formalization of set theory without variables. Colloquium Publications 41, American Mathematical Society (1987) 16. Wei, V.K.: A lower bound for the stability number of a simple graph. Bell Lab. Tech. Memor. 81-11217-9 (1981)