kk-Equivalence Relations and Associated Algorithms

1 Introduction

Lines and circles pose significant scalability challenges in synthetic geometry. A line with $n$ points implies ${n\choose 3}$ collinearity atoms coll, or alternatively, when lines are represented as functions, equality among ${n\choose 2}$ different lines. Similarly, a circle with $n$ points implies ${n\choose 4}$ cocyclicity atoms cycl, or equality among ${n\choose 3}$ circumcircles. Although geometry problem statements may not contain any lines or circles with more than a few points on them, synthetic provers need to introduce auxiliary points, and doing so may result in lines and circles with dozens if not hundreds of points on them. To support efficient reasoning in the presence of a large number of auxiliary points, we introduce a new mathematical concept of $k$ -equivalence relations, which generalizes equality ( $k=1$ ) to include both lines ( $k=2$ ) and circles ( $k=3$ ), and present an efficient, proof-producing procedure to compute the closure of a $k$ -equivalence relation that uses exponentially less space (in $k$ ) than the naïve procedure.

2 $k$ -Equivalence Relations

A binary relation $R$ is an equivalence relation provided it satisfies the following three laws:

Reflexivity	$\forall a.R(a,a)$
Symmetry	$\forall ab.R(a,b)\implies R(b,a)$
Transitivity	$\forall abc.R(a,b)\wedge R(a,c)\implies R(b,c)$

In synthetic geometry, the ternary relation $\mathsf{coll}$ representing collinearity satisfies similar laws:

Sub-reflexivity	$\forall abc.\neg\mathrm{distinct}(a,b,c)\implies\mathsf{coll}(a,b,c)$
p Perm-invariance	$\forall abc.\mathsf{coll}(a,b,c)\implies\forall\pi.\mathrm{perm}(\pi)\implies\mathsf{coll}(\pi(a),\pi(b),\pi(c))$
2-transitivity	$\forall abcd.\mathsf{coll}(a,b,c)\wedge\mathsf{coll}(a,b,d)\wedge a\neq b\implies\mathsf{coll}(b,c,d)$

as does the quaternary relation $\mathsf{cycl}$ representing cocyclicity:

Sub-reflexivity	$\forall abcd.\neg\mathrm{distinct}(a,b,c,d)\implies\mathsf{cycl}(a,b,c,d)$
Perm-invariance	$\forall abcd.\mathsf{cycl}(a,b,c,d)\implies\forall\pi.\mathrm{perm}(\pi)\implies\mathsf{cycl}(\pi(a),\pi(b),\pi(c),\pi(d))$
3-transitivity	$\forall abcde.\mathsf{cycl}(a,b,c,d)\wedge\mathsf{cycl}(a,b,c,e)\wedge\mathrm{distinct}(a,b,c)\implies\mathsf{cycl}(b,c,d,e)$

This pattern leads us to a natural generalization of equivalence relations that we call $k$ -equivalence relations.

Definition 1 ( $k$ -Equivalence Relation).

We say a $(k+1)$ -ary relation $R$ is a $k$ -equivalence relation provided it satisfies the following laws:

Sub-reflexivity	$\forall x_{1}\dotsm x_{k+1}.\neg\mathrm{distinct}(\vec{x})\implies R(\vec{x})$
Perm-invariance	$\forall x_{1}\dotsm x_{k+1}\pi.R(\vec{x})\wedge\mathrm{perm}(\pi)\implies R(\pi(\vec{x}))$
$k$ -transitivity	$\forall x_{1}\dots x_{k}y_{1}y_{2}.R(\vec{x},y_{1})\wedge R(\vec{x},y_{2})\wedge\mathrm{distinct}(\vec{x})\implies R(\vec{x}_{2:},y_{1},y_{2})$

3 Basic Properties

The key property of $k$ -equivalence relations that we exploit in our algorithms is that they can be represented compactly in terms of finite sets.

Definition 2 ( $k$ -predicate).

Let $R$ be a $k$ -equivalence relation. Define its $k$ -predicate $\Phi_{R}$ as follows: for any finite set $X$ ,

\Phi_{R}(X)\coloneqq\bigwedge_{x\subseteq X,|x|=k+1}R(\vec{x})

