=Paper=
{{Paper
|id=Vol-1454/ramics15-st_53-60
|storemode=property
|title=Relational Approximation of Maximum Independent Sets
|pdfUrl=https://ceur-ws.org/Vol-1454/ramics15-st_53-60.pdf
|volume=Vol-1454
}}
==Relational Approximation of Maximum Independent Sets==
https://ceur-ws.org/Vol-1454/ramics15-st_53-60.pdf
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)