Correctness of the Algorithm

Preliminaries

To frame the problem of correctness of the constraint solving algorithm precisely, we must make more precise the notions of well-constrained, overconstrained and underconstrained constraint systems. As discussed in the section on constraint assignment, each geometric element in the constraint problems we consider has two degrees of freedom. Each constraint in the problem eliminates one of these, thus if there are no fixed geometries in the problem, we expect that
| E | = 2 | V | - 3
where | E | is the number of edges and | V | is the number of nodes in the corresponding constraint graph. Note that the solution will be a rigid body with three remaining degrees of freedom, because the constraints determine only the relative position of the geometric elements.

The intuitive notions of well-constrained, overconstrained and underconstrained can be made technically precise as follows:

Definition 1
A graph with n nodes is structurally overconstrained if there is an induced subgraph with m < n nodes and more than 2 m - 3 edges.
Definition 2
A graph with n nodes is structurally underconstrained if it is not overconstrained, and the number of edges is less than 2 n - 3.
Definition 3
A graph with n node is structurally well-constrained if it is not overconstrained, and the number of edges is equal to 2 n - 3.
For an algorithm to test whether a graph is structurally well-constrained see, e.g.,[46], [102]. Note also that a structurally well-constrained graph can be overconstrained in a geometric sense, for example if there are three lines with pairwise angle constraints.

Problem Formulation

We are given a constraint graph G = (V, E) whose nodes V are the geometric elements of the sketch, and whose edges E are the constraints between geometries. Note that the geometric elements are reduced to points and lines, and the constraints to those of distance and angle, as discussed elsewhere. For now, we restrict to geometric constraint problems in which no two lines are constrained to be parallel. This restriction simplifies the correctness proof but is not essential to it.

We consider sets C whose elements are sets S that in turn have as elements nodes of G. Each set S is a cluster of the constraint problem. Initially, we form a set CG from G. For each edge e = (u, v) in G, there is a cluster Se = {u, v}. The construction steps that solve the constraint problem amount to one reduction step that merges three clusters whose pairwise intersection is a singleton. The reduction is denoted by ->, where we sometimes indicate with postscripts which clusters are to be merged.

In this section, we consider clusters as sets and study their structure under reduction. We prove first a weak notion of correctness:

If the constraint graph is not structurally overconstrained, then our algorithm reduces the initial set CG to a singleton, no matter in which order the reduction steps are applied. That is, the set CG and the reduction -> are a terminating, confluent rewriting system.
Notice, however, that a well-constrained geometric problem has in general several incongruent solution [7]. We prove therefore a stronger uniqueness theorem in the next section:
If the constraint graph is well-constrained and our algorithm reduces the initial set CG to a single cluster using, in the construction phase, the placement rules given before, then the solutions derived by different reduction sequences place a fixed set of triples of geometric elements in the same relative position.
This result implies that different reduction sequences must produce geometric solutions that are congruent.

Termination and Uniqueness of Normal Forms

Given the constraint graph G = (V, E) , we consider the set of clusters
CG = { {u, v} : (u, v) is in E}
Cluster sets are rewritten using a reduction ->. The reduction -> is formally defined as follows:
Definition 4
Let C be a set of clusters in which there are three clusters S1, S2, and S3 such that
        S1 ^ S2 = {g1}   
        S2 ^ S3 = {g2}  
        S3 ^ S1 = {g3} 
where ^ is set intersection. Then
        C ->  C'= { C U { S1 U S2 U S3}} \ { S1, S2, S3 }
where U is set union.
We will show that the reduction system (CG, ->) has a unique normal form that is obtained after finitely many reductions.
Definition 5
The set C' of clusters is derived from C, if C' can be obtained by applying a sequence t of reductions to C. We denote this by C ->* C'.
Definition 6
A set of clusters C to which -> is not applicable is called irreducible. If C' can be derived from C, then C' is called a normal form of C.
We will show that the initial cluster set CG obtained from a constraint graph that is not structurally overconstrained has a unique normal form, and that this normal form is derived by a finite sequence of reduction steps.

Lemma 1
If CG is obtained from a constraint graph with n nodes and e edges, then every reduction sequence t has length less than (e + 1) / 2.
Proof: CG has initially e clusters. Each reduction step reduces the number of clusters by 2.
Lemma 2
Let G be a constraint graph. If CG ->* C, then the subgraph that corresponds to a cluster in C is structurally well-constrained.
Proof: The proof is by induction on the length of the reduction sequence deriving C. The induction basis is C = CG and is trivial. For the induction step, consider the last reduction step which merges three clusters S1, S2, and S3 into a new cluster S. Let GS be the subgraph of G corresponding to S, Gk the subgraph of G corresponding to Sk, k = 1, 2, 3. Note that these graphs are not necessarily induced subgraphs of G, and that the edge sets of the Gk are disjoint.

Let ni be the number of nodes and ei the number of edges in the subgraph of G induced by Si. From the induction hypothesis, ei = 2 ni - 3. Since | S1 ^ S2 | = | S1 ^ S3 | = | S2 ^ S3 | = 1, S has n = n1 + n2 + n3 - 3 vertices. Then e1 + e2 + e3 = 2 n - 3.

Lemma 3
Let CG ->* C. If the clusters S1 and S2 in C intersect in more than one node then Gis structurally overconstrained.
Proof: Assume | S1 ^ S2 | = m > 1 and that G1 and G2 are the corresponding subgraphs of S1 and S2. By Lemma 2, e1 = 2 n1 - 3 and e2 = 2 n2 - 3. Consider the subgraph G0 induced by S1 U S2. G0 has n0 = n1 + n2 - m vertices and e0 >= e1 + e2 edges. But e0 >= e1 + e2 = 2 ( n1 + n2 ) - 6 > 2 n0 - 3. Therefore, G is structurally overconstrained.
Theorem 4
If the original constraint graph is not structurally overconstrained, then the reduction system (C, ->) is confluent, where CG ->* C.
Proof: Let C be a set of clusters, CG ->* C. Assume there are two different reductions possible, C ->1 C1 and C ->2 C2 It suffices to show that then C1 ->2 C3 and C2 ->1 C3. The reduction ->1 involves the clusters S11, S12, and S13, and the reduction ->2 involves the clusters S21, S22, and S23. Several cases must be distinguished based on how many distinct clusters there are among the clusters Sik.

3 clusters:

Since there are only three distinct clusters, and since the reductions are different, there must be two clusters that have more than one element in common. Thus the constraint graph is overconstrained.

4 clusters:

Since each reduction requires three distinct clusters, the cluster not used in the reduction ->1 must connect two of the clusters S11, S12, and S13. But then C1 contains two distinct clusters whose intersection is larger than one element. Hence the original graph is overconstrained. By symmetry, using ->2 similarly certifies an overconstrained.

5 clusters:

Let S11 = S21 and assume that S11 ^ S12 = { g1} and S11 ^ S13 = { g2} . Clearly S22 and S23 intersect S11 in singletons. If S22 and S23 are both disjoint from S12 U S13 \ {g1, g2}, then it is clear that C1 ->2 C3 and C2 ->1 C3. But if (S22 U S23) ^ (S12 U S13 \ {g1, g2}) is not empty, then C1 and C2 must contain two clusters that share more than one common element, contradicting that the original is not overconstrained.

6 clusters:

Since the clusters are all distinct, the reductions ->1 and ->2 commute.

Corollary 5
If the constraint graph G is not overconstrained, then the reduction system (C, ->) has a unique normal form that is obtained by finitely many reduction steps.
Proof: Immediate from Lemma 1 and Theorem 4.

Theory