Definition 3 ( $k$ -predicate laws).

The following laws follow from Definition 1 and Definition 2:

Sub-reflexivity	$\forall x,\|x\|\leq k\implies\Phi_{R}(x)$
$k$ -transitivity	$\forall x\forall y,\Phi_{R}(x)\wedge\Phi_{R}(y)\wedge\|x\cap y\|\geq k\implies\Phi(x\cup y)$
Projection	$\forall xy,\Phi_{R}(x)\wedge y\subseteq x\implies\Phi_{R}(y)$

Definition 4 ( $k$ -function).

A $k$ -predicate $\Phi_{R}$ induces a $k$ -function $\phi_{R}$ on sets of size $k$ as follows:

\phi_{R}(x)\coloneqq\{y:\Phi_{R}(x\cup y)\}

Example 1.

Note that $\phi_{\mathsf{coll}}(\{a,b\})$ is the set of points collinear with $\{a,b\}$ , i.e. the line through $a$ and $b$ . Similarly, $\phi_{\mathsf{cycl}}(\{a,b,c\})$ is the set of points cocyclic with $\{a,b,c\}$ , i.e. the circumcircle of $a,b,c$ .

Lemma 1.

Let $x_{1},x_{2}$ be two sets of size $k$ . Then

\phi_{R}(x_{1})=\phi_{R}(x_{2})\iff\Phi_{R}(x_{1}\cup x_{2})

Proof.

First suppose $\{y:\Phi_{R}(x_{1}\cup y)\}=\{y:\Phi_{R}(x_{2}\cup y)\}$ . Then $x_{2}$ is in the second set by subreflexivity so it must be in the first set, which yields $\Phi_{R}(x_{1}\cup x_{2})$ . Now suppose $\Phi_{R}(x_{1}\cup x_{2})$ , and let $y$ be such that $\Phi_{R}(x_{1}\cup y)$ . Since $x_{1}\cup y$ and $x_{1}\cup x_{2}$ overlap at $x_{1}$ of size $k$ , it follows by $k$ -transitivity that $\Phi_{R}(x_{1}\cup x_{2}\cup y)$ , and by projection that $\Phi_{R}(x_{2}\cup y)$ . ∎

4 Deciding $k$ -Equivalence Relations

It is well known that a traditional equivalence relation defines a partition, which can be represented as a set of disjoint sets and computed using e.g. the union-find algorithm [2]. Similarly, a $k$ -equivalence relation can be represented as a set of sets whose pairwise intersections are less than $k$ . When $k=1$ , the sets must be disjoint, but this is not the case for higher values of $k$ . For example, a point $A$ in the plane may be collinear with two points $B_{1}$ and $C_{1}$ , and also with two points $B_{2}$ and $C_{2}$ , but this does not imply that the five points are all collinear.

4.1 Procedure

Fix a $k$ -equivalence relation $R$ , and consider a sequence $H_{i}$ of $R$ -atoms over a set of distinct terms $x_{i}$ (we relax the assumption of distinctness in Section 4.4). We are interested in determining, for a given $R$ -atom $R(y_{1},\dotsc,y_{k+1})$ , whether or not $\bigwedge_{i}H_{i}\implies R(y_{1},\dotsc,y_{k+1})$ . The main idea of our procedure is to reason using the $k$ -predicate $\Phi_{R}$ , and to saturate with the rules from Definition 3 rather than those of Definition 1. Our procedure produces proofs using the following constructors:

1.

assume(<hypothesis-idx>)
2.

subrefl(<terms>)
3.

trans(<pf1>, <pf2>)
4.

project(<pf>, <terms>)

where the latter three correspond to the laws of Definition 3. Define a $k$ -set $s$ to be a set representing the fact $\Phi_{R}(s)$ . Our procedure maintains three datastructures:

1.

ksets: an array of $k$ -sets. Note that we store the entire history of $k$ -sets to facilitate proof production but only some $k$ -sets are considered active.
2.

proofs: an array of proofs, one for each $k$ -set.
3.

term2parents: a map from terms to the IDs of the active ksets that contain it.

