Skip to content

Commit

Permalink
feat: pictures
Browse files Browse the repository at this point in the history
  • Loading branch information
@Vtec234
Vtec234 committed Sep 8, 2024
1 parent 37c1bd9 commit 81a0c80
Showing 1 changed file with 254 additions and 57 deletions.
311 changes: 254 additions & 57 deletions ITP/slides.typ
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,39 @@
#import "@preview/cetz:0.2.2"
#import themes.metropolis: *

// Like cetz.draw.grid, but allows independently specifying
// where the grid lines should be placed (`from`, `to`),
// and how far they should extend (`froml`, `tol`).
#let grid2(from, to, froml, tol, step: 1, ..style) = {
import cetz.draw: line
let (fx, fy) = from
let (tx, ty) = to
let (flx, fly) = froml
let (tlx, tly) = tol
assert(fx <= tx)
assert(fy <= ty)
assert(flx <= tlx)
assert(fly <= tly)
assert(flx <= fx)
assert(tx <= tlx)
assert(fly <= fy)
assert(ty <= tly)
let eps = 0.000000000001
let x = fx
while x <= tx + eps {
line((x, fly), (x, tly), ..style)
x += step
}

let y = fy
while y <= ty + eps {
line((flx, y), (tlx, y), ..style)
y += step
}
}

#let lean = $"L∃∀N"$

// Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf

#let config = (
Expand Down Expand Up @@ -42,7 +75,6 @@
Fix a set $S$ of points on the plane, _no three collinear_.
A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior.

// PERTURB THE POINTS
#align(center, components.side-by-side(
cetz.canvas(length: 33%, {
import cetz.draw: *
Expand All @@ -64,7 +96,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior.
import cetz.draw: *
set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
on-layer(1, {
circle((angle: 0deg, radius: 1), name: "a")
circle((angle: 1deg, radius: 1), name: "a")
circle((angle: 120deg, radius: 1), name: "b")
circle((angle: 180deg, radius: 0.2), name: "c")
circle((angle: 240deg, radius: 1), name: "d")
Expand All @@ -78,7 +110,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior.
import cetz.draw: *
set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
on-layer(1, {
circle((angle: 0deg, radius: 1), name: "a")
circle((angle: 359deg, radius: 1), name: "a")
circle((angle: 120deg, radius: 1), name: "b")
circle((angle: 240deg, radius: 1), name: "c")
circle((angle: 30deg, radius: 0.2))
Expand Down Expand Up @@ -207,29 +239,36 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior.
}
}))

/////////// DONE ABOVE
/////////// WORK AREA BELOW
== The Happy Ending Problem

// TODO(WN): make #pause-gray gray out the things that came before
$g(k) =$ least $n$ s.t. any set of $n$ points must contain a *convex $bold(k)$-gon*
$h(k) =$ least $n$ s.t. any set of $n$ points must contain a *$bold(k)$-hole* #pause
We just showed $h(4) ≤ 5$ and $9 < h(5)$. #pause

*Theorem* @35erdos_combinatorial_problem_geometry.
For a fixed $k$, every _sufficiently large_ set of points contains a convex $k$-gon.
So all $g(k)$ are finite. #pause

*Theorem* @hortonSetsNoEmpty1983.
For any $k ≥ 7$, there exist arbitrarily large sets of points containing no $k$-holes.
So $h(7) = h(8) = … = ∞$.
#slide(
config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)),
self => [
// WN: Not sure about this uncover dance..
#uncover("1, 3, 5", [$g(k) =$ least $n$ s.t. any set of $n$ points must contain a *convex $bold(k)$-gon*])

#uncover("1, 2, 4, 5", [$h(k) =$ least $n$ s.t. any set of $n$ points must contain a *$bold(k)$-hole*])

#uncover("2, 5", [We just showed $h(4) ≤ 5$ and $9 < h(5)$])

#uncover("3, 5", [
*Theorem* @35erdos_combinatorial_problem_geometry.
For a fixed $k$, every _sufficiently large_ set of points contains a convex $k$-gon.
So all $g(k)$ are finite.
])

