diff --git a/ITP/geometry.tex b/ITP/geometry.tex index f185c62..50b7276 100644 --- a/ITP/geometry.tex +++ b/ITP/geometry.tex @@ -12,11 +12,13 @@ def ConvexIndep (S : Set Point) : Prop := ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a}) +/-- `ConvexEmptyIn S P' means that `S' forms a convex empty polygon in `P' -/ def ConvexEmptyIn (S P : Set Point) : Prop := ConvexIndep S ∧ EmptyShapeIn S P -def HasEmptyKGon (k : Nat) (S : Set Point) : Prop := - ∃ s : Finset Point, s.card = k ∧ ↑s ⊆ S ∧ ConvexEmptyIn s S +/-- `HasEmptyKGon k P' means that `P' has a convex, empty `k'-gon -/ +def HasEmptyKGon (k : Nat) (P : Set Point) : Prop := + ∃ S : Finset Point, S.card = k ∧ ↑S ⊆ P ∧ ConvexEmptyIn S P \end{lstlisting} Let \lstinline|SetInGenPos| be a predicate that states that a set of points is in \emph{general position}, i.e., no three points lie on a common line (made precise in~\Cref{sec:triple-orientations}). @@ -24,7 +26,7 @@ \begin{lstlisting} theorem hole_6_theorem : ∀ (pts : Finset Point), - Point.SetInGenPos pts → pts.card = 30 → HasEmptyKGon 6 pts + SetInGenPos pts → pts.card = 30 → HasEmptyKGon 6 pts \end{lstlisting} At the root of the encoding of Heule and Scheucher is the idea that diff --git a/ITP/intro.tex b/ITP/intro.tex index 77a29c4..98b91db 100644 --- a/ITP/intro.tex +++ b/ITP/intro.tex @@ -89,7 +89,7 @@ In the 1930s, Erd\H{o}s and Szekeres, inspired by Esther Klein, showed that for any $k \geq 3$, one can find a sufficiently large number $n$ -such that every $n$ points in \emph{general position} +such that every $n$ points in the plane in \emph{general position} (i.e., with no three points collinear) contain a convex \emph{$k$-gon}, i.e., a convex polygon with $k$ vertices~\cite{35erdos_combinatorial_problem_geometry}. The minimal such $n$ is denoted $g(k)$. diff --git a/ITP/related-work.tex b/ITP/related-work.tex index 8e7448c..c8f1301 100644 --- a/ITP/related-work.tex +++ b/ITP/related-work.tex @@ -13,7 +13,7 @@ Rather than devise a new SAT encoding, we use essentially the same encoding presented by Heule and Scheucher~\cite{emptyHexagonNumber}. Interestingly, -a (verified) proof of $g(6) \leq 17$ can be obtained +a formal proof of $g(6) \leq 17$ can be obtained as a corollary of our development. We can assert the hole variables $\hvar_{a,b,c}$ as true while leaving the remainder of the encoding in~\Cref{fig:full-encoding} unchanged, @@ -29,8 +29,8 @@ We checked this formula to be unsatisfiable for $n = 17$, giving the same result as Marić: \begin{lstlisting} -theorem gon_6_theorem (pts : List Point) (gp : ListInGenPos pts) - (h : pts.length ≥ 17) : HasConvexKGon 6 pts.toFinset +theorem gon_6_theorem : ∀ (pts : Finset Point), + SetInGenPos pts → pts.card = 17 → HasConvexKGon 6 pts \end{lstlisting} Since both formalizations can be executed, diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex index 20e886f..6a0cf28 100644 --- a/ITP/symmetry-breaking.tex +++ b/ITP/symmetry-breaking.tex @@ -30,16 +30,20 @@ \input{fig-sigma-equiv} Third, the lex-order property breaks symmetry due to \emph{reflection}. -Reflecting a set of points~$S$ through a line (e.g., with the map $(x, y) \mapsto (-x, y)$) +Reflecting a set of points~$S$ over a line (e.g., with the map $(x, y) \mapsto (-x, y)$) preserves the presence of $k$-holes and convex $k$-gons. -Such reflected point sets are almost $\sigma$-equivalent to $S$, -but their orientations have all changed sign. -Consider the point sets in \Cref{fig:sigma-equiv}. -As a result, -we included the \emph{parity} flag in our Lean definition of $\sigma$-equivalence -to capture changes in orientations due to reflection, -where \lstinline|parity := true| changes sign of all orientations. -The lex-order property ensures that the point set is the lexicographically-larger reflection. +This operation does not quite preserve orientations, but rather flips them +(clockwise orientations become counterclockwise and vice versa). +Our definition of $\sigma$-equivalence includes a \emph{parity} flag for this purpose: +\lstinline|parity := false| corresponds to the case that orientations are the same, +and \lstinline|parity := true| corresponds to the case that all orientations have been flipped. +See the point sets in \Cref{fig:sigma-equiv} for an example. + +The lex-order property, then, picks between a set of points and its reflection over \(x=0\). +The vector of consecutive orientations from the middle to the left +is assumed to be at least as big as the vector of consecutive orientations from the middle to the right. +This constraint is not geometrically meaningful, +but is easy to implement in the SAT encoding. We prove that there always exists a $\sigma$-equivalent point set in canonical position. @@ -54,14 +58,33 @@ \begin{proof}[Proof Sketch] -The proof proceeds in 6 steps, illustrated in~\Cref{fig:symmetry-breaking}. In each of the steps, we will construct a new list of points that is $\sigma$-equivalent to the previous one, and the last one will be in canonical position.\footnote{Even though we defined $\sigma$-equivalence for sets of points, our formalization goes back and forth between sets and lists. Given that symmetry breaking distinguishes between the order of the points e.g., $x$-order, this proof proceeds over lists. All permutations of a list are immediately $\sigma$-equivalent.} -The main justification for each step is that, given that the function $\sigma$ is defined as a sign of the determinant, applying transformations that preserve (or, when \lstinline|parity := true|, uniformly reverse) the sign of the determinant will preserve (or uniformly reverse) the values of $\sigma$. In particular, given the identity $\det(AB) = \det(A)\det(B)$, if we apply a transformation to the points that corresponds to multiplying by a matrix $B$ such that $\det(B) > 0$, then $\sign(\det(A)) = \sign(\det(AB))$, and thus orientations will be preserved. -In step 1, we transform the list of points so that no two points share the same $x$-coordinate. This can be done by applying a rotation to the list of points, which corresponds to multiplying by a rotation matrix. -Rotations always have determinant $1$. -In step 2, we translate all points by a constant vector $t$, by multiplying by a translation matrix, so that the left most point gets position $(0, 0)$, and naturally every other point will have a positive $x$-coordinate. -Let $L_2$ be the list of points after this transformation, excluding $(0,0)$ which we will denote by $p_1$. -Then, in step 3, we apply the projective transformation $f: (x, y) \mapsto (y/x, 1/x)$ to every point in $L_2$, showing that this preserves orientations within $L_2$. -To see that this mapping is a $\sigma$-equivalence consider that +The proof proceeds in 6 steps, illustrated in~\Cref{fig:symmetry-breaking}. +In each of the steps, we construct a new list of points that is $\sigma$-equivalent to the previous one, +with the last one being in canonical position.\footnote{ +Even though we defined $\sigma$-equivalence for sets of points, +our formalization goes back and forth between sets and lists. +Given that symmetry breaking distinguishes between the order of the points +e.g., $x$-order, this proof proceeds over lists. +All permutations of a list are immediately $\sigma$-equivalent.} +The main justification for each step is that, +given that the function $\sigma$ is defined as a sign of the determinant, +applying transformations that preserve (or, when \lstinline|parity := true|, uniformly reverse) +the sign of the determinant will preserve (or uniformly reverse) the values of $\sigma$. + +For example, given the identity $\det(AB) = \det(A)\det(B)$, +if we apply a transformation to the points that corresponds to multiplying by a matrix $B$ such that $\det(B) > 0$, +then $\sign(\det(A)) = \sign(\det(AB))$, and thus orientations will be preserved. +\textbf{Step 1}: we transform the list of points so that no two points share the same $x$-coordinate. +This can be done by applying a rotation to the list of points, which corresponds to multiplying by a rotation matrix. +Rotations always have determinant $1$. +\textbf{Step 2}: we translate all points by a constant vector $t$, which corresponds to multiplying by a translation matrix, +to bring the leftmost point~$p_1$ to position $(0, 0)$. +As a result, every other point has a positive $x$-coordinate. + +Let $L_2$ be the list of points excluding $p_1$ after Step 2. +\textbf{Step 3}: we apply the projective transformation $f: (x, y) \mapsto (y/x, 1/x)$ to every point in $L_2$, +showing that this preserves orientations within $L_2$. +To see that this mapping is a $\sigma$-equivalence consider that \[ \begin{multlined} \sign \det \begin{pmatrix} p_x & q_x & r_x \\ p_y & q_y & r_y \\ 1 & 1 & 1 \end{pmatrix} = \sign \det \left( \begin{pmatrix} 0 & 0 & 1 \\ 1 & 0 & 0\\ 0 & 1 & 0 \end{pmatrix} \begin{pmatrix} \nicefrac{p_y}{p_x} & \nicefrac{q_y}{q_x} & \nicefrac{r_y}{r_x} \\ \nicefrac{1}{p_x} & \nicefrac{1}{q_x} & \nicefrac{1}{r_x} \\ 1 & 1 & 1 \end{pmatrix} \begin{pmatrix} p_x & 0 & 0 \\ 0 & q_x & 0\\ 0 & 0 & r_x \end{pmatrix} \right)\\ @@ -69,7 +92,8 @@ % \tag{As $p_x q_x r_x > 0$ by step 2} \end{multlined} \] -To preserve orientations with respect to the leftmost point $(0, 0)$, we set $f( (0, 0)) = (0, \infty)$, a special point that is treated separately as follows. +To preserve orientations with respect to the leftmost point $(0, 0)$, we set $f( (0, 0)) = (0, \infty)$, +a special point that is treated separately as follows. As the function $\sigma$ takes points in $\mathbb{R}^2$ as arguments, we need to define an extension \( @@ -79,13 +103,25 @@ \end{cases}, \) We then show that $\sigma((0, 0), q, r) = \sigma_{(0, \infty)}(f(q), f(r))$ for all points $q, r \in L_2$. -In step 4, we sort the list $L_2$ by $x$-coordinate in increasing order, thus obtaining a list $L_3$. -This can be done while preserving $\sigma$-equivalence because sorting corresponds to a permutation, and all permutations of a list are $\sigma$-equivalent by definition. -In step 5, we check whether the \textsf{Lex order} condition above is satisfied in $L_3$, and if it is not, we reflect the pointset, which preserves $\sigma$-equivalence with \lstinline|parity := true|. + +\textbf{Step 4}: we sort the list~$L_2$ by $x$-coordinate in increasing order, +thus obtaining a list~$L_3$. +This can be done while preserving $\sigma$-equivalence because sorting corresponds to a permutation, +and all permutations of a list are $\sigma$-equivalent by definition. +\textbf{Step 5}: we check whether the \textsf{Lex order} condition above is satisfied in $L_3$, +and if it is not, we reflect the pointset, +which preserves $\sigma$-equivalence with \lstinline|parity := true|. Note that in such a case we need to relabel the points from left to right again. -In step 6, we bring point $(0, \infty)$ back into the range by first finding a constant $c$ such that all points in $L_3$ are to the right of the line $y=c$, and then finding a large enough value $M$ such that $(c, M)$ has the same orientation with respect to the other points as $(0, \infty)$ did, meaning that + +\textbf{Step 6}: we bring point $(0, \infty)$ back into the range +by first finding a constant $c$ such that all points in $L_3$ are to the right of the line $y=c$, +and then finding a large enough value $M$ such that $(c, M)$ has the same orientation +with respect to the other points as $(0, \infty)$ did, +meaning that \(\sigma((c, M), q, r) = \sigma_{(0, \infty)}(q, r)\) for every $q, r \in L_3$. -Finally, we note that the list of points obtained in step 6 satisfies the \text{CCW-order} property by the following reasoning: + +Finally, we note that the list of points obtained in step 6 +satisfies the \text{CCW-order} property by the following reasoning: if $1 < i < j \leq n$ are indices, then \begin{align*} \sigma(p_1, p_i, p_j) = 1 &\iff \sigma((c, M), p_i, p_j) = 1\\ @@ -95,4 +131,3 @@ \end{align*} This concludes the proof. \end{proof} - diff --git a/ITP/triple-orientations.tex b/ITP/triple-orientations.tex index ce283f2..a000063 100644 --- a/ITP/triple-orientations.tex +++ b/ITP/triple-orientations.tex @@ -128,13 +128,18 @@ structure σEquiv (S T : Set Point) where f : Point → Point bij : Set.BijOn f S T - parity : Bool -- See Section 4 for details on this field + parity : Bool σ_eq : ∀ (p ∈ S) (q ∈ S) (r ∈ S), σ p q r = parity ^^^ σ (f p) (f q) (f r) def OrientationProperty (P : Set Point → Prop) := ∀ {{S T}}, S ≃σ T → P S → P T -- `≃σ` is infix notation for `σEquiv` \end{lstlisting} +Our notion of \(\sigma\) equivalence allows for all orientations to be flipped. +The \lstinline{^^^} (xor) operation does nothing when \lstinline{parity} is false, +and negates the orientation when \lstinline{parity} is true. +See~\Cref{sec:symmetry-breaking} for more details. + To illustrate how these notions will be used, let us consider the property \( \pi_k(S) \triangleq \text{\em ``pointset } S \text{ contains an empty convex } k\text{-gon''} @@ -184,17 +189,17 @@ ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ∀ (a ∈ s) (b ∈ s) (c ∈ s), a ≠ b → a ≠ c → b ≠ c → σIsEmptyTriangleFor a b c S -theorem σHasEmptyKGon_iff_HasEmptyKGon (gp : ListInGenPos pts) : - σHasEmptyKGon n pts.toFinset ↔ HasEmptyKGon n pts.toFinset +theorem σHasEmptyKGon_iff_HasEmptyKGon {n : Nat} (gp : ListInGenPos pts) : + σHasEmptyKGon n pts.toFinset ↔ HasEmptyKGon n pts.toFinset \end{lstlisting} Then, because \lstinline|σHasEmptyKGon| is ultimately defined in terms of $\sigma$, we can prove \begin{lstlisting} -lemma OrientationProperty_σHasEmptyKGon : OrientationProperty (σHasEmptyKGon n) +lemma OrientationProperty_σHasEmptyKGon {n : Nat} : OrientationProperty (σHasEmptyKGon n) \end{lstlisting} Which in combination with \lstinline|theorem σHasEmptyKGon_iff_HasEmptyKGon|, provides \begin{lstlisting} -theorem OrientationProperty_HasEmptyKGon : OrientationProperty (HasEmptyKGon n) +theorem OrientationProperty_HasEmptyKGon {n : Nat} : OrientationProperty (HasEmptyKGon n) \end{lstlisting} The previous theorem is important for two reasons. @@ -239,15 +244,25 @@ \subsection{Properties of orientations}\label{sec:sigma-props} σ p q r = cw → σ q r s = cw → σ p r s = cw \end{lstlisting} -They will be used in justifying the addition of clauses~\labelcref{eq:signotopeClauses11,eq:signotopeClauses12}; -clauses like these or the one below are easily added, -and are commonly used to reduce the search space in SAT encodings~\cite{emptyHexagonNumber,scheucherTwoDisjoint5holes2020,subercaseaux2023minimizing, szekeres_peters_2006}. - -\begin{align} - &\left(\neg \orvar_{a, b, c} \lor \neg \orvar_{a, c, d} \lor \orvar_{a, b, d}\right) \land \left(\orvar_{a, b, c} \lor \orvar_{a, c, d} \lor \neg \orvar_{a, b, d}\right) -\end{align} +Our proofs of these properties are based on an equivalence between +the orientation of a triple of points +and the \emph{slopes} of the lines that connect them. +Namely, if $p, q, r$ are sorted from left to right, +then (i) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pq}) < \textsf{slope}(\overrightarrow{pr})$ +and (ii) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pr}) < \textsf{slope}(\overrightarrow{qr})$. +By first proving these \emph{slope-orientation} equivalences +we can then easily prove \lstinline|σ_prop₁| and others, +as illustrated in~\Cref{fig:orientation-implication}. + +These properties will be used in~\Cref{sec:encoding} +to justify clauses~\labelcref{eq:signotopeClauses11,eq:signotopeClauses12} of the SAT encoding; +these clauses are commonly added in orientation-based SAT encodings +to reduce the search space by removing some ``unrealizable'' orientations~\cite{emptyHexagonNumber,scheucherTwoDisjoint5holes2020,subercaseaux2023minimizing, szekeres_peters_2006}. +\[ + \left(\neg \orvar_{a, b, c} \lor \neg \orvar_{a, c, d} \lor \orvar_{a, b, d}\right) \land + \left(\orvar_{a, b, c} \lor \orvar_{a, c, d} \lor \neg \orvar_{a, b, d}\right) +\] -Our proofs of these properties are based on an equivalence between the orientation of a triple of points and the \emph{slopes} of the lines that connect them. Namely, if $p, q, r$ are sorted from left to right, then (i) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pq}) < \textsf{slope}(\overrightarrow{pr})$ and (ii) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pr}) < \textsf{slope}(\overrightarrow{qr})$. By first proving these \emph{slope-orientation} equivalences we can then easily prove \lstinline|σ_prop₁| and others, as illustrated in~\Cref{fig:orientation-implication}. \begin{figure} \centering diff --git a/Lean/Geo.lean b/Lean/Geo.lean index 0335fc7..17bf0a0 100644 --- a/Lean/Geo.lean +++ b/Lean/Geo.lean @@ -19,11 +19,11 @@ i.e. the point set encloses a convex polygon. Also known as a "convex-independen recall Geo.ConvexIndep (S : Set Point) : Prop := ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a}) -recall Geo.HasConvexKGon (n : Nat) (S : Set Point) : Prop := - ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s +recall Geo.HasConvexKGon (n : Nat) (P : Set Point) : Prop := + ∃ S : Finset Point, S.card = n ∧ ↑S ⊆ P ∧ ConvexIndep S -recall Geo.HasEmptyKGon (n : Nat) (S : Set Point) : Prop := - ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s ∧ EmptyShapeIn s S +recall Geo.HasEmptyKGon (n : Nat) (P : Set Point) : Prop := + ∃ S : Finset Point, S.card = n ∧ ↑S ⊆ P ∧ ConvexIndep S ∧ EmptyShapeIn S P /- `gonNumber k` is the smallest number `n` such that every set of `n` or more points in general position contains a convex-independent set of size `k`. -/ diff --git a/Lean/Geo/Definitions/Structures.lean b/Lean/Geo/Definitions/Structures.lean index 586508d..329dc35 100644 --- a/Lean/Geo/Definitions/Structures.lean +++ b/Lean/Geo/Definitions/Structures.lean @@ -257,10 +257,10 @@ theorem EmptyShapeIn.split (cvx : ConvexIndep S) (ha : a ∈ S) (hb : b ∈ S) (H2 : EmptyShapeIn {x ∈ S | σ a b x ≠ .cw} P) : EmptyShapeIn S P := fun _ ⟨pP, pS⟩ hn => (split_convexHull cvx ha hb hn).elim (H1 _ ⟨pP, mt And.left pS⟩) (H2 _ ⟨pP, mt And.left pS⟩) -def HasEmptyKGon (n : Nat) (S : Set Point) : Prop := - ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexEmptyIn s S +def HasEmptyKGon (n : Nat) (P : Set Point) : Prop := + ∃ S : Finset Point, S.card = n ∧ ↑S ⊆ P ∧ ConvexEmptyIn S P -def HasConvexKGon (n : Nat) (S : Set Point) : Prop := - ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s +def HasConvexKGon (n : Nat) (P : Set Point) : Prop := + ∃ S : Finset Point, S.card = n ∧ ↑S ⊆ P ∧ ConvexIndep S end Geo