Figure 1 shows pseudocode for the procedure. We first initialize ksets, proofs, and term2parents to empty (L2). We then iterate over the hypotheses in sequence (L3). For the $i$ th hypothesis R(xs), we first create a new $k$ -set for it using New (L4), which involves appending new entries to ksets and proofs and updating the term2parents datastructure (L14). At this point, the new $k$ -set may overlap one or more existing $k$ -sets by $k$ elements. Thus, we need to detect these overlaps and merge $k$ -sets as necessary. We accomplish by calling FindMerges on the newly created $k$ -set (L5). To find the necessary merges, we compute the $k$ -sets that overlap at least $k$ with the newly created $k$ -set by first multiset-unioning the parents of the new $k$ -set (L17) and then filtering the parents that occur atleast $k$ times (L18). If there are no such $k$ -sets (besides the new one), there is nothing to do (L19). Otherwise we fold over the filtered $k$ -sets, merging them (with Merge) in sequence into one big $k$ -set (L21). The procedure Merge simply deactivates the old $k$ -sets by removing them from term2parents (L24-25) and then creates new $k$ -set with the union of the two old $k$ -sets (L26). Note that once the matches have been merged into one big $k$ -set, this new $k$ -set may overlap atleast $k$ with another active $k$ -set; thus we must recursively find the merges of the new $k$ -set (L22). Finally, to answer the query R(xs), we intersect the parents of the elements of xs (L7); if the result is empty the query is not entailed (L8), otherwise we call explain to produce a proof of the query, which we discuss in Section 4.3. Note that we can easily extend KDecide to support arbitrary-sized queries by first checking if the query R(xs) has size $\leq k$ and if so returning subrefl(xs).

1:procedure KDecide(hyps, query)

2: ksets, proofs, term2parents

\leftarrow

{}, {}, {}

3: for i,

R

(xs) in hyps do

4: n

\leftarrow

New(xs, assume(i))

5: FindMerges(n)

6:

R

(xs)

\leftarrow

query

7: matches

\leftarrow

intersect parents of xs

8: if matches.isEmpty then return not-entailed

9: else return explain(matches[0], xs)

10:procedure New(xs, proof)

11: n

\leftarrow

ksets.size()

12: ksets.append(xs)

13: proofs.append(proof)

14: for x in xs do term2parent[x].insert(n)

15: return n

16:procedure FindMerges(n)

17: allParents

\leftarrow

multiset union of the parents of ksets[n]

18: matches

\leftarrow

subset of allParents that appear at least

k

times

19: if |matches| < 2 then return

20: last

\leftarrow

matches[0]

21: for

i

= 1 to length(matches)-1 do last

\leftarrow

Merge(last, matches[i])

22: FindMerges(last)

23:procedure Merge(i1, i2)

24: for x in ksets[i1] do term2parent[x].remove(i1)

25: for x in ksets[i2] do term2parent[x].remove(i2)

26: return New(union(ksets[i1], ksets[i2]), trans(i1,i2))

Figure 1: Deciding

k

-equivalence relations.

4.2 Example

We provide more intuition for our procedure by walking through the following small example ( $k=2$ ):

R(a,b,c)\wedge R(c,d,e)\wedge R(e,f,g)\wedge R(a,d,g)\wedge R(b,c,d)

The final state of the procedure is shown in Table 1. None of the first four hypotheses trigger any merges. The fifth hypothesis (H4) matches with both H0 and H1, producing the $k$ -set $\{a,b,c,d,e\}$ . This $k$ -set then (recursively) matches with H3 yielding $\{a,b,c,d,e,g\}$ which (recusively) matches with H2, yielding a singleton $k$ -set containing the union of all original hypotheses.

KSet Index	Active	Proof	Terms
0	0	assume(H0)	a, b, c
1	0	assume(H1)	c, d, e
2	0	assume(H2)	e, f, g
3	0	assume(H3)	a, d, g
4	0	assume(H4)	b, c, d
5	0	trans(0, 4)	a, b, c, d
6	0	trans(1, 5)	a, b, c, d, e
7	0	trans(3, 6)	a, b, c, d, e, g
8	1	trans(2, 7)	a, b, c, d, e, f, g

Table 1: The state of the procedure after asserting the hypotheses in the example problem of Section 4.2 given by