#uncover("4, 5", [
*Theorem* @hortonSetsNoEmpty1983.
For any $k ≥ 7$, there exist arbitrarily large sets of points containing no $k$-holes.
So $h(7) = h(8) = … = ∞$.
])
]
)

== Known tight bounds

// TODO: This slide is too wordy

#table(
columns: (auto, auto),
inset: 5pt,
Expand All @@ -239,13 +278,12 @@ So $h(7) = h(8) = … = ∞$.
[$h(4) = 5$ (Klein 1932)],
[$g(4) = 5$ (Klein 1932)],
[$h(5) = 10$ @Harborth1978],
// TODO: see https://en.wikipedia.org/wiki/Happy_ending_problem#cite_note-4
[$g(5) = 9$ (CITATION NEEDED)],
[$g(5) = 9$ (Makai 1930s)],
[*$bold(h(6) = 30)$ @03overmars_finding_sets_points_empty_convex_6_gons @24heule_happy_ending_empty_hexagon_every_set_30_points*],
[$g(6) = 17$ @szekeres_peters_2006],
) #pause

We formally verified all the above in $L∃∀N$. #pause
We formally verified all the above in #lean. #pause

Upper bounds by combinatorial reduction to SAT. #pause

Expand Down Expand Up @@ -274,50 +312,209 @@ _focus of our work_.

== Reduction from geometry to SAT

// TODO: make text shorter
#slide(
config: config-methods(cover: (self: none, body) => box(scale(x: 0%, body))),
self => [
#set text(size: 23pt)
1. Discretize from continuous coordinates in $ℝ²$ to boolean variables. #pause
2. Points can be put in _canonical form_
without removing $k$-holes.
```lean
theorem symmetry_breaking {l : List Point} :
3 ≤ l.length → PointsInGenPos l →
∃ w : CanonicalPoints, l ≼σ w.points
``` #pause
3. $n$ points in canonical form with no $6$-holes
induce a propositional assignment that satisfies $φ_n$.
```lean
theorem satisfies_hexagonEncoding {w : CanonicalPoints} :
¬σHasEmptyKGon 6 w → w.toPropAssn ⊨ Geo.hexagonCNF w.len
``` #pause
4. But $φ_30$ is unsatisfiable.
```lean
axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat
```
]
)

// TODO(WN): pauses for the list
#set text(size: 23pt)
1. Points can be put in _canonical form_
without removing $k$-holes.
```lean
theorem symmetry_breaking {l : List Point} :
3 ≤ l.length → PointsInGenPos l →
∃ w : CanonicalPoints, l ≼σ w.points
```
2. $n$ points in canonical form with no $6$-holes
induce a propositional assignment that satisfies $φ_n$.
```lean
theorem satisfies_hexagonEncoding {w : CanonicalPoints} :
¬σHasEmptyKGon 6 w → w.toPropAssn ⊨ Geo.hexagonCNF w.len
```
3. But $φ_30$ is unsatisfiable.
```lean
axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat
```
== Discretization with triple-orientations

== 1. Symmetry breaking
#let fig = align(center, cetz.canvas({
import cetz.draw: *
set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.1))
scale(3.2)

on-layer(1, {
let pts = (
(0, 0, "p"), (1, 1, "s"), (2, 1, "q"), (1.2, 2, "r"), (1.8, 1.8, "t")
)
for (x, y, n) in pts {
circle((x, y), name: n)
content((x, y+0.015), [#set text(fill: config.colors.neutral-lightest, size: 20pt); $#n$])
}
})

let (cg, cb, cr) = (green, blue, red).map(c => c.desaturate(50%))
line("p", "r", "q", stroke: cg, mark: (end: "stealth", fill: cg))
line("p", "s", "t", stroke: cb, mark: (end: "stealth", fill: cb))
line("r", "s", "q", stroke: cr, mark: (end: "stealth", fill: cr))
}))

// TODO: add teh content
#components.side-by-side(
columns: (1fr, 18em),
fig,
[
$ σ(p,r,q) &= 1 &("clockwise") \
σ(p,s,t) &= 0 &("collinear") \
σ(r,s,q) &= -1#h(1em) &("counter-clockwise") $
]
) #pause