R(a,b,c)\wedge R(c,d,e)\wedge R(e,f,g)\wedge R(a,d,g)\wedge R(b,c,d)

.

4.3 Producing proofs

Suppose for a given query $R(\vec{x})$ , we find a $k$ -set $y$ containing $\vec{x}$ . We can easily produce a proof of $R(\vec{x})$ by simply projecting the proof of $\Phi_{R}(y)$ stored in the proofs array with the project proof constructor corresponding to the project rule in Definition 3. However, this proof may be extremely suboptimal in general. We take inspiration from [3] and provide an Explain operation that produces a proof of the query using a minimal subset of the hypotheses.

Figure 2 contains pseudocode for the Explain procedure, which is called on the index $n$ of the $k$ -set that contains the query, along with the terms in the query. The procedure rests on two key insights. First, if we want to produce a proof of xs from a $k$ -set constructed from a merge, and if one of the merged $k$ -sets s1 already contains xs, then we can produce a proof directly from s1 without considering s2 (L4-5). Second, even if xs is not contained in either s1 or s2, we still do not need to produce proofs of s1 and s2 in their entirety; if we can produce child proofs of union(inter(s1, s2), inter(s1, xs)) and union(inter(s1, s2), inter(s2, xs)) respectively, we can glue them together with $k$ -transitivity to produce a proof of a set containing xs, from which we can project a proof of xs.

1:procedure Explain(n, xs)

2: if histories[n] = assume(i) then return assume(i)

3: else if histories[n] = merge(i1, i2) then

4: if xs

\subseteq

ksets[i1] then return Explain(i1, xs)

5: else if xs

\subseteq

ksets[i2] then return Explain(i2, xs)

6: else

7: anchor

\leftarrow

ksets[i1]

\cap

ksets[i2]

8: pf1

\leftarrow

Explain(i1, anchor

\cup

(ksets[i1]

\cap

xs))

9: pf2

\leftarrow

Explain(i2, anchor

\cup

(ksets[i2]

\cap

xs))

10: return project(trans(pf1, pf2), xs)

Figure 2: Producing compact proofs.

Example.

Suppose that after asserting the hypotheses of Section 4.2 we queried Explain(8, {a, b, d}). Explain will take the branch in L5 three consecutive times and finally return the minimal proof project(trans(assume(H0), assume(H4)), {a, b, d}).

4.4 Terms that may not be distinct

We now show how to lift the simplifying assumption of 4.1 that each of the terms that appeared in the $k$ -equivalence relation are known to be distinct. Suppose that rather than assuming that every term is distinct, we assume that we have a partition $\sigma$ on terms such that two terms in different equivalence classes $\gamma$ are known to be distinct. In geometry solvers, it is common to use numericals diagrams to determine acceptable distinctness conditions to assume, in which case such a partition can be determined by rounding the coordinates of each (possibly equal) point to a given precision. To support this scenario, it suffices to tweak L17 by first set-unioning the parents within each equivalence class before multiset-unioning the results. This will compute the set of $k$ -sets that overlap with the new $k$ -set at atleast $k$ points that are known to be distinct.

4.5 Asymptotics

Let $n$ be the number of hypotheses and $m$ the maximum number of parents of any term at any time during the procedure.

Lemma 2.

There can only ever be as many as $n$ active $k$ -sets.

Proof.

Only processing a new hypothesis increases the number of active $k$ -sets; all other calls to New are during merges, which first deactivate two $k$ -sets and so decrease the number of active $k$ -sets by one. ∎

Lemma 3.

$m=O(n)$

Lemma 4.

There can be at most $n-1=O(n)$ merges.

Lemma 5.

FindMerges is called at most $2n=O(n)$ times.

Lemma 6.

The largest size of any $k$ -set is $k+n$ .

Proof.

Any $k$ -set must be the union of some $n_{0}$ -element subset of the set of the $n$ original $k+1$ -element $k$ -sets corresponding to the hypotheses. For these $n_{0}$ $k$ -sets to be merged into one, they all must overlap $k$ with their union; thus the union can have at most $n_{0}+k$ elements. The result follows from $n_{0}\leq n$ . ∎

Lemma 7.

The cumulative execution of time of L17 is at most $2n(k+n)m=O(knm+n^{2}m)$ time.

Lemma 8.

The cumulative execution time of L14, L24, L25, L26 are all bounded by $O(n(k+n))$ .

Theorem 4.1 (Worst-Case Upper Bound).

The worst-case running time of KDecide(hyps, query) is $O\left(kmn+n^{2}m\right)$ . Since $m=O(n)$ , this simplifies to $O\left(kn^{2}+n^{3}\right)$ .

Corollary 1.

The worst-case running time is linear in $k$ , whereas the naïve implementation is exponential in $k$ .

4.6 Integrating with congruence closure

It is relatively straightforward to integrate the decision procedure of Section 4.1 into a congruence closure procedure. Suppose we have a sequence of equalities and $R$ -atoms for various $k$ -equivalence relations, and for simplicity assume that no equalities among $k$ -functions are provided explicitly. For a given $k$ -equivalence relation, we can represent the entailed $R$ -atoms compactly using $k$ -sets, where each $k$ -set also stores its canonical $k$ -function application. Whenever two equivalence classes are merged, in addition to the standard congruence closure bookkeeping, we traverse all $k$ -sets that include any member of the smaller class. For each one, we replace all terms with their new representatives and call New on the result. Whenever two $k$ -sets are merged, we also merge the $E$ -classes of their canonical $k$ -function applications.

5 Related Work

In [1], both lines and circles are represented using lists of points, and the corresponding permutation and transitivity rules are claimed to be built-in to the solver; however, few details are provided about how these rules are propagated. Equivalence relations have previously been generalized to ternary equivalence relations [4], which include collinearity but does not generalize to cocyclicity. The concept of $E$ -sequences [5] is related to our notion of $k$ -equivalence relation as follows: a $(k+1)$ -ary relation $R$ is a $k$ -equivalence relation if and only if the sequence of relations $(\mathrm{notDistinct}_{2},\dotsc,\mathrm{notDistinct_{k}},R)$ forms an $E$ -sequence.

Acknowledgments

We thank Nikolaj Bjørner for detailed discussions.

$k$ -Equivalence Relations and Associated Algorithms

Abstract

1 Introduction

2 $k$ -Equivalence Relations

Definition 1 ( $k$ -Equivalence Relation).

3 Basic Properties

Definition 2 ( $k$ -predicate).

Definition 3 ( $k$ -predicate laws).

Definition 4 ( $k$ -function).

Example 1.

Lemma 1.

Proof.

4 Deciding $k$ -Equivalence Relations

4.1 Procedure

4.2 Example

4.3 Producing proofs

Example.

4.4 Terms that may not be distinct

4.5 Asymptotics

Lemma 2.

Proof.

Lemma 3.

Lemma 4.

Lemma 5.

Lemma 6.

Proof.

Lemma 7.

Lemma 8.

Theorem 4.1 (Worst-Case Upper Bound).

Corollary 1.

4.6 Integrating with congruence closure

5 Related Work

Acknowledgments

References

kk-Equivalence Relations and Associated Algorithms

Abstract

1 Introduction

2 kk-Equivalence Relations

Definition 1 (kk-Equivalence Relation).

3 Basic Properties

Definition 2 (kk-predicate).

Definition 3 (kk-predicate laws).

Definition 4 (kk-function).

Example 1.

Lemma 1.

Proof.

4 Deciding kk-Equivalence Relations

4.1 Procedure

4.2 Example

4.3 Producing proofs

Example.

4.4 Terms that may not be distinct

4.5 Asymptotics

Lemma 2.

Proof.

Lemma 3.

Lemma 4.

Lemma 5.

Lemma 6.

Proof.

Lemma 7.

Lemma 8.

Theorem 4.1 (Worst-Case Upper Bound).

Corollary 1.

4.6 Integrating with congruence closure

5 Related Work

Acknowledgments

References

$k$ -Equivalence Relations and Associated Algorithms

2 $k$ -Equivalence Relations

Definition 1 ( $k$ -Equivalence Relation).

Definition 2 ( $k$ -predicate).

Definition 3 ( $k$ -predicate laws).

Definition 4 ( $k$ -function).

4 Deciding $k$ -Equivalence Relations