The sequence of six steps from Fig. 5
(transformation into `CanonicalPoints`);
make it an animation.
#align(center, [
$∃$ $k$-hole ⇔ a propositional formula over $σ(a,b,c)$ is satisfiable
])

// WN: I think cap-cup here would be too deep into the weeds

== 2. SAT encoding
== Symmetry breaking

// TODO: add teh content
#slide(repeat: 6, align: center+horizon, self => [
#let fig = cetz.canvas({
import cetz.draw: *
let pts = (
((-1.3, 0.25), (-1.3, 0.9), (-0.7, -0.45), (-0.35, 0.35), (-0.35, -0.8), (0.6, 0.5), (0.9, -0.6), (1.4, 1.1), (0.6, -1.1),),
((-1.09601563215555, -0.7424619411597272), (-1.5556349648261614, -0.28284245828783905), (-0.17677682816699475, -0.8131727694796578), (-0.49497474683057663, 8.087761060870946e-08), (0.3181979186635819, -0.8131728503572684), (0.07071080521204193, 0.7778174477512475), (1.0606602064416402, 0.21213186104679588), (0.21213232320457065, 1.767766918304512), (1.202081470247393, -0.3535535870103234),),
((0.4596193326706113, -0.45961948287188814), (0.0, 0.0), (1.3788581366591666, -0.5303303111918187), (1.0606602179955846, 0.28284253916544966), (1.8738328834897433, -0.5303303920694293), (1.6263457700382034, 1.0606599060390867), (2.6162951712678018, 0.4949743193346349), (1.767767288030732, 2.0506093765923508), (2.7577164350735544, -0.07071112872248436),),
((-1.00000032679495, 2.1757135283877527), (0, 3.85), (-0.3846155721840648, 0.7252377698715973), (0.2666664916498519, 0.9428090005013866), (-0.2830190444100679, 0.5336655199142649), (0.6521736801480853, 0.6148753963780468), (0.1891890199433349, 0.3822198699068886), (1.1599996167350177, 0.5656853177286622), (-0.025641189145902285, 0.3626188636662086),),
((-1.00000032679495, 2.1757135283877527), (-1.2, 3.85), (-0.3846155721840648, 0.7252377698715973), (0.2666664916498519, 0.9428090005013866), (-0.2830190444100679, 0.5336655199142649), (0.6521736801480853, 0.6148753963780468), (0.1891890199433349, 0.3822198699068886), (1.1599996167350177, 0.5656853177286622), (-0.025641189145902285, 0.3626188636662086),),
((-1.2, 3.85), (-1.00000032679495, 2.1757135283877527), (-0.3846155721840648, 0.7252377698715973), (-0.2830190444100679, 0.5336655199142649), (-0.025641189145902285, 0.3626188636662086), (0.1891890199433349, 0.3822198699068886), (0.2666664916498519, 0.9428090005013866), (0.6521736801480853, 0.6148753963780468), (1.1599996167350177, 0.5656853177286622),),
)
let extents = (
((-1.7, -1.3), (1.7, 2.3)),
((-1.7, -1.3), (1.7, 2.3)),
((-0.7, -1.3), (3.1, 2.3)),
((-1.2, -0.2), (2.4, 2.9)),
((-1.5, -0.2), (2.4, 3.7)),
((-1.5, -0.2), (2.4, 3.7)),
)
let regions = (
(("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),),
(("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),),
(("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),),
(("1", "3", "4", "b", "a", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("4", "6", "8", "c", "b", "4"),),
(("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),),
(("1", "2", "3", "7", "1"), ("3", "4", "5", "6", "8", "7", "3"), ("6", "9", "8", "6"), ("7", "8", "9", "1", "7"),),
)

scale(3.2)

// Grid and axes
let ((efx, efy), (etx, ety)) = extents.at(self.subslide - 1)
on-layer(-1, {
grid2(
(calc.ceil(efx), calc.ceil(efy)), (calc.floor(etx), calc.floor(ety)),
(efx, efy), (etx, ety),
stroke: (thickness: 0.2pt, paint: gray, dash: "dashed"))
})
set-style(line: (stroke: (paint: config.colors.neutral-darkest, thickness: 1.5pt)))
line((efx, 0), (etx, 0), mark: (end: "stealth", fill: config.colors.neutral-darkest))
line((0, efy), (0, ety), mark: (end: "stealth", fill: config.colors.neutral-darkest))
content((etx -0.18, -0.2), $x$)
content((0.2, ety -0.1), $y$)

// Points
on-layer(1, {
set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.1))
for (n, (x, y)) in pts.at(self.subslide - 1).enumerate(start: 1) {
if self.subslide == 4 and n == 2 {
// Point at infinity gets special color
circle((x, y), name: str(n), fill: config.colors.primary)
} else {
circle((x, y), name: str(n))
}
content((x, y), [#set text(fill: config.colors.neutral-lightest, size: 20pt); #str(n)])
}
})

// Convex regions
on-layer(-1, {
set-style(line: (stroke: none))
let colors = (red, orange, blue, green).map(c => c.transparentize(70%))
// Extra convex regions at infinity
if self.subslide == 4 {
circle((-1.00000032679495, 2.7), name: "a", radius: 0)
circle((0.2666664916498519, 2.7), name: "b", radius: 0)
circle((1.1599996167350177, 2.7), name: "c", radius: 0)
circle((-0.1, 3.4), name: "x", radius: 0)
circle((0, 3.4), name: "y", radius: 0)
circle((0.1, 3.4), name: "z", radius: 0)
line("x", "y", "2", "x", fill: colors.at(0))
line("y", "z", "2", "y", fill: colors.at(3))
line("a", "x", stroke: (thickness: 2pt, dash: "dotted", paint: colors.at(0)))
line("b", "y", stroke: (thickness: 2pt, dash: "dotted", paint: colors.at(0)))
line("c", "z", stroke: (thickness: 2pt, dash: "dotted", paint: colors.at(3)))
}

for (r, c) in regions.at(self.subslide - 1).zip(colors) {
line(..r, fill: c)
}
})

// Equal-x marker lines
if self.subslide == 1 {
let ((_, yf), (_, yt)) = extents.at(0)
let (x4, _) = pts.at(0).at(3)
let (x6, _) = pts.at(0).at(5)
set-style(line: (stroke: (thickness: 1pt, dash: "dashed", paint: red)))
line((x4, yf), (x4, yt))
line((x6, yf), (x6, yt))
}
})

#let captions = (
[Starting set of points.],
[Rotation ensures distinct $x$.],
[Translate leftmost point to $(0,0)$.\
Ensures nonnegative $x$.],
[Map $(x,y) ↦ (y/x, 1/x)$.],
[Bring point at $∞$ back.],
[Relabel in order of increasing $x$.],
)

#components.side-by-side(
columns: (15em, 1fr),
captions.at(self.subslide - 1),
fig,
)
])

// TODO: Maybe rm this slide? It's not adding much
== Symmetry breaking: result

Points now in normal form. #pause

- Introduce $σ$ variables
- Show scary picture of full encoding (?)
- Talk about cap-cup clauses; copy slide 14/21 from Marijn
Normalization drastically reduces search space for SAT solver. #pause

```lean
structure CanonicalPoints where
leftmost : Point
rest : List Point
sorted' : (leftmost :: rest).Sorted (·.x < ·.x)
gp' : ListInGenPos (leftmost :: rest)
oriented : rest.Pairwise (σ leftmost · · = .ccw)
lex : σRevLex rest
```

== 3. Running the SAT solver
== Running the SAT solver

// TODO: add teh content
CNF formula produced directly from executable #lean definition. #pause

How many clauses, how long it took, cluster compute amount (from 'Running the CNF')
To verify $h(6) ≤ 30$:\ #pause
▸ CNF with 444215 clauses\ #pause
▸ partitioned into 312 418 subproblems\ #pause
▸ each subproblem solved by CaDiCaL 1.9.5\ #pause
▸ unsatisfiability proofs checked on-the-fly by `cake_lpr`\ #pause
▸ 25 876.5 CPU hours on Bridges 2 cluster of Pittsburgh Supercomputing Center

== Lower bounds

Expand Down

0 comments on commit 81a0c80

Please sign in to comment.