diff --git a/ITP/Monokai Dark.tmTheme b/ITP/Monokai Dark.tmTheme new file mode 100644 index 0000000..d8de214 --- /dev/null +++ b/ITP/Monokai Dark.tmTheme @@ -0,0 +1,410 @@ + + + + + name + Monokai Dark + settings + + + settings + + background + #0D0D0D + caret + #F8F8F0 + foreground + #F8F8F2 + invisibles + #3B3A32 + lineHighlight + #3D3D3D55 + selection + #A63A62 + + + + name + Comment + scope + comment + settings + + foreground + #8C8C8C + + + + name + String + scope + string + settings + + foreground + #FFEE99 + + + + name + Number + scope + constant.numeric + settings + + foreground + #FF80F4 + + + + name + Built-in constant + scope + constant.language + settings + + foreground + #FF80F4 + + + + name + User-defined constant + scope + constant.character, constant.other + settings + + foreground + #FF80F4 + + + + name + Variable + scope + variable + settings + + fontStyle + + + + + name + Keyword + scope + keyword + settings + + foreground + #F92672 + + + + name + Storage + scope + storage + settings + + fontStyle + + foreground + #F92672 + + + + name + Storage type + scope + storage.type + settings + + fontStyle + italic + foreground + #66D9EF + + + + name + Class name + scope + entity.name.class + settings + + fontStyle + underline + foreground + #A6E22E + + + + name + Inherited class + scope + entity.other.inherited-class + settings + + fontStyle + italic underline + foreground + #A6E22E + + + + name + Function name + scope + entity.name.function + settings + + fontStyle + + foreground + #A6E22E + + + + name + Function argument + scope + variable.parameter + settings + + fontStyle + italic + foreground + #FD971F + + + + name + Tag name + scope + entity.name.tag + settings + + fontStyle + + foreground + #F92672 + + + + name + Tag attribute + scope + entity.other.attribute-name + settings + + fontStyle + + foreground + #A6E22E + + + + name + Library function + scope + support.function + settings + + fontStyle + + foreground + #66D9EF + + + + name + Library constant + scope + support.constant + settings + + fontStyle + + foreground + #66D9EF + + + + name + Library class/type + scope + support.type, support.class + settings + + fontStyle + italic + foreground + #66D9EF + + + + name + Library variable + scope + support.other.variable + settings + + fontStyle + + + + + name + PHP Namespaces + scope + support.other.namespace, entity.name.type.namespace + settings + + foreground + #FFB2F9 + + + + name + PHP Namespace Alias + scope + support.other.namespace.use-as.php + settings + + foreground + #66D9EF + + + + name + PHP Namespace Keyword + scope + variable.language.namespace.php + settings + + foreground + #D66990 + + + + name + PHP Namespace Separator + scope + punctuation.separator.inheritance.php + settings + + foreground + #F92672 + + + + name + CSS Functions / Property Values + scope + support.function.misc.css, support.constant.property-value.css, support.constant.font-name.css + settings + + foreground + #FFEE99 + + + + name + Twig Tagbraces + scope + entity.other.tagbraces.twig + settings + + foreground + #A6E22E + + + + name + Twig Tag + scope + keyword.control.twig + settings + + foreground + #FD971F + + + + name + Twig Variable + scope + variable.other.twig + settings + + foreground + #FF80F4 + + + + name + Twig Variable Filter + scope + support.function.filter.variable.twig + settings + + foreground + #FFCCFB + + + + name + Twig Function + scope + entity.name.function.twig + settings + + foreground + #F92672 + + + + name + Twig Function Argument + scope + entity.other.argument.twig + settings + + foreground + #E5DB7E + + + + name + Invalid + scope + invalid + settings + + background + #F92672 + fontStyle + + foreground + #F8F8F0 + + + + name + Invalid deprecated + scope + invalid.deprecated + settings + + background + #FF80F4 + foreground + #F8F8F0 + + + + uuid + 233F0694-0B9C-43E3-A44A-ECECF7DF6C73 + + diff --git a/ITP/main.bib b/ITP/main.bib index 53681cd..d724e16 100644 --- a/ITP/main.bib +++ b/ITP/main.bib @@ -43,17 +43,6 @@ @article{60erdos_some_extremum_problems_elementary_geometry year={1960} } -@article{06szekeres_computer_solution_17_point_erdos_szekeres_problem, - title={Computer solution to the 17-point Erd{\H{o}}s-Szekeres problem}, - author={George Szekeres and Lindsay Peters}, - journal={The ANZIAM Journal}, - volume={48}, - number={2}, - pages={151--164}, - year={2006}, - publisher={Cambridge University Press} -} - @incollection{Crawford, author = {James Crawford and Matthew Ginsberg and Eugene Luks and Amitabha Roy}, title = {Symmetry-Breaking Predicates for Search Problems}, @@ -689,3 +678,58 @@ @InProceedings{cube_and_conquer abstract="Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel.", isbn="978-3-642-34188-5" } + +@inproceedings{24heule_happy_ending_empty_hexagon_every_set_30_points, + author = {Marijn J. H. Heule and + Manfred Scheucher}, + editor = {Bernd Finkbeiner and + Laura Kov{\'{a}}cs}, + title = {Happy Ending: An Empty Hexagon in Every Set of 30 Points}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems + - 30th International Conference, {TACAS} 2024, Held as Part of the + European Joint Conferences on Theory and Practice of Software, {ETAPS} + 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, + Part {I}}, + series = {Lecture Notes in Computer Science}, + volume = {14570}, + pages = {61--80}, + publisher = {Springer}, + year = {2024}, + url = {https://doi.org/10.1007/978-3-031-57246-3_5}, + doi = {10.1007/978-3-031-57246-3_5}, + timestamp = {Sat, 08 Jun 2024 13:13:56 +0200}, + biburl = {https://dblp.org/rec/conf/tacas/HeuleS24.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{03overmars_finding_sets_points_empty_convex_6_gons, + author = {Mark H. Overmars}, + title = {Finding Sets of Points without Empty Convex 6-Gons}, + journal = {Discret. Comput. Geom.}, + volume = {29}, + number = {1}, + pages = {153--158}, + year = {2003}, + url = {https://doi.org/10.1007/s00454-002-2829-x}, + doi = {10.1007/S00454-002-2829-X}, + timestamp = {Thu, 12 Mar 2020 17:21:09 +0100}, + biburl = {https://dblp.org/rec/journals/dcg/Overmars03.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{90dobkin_searching_empty_convex_polygons, + author = {David P. Dobkin and + Herbert Edelsbrunner and + Mark H. Overmars}, + title = {Searching for Empty Convex Polygons}, + journal = {Algorithmica}, + volume = {5}, + number = {4}, + pages = {561--571}, + year = {1990}, + url = {https://doi.org/10.1007/BF01840404}, + doi = {10.1007/BF01840404}, + timestamp = {Wed, 17 May 2017 14:25:12 +0200}, + biburl = {https://dblp.org/rec/journals/algorithmica/DobkinEO90.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} \ No newline at end of file diff --git a/ITP/proof.png b/ITP/proof.png new file mode 100644 index 0000000..f0b9757 Binary files /dev/null and b/ITP/proof.png differ diff --git a/ITP/slides.typ b/ITP/slides.typ new file mode 100644 index 0000000..edb900b --- /dev/null +++ b/ITP/slides.typ @@ -0,0 +1,739 @@ +#import "@preview/touying:0.5.2": * +#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 = "Lean" +#let thin = h(3em/18) + +// Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf + +#let config = ( + aspect-ratio: "16-9", + // config-common(handout: true), + ..config-info( + title: [Formal Verification of the Empty Hexagon Number], + author: [ + Bernardo Subercaseaux¹, Wojciech Nawrocki¹, James Gallicchio¹,\ + Cayden Codel¹, #underline[Mario Carneiro]#h(0em)¹, Marijn J. H. Heule¹ + ], + date: [ + _Interactive Theorem Proving_ | September 9th, 2024\ + Tbilisi, Georgia + ], + institution: [¹ Carnegie Mellon University, USA] + ), + ..config-colors( + primary: rgb("#fb912b"), + primary-light: rgb("#d6c6b7"), + secondary: rgb("#fafafa"), + neutral-lightest: rgb("#13272b"), + neutral-dark: rgb("#fafafa"), + neutral-darkest: rgb("#fafafa"), + ) +) +#show: metropolis-theme.with(config) +#set text(size: 23pt) +#set raw(theme: "Monokai Dark.tmTheme") + +#title-slide() + +// WN: I think this should be first slide, not the 9-pt example; +// it is really confusing to look at a pointset +// without knowing what kind of structure one is looking for. + +== Empty $k$-gons + +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. + +#align(center, components.side-by-side( + cetz.canvas(length: 33%, { + 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: 72deg, radius: 1), name: "b") + circle((angle: 144deg, radius: 1), name: "c") + circle((angle: 216deg, radius: 1), name: "d") + circle((angle: 290deg, radius: 1), name: "e") + circle((angle: 30deg, radius: 1.5)) + circle((angle: 240deg, radius: 1.5)) + }) + line("a", "b", "c", "d", "e", "a", fill: config.colors.primary.transparentize(20%), stroke: config.colors.primary) + content((0, -1.5), "5-hole ✔") + content((0, -2.0), "convex 5-gon ✔") + }), + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + on-layer(1, { + 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") + circle((angle: 200deg, radius: 1.2)) + }) + line("a", "b", "c", "d", "a", fill: config.colors.primary-light.transparentize(20%), stroke: config.colors.primary-light) + content((0, -1.5), "4-hole ✘") + content((0, -2.0), "convex 4-gon ✘") + }), + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + on-layer(1, { + 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)) + }) + line("a", "b", "c", "a", fill: config.colors.primary-light.transparentize(20%), stroke: config.colors.primary-light) + content((0, -1.5), "3-hole ✘") + content((0, -2.0), "convex 3-gon ✔") + }), +)) + +// TOOO: speaker note: our points are never collinear + +== 5 points must contain a 4-hole + +#slide(repeat: 10, self => [ + #let (uncover,) = utils.methods(self) + + *Theorem* (Klein 1932). // WN: I don't think a citation exists for this + Every set of 5 points in the plane contains a 4-hole. #pause + + _Proof._ By cases on the size of the convex hull. + + #components.side-by-side( + uncover("3-", align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05), + line: (stroke: config.colors.neutral-darkest)) + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 72deg, radius: 1), name: "b") + circle((angle: 144deg, radius: 1), name: "c") + circle((angle: 216deg, radius: 1), name: "d") + circle((angle: 290deg, radius: 1), name: "e") + }) + line("a", "b", "c", "d", "e", "a") + if 4 <= self.subslide { + line("a", "b", "c", "d", "a", fill: config.colors.primary.transparentize(20%)) + } + }))), + uncover("5-", align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05), + line: (stroke: config.colors.neutral-darkest)) + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 90deg, radius: 1), name: "b") + circle((angle: 180deg, radius: 1), name: "c") + circle((angle: 270deg, radius: 1), name: "d") + circle((angle: 60deg, radius: 0.5), name: "x") + }) + line("a", "b", "c", "d", "a") + if 7 <= self.subslide { + line("a", "d", "c", "x", "a", fill: config.colors.primary.transparentize(20%)) + } + if 6 <= self.subslide { + line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: (paint: config.colors.primary, thickness: 1.5pt, dash: "dashed")) + } + }))), + uncover("8-10", align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05), + line: (stroke: config.colors.neutral-darkest)) + let xθ = 20deg + let yθ = xθ + 180deg + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 120deg, radius: 1), name: "b") + circle((angle: 240deg, radius: 1), name: "c") + circle((angle: xθ, radius: 0.3), name: "x") + circle((angle: yθ, radius: 0.3), name: "y") + }) + line("a", "b", "c", "a") + if 9 <= self.subslide { + line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: (paint: config.colors.primary, thickness: 1.5pt, dash: "dashed")) + } + if 10 <= self.subslide { + line("a", "x", "y", "c", "a", fill: config.colors.primary.transparentize(20%)) + } + }))) + ) +]) + +== 9 points with no 5-holes + +#slide( + // Hide header by making it background-coloured + // config: config-colors(secondary: config.colors.neutral-lightest), + align: center+horizon, + repeat: 4, + self => cetz.canvas({ + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2), + line: (stroke: config.colors.neutral-darkest)) + scale(.1) + on-layer(1, { + let pts = ( + (1, 0, "a"), + (100, 0, "b"), + (51, 88, "c"), + + (30, 40, "d"), + (49, 10, "e"), + (70, 40, "f"), + + (45, 26, "g"), + (55, 26, "h"), + (50, 35, "i"), + ) + + for (x, y, n) in pts { + circle((x, y), name: n) + } + }) + if self.subslide > 1 { + line("a", "b", "c", "a") + line("d", "e", "f", "d") + line("g", "h", "i", "g") + } + if self.subslide == 3 { + line("a", "e", "h", "i", "d", "a", fill: config.colors.primary-light.transparentize(20%)) + content((25, -10), [5-hole ✘]) + content((25, -20), [convex 5-gon ✔]) + } + if self.subslide == 4 { + line("d", "e", "b", "h", "g", "d", fill: config.colors.primary-light.transparentize(20%)) + content((75, -10), [convex 5-gon ✘]) + } +})) + +== The Happy Ending Problem + +#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 + +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 6, + self => [ + #let (uncover, only, alternatives) = utils.methods(self) + #let mkalt(s, k, n) = alternatives( + $#s (#k) = #n$, + $#s (#k) ≤ #n$, $#s (#k) ≤ #n$, $#s (#k) ≤ #n$, + $#(n -1) < #s (#k)$, + $#s (#k) = #n$ + ) + #let mkbnd(s, k, n, c) = [#mkalt(s, k, n) #set text(size: 15pt);#c] + #table( + columns: (1.3fr, 1fr), + inset: 6pt, + stroke: none, + mkbnd("h", 3, 3, [(trivial)]), + mkbnd("g", 3, 3, [(trivial)]), + mkbnd("h", 4, 5, [(Klein 1932)]), + mkbnd("g", 4, 5, [(Klein 1932)]), + mkbnd("h", 5, 10, [@Harborth1978]), + mkbnd("g", 5, 9, [(Makai 1930s)]), + [*#mkbnd("h", 6, 30, [@03overmars_finding_sets_points_empty_convex_6_gons @24heule_happy_ending_empty_hexagon_every_set_30_points])*], + mkbnd("g", 6, 17, [@szekeres_peters_2006]), + ) + + #uncover("1, 6", [We formally verified all the above in #lean.]) + + #uncover("2-4, 6", [Upper bounds by combinatorial reduction to SAT.]) + #[ + #set par(first-line-indent: 1em, hanging-indent: 1em) + #uncover("2, 6", [▸ We focused on $h(6)$, established this year.])\ + #uncover("3, 6", [▸ $g(6)$ previously verified in Isabelle/HOL @19maric_fast_formal_proof_erdos_szekeres_conjecture_convex_polygons_most_six_points.])\ + #uncover("4, 6", [▸ Efficient SAT encoding of Heule & Scheucher speeds up $g(6)$ verification.]) + ] + + #uncover("5, 6", [Lower bounds by checking concrete sets of points.]) + ] +) + +== SAT-solving mathematics + +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 4, + self => [ + #let (uncover, only,) = utils.methods(self) + + #uncover("1, 3, 4", [ + *Reduction.* Show that a mathematical theorem is true + if a propositional formula φ is unsatisfiable. + ]) + + #uncover("1, 2, 4", [ + *Solving.* Show that φ is indeed unsatisfiable using a SAT solver. + ]) + + #uncover("2, 4", [ + ▸ Solving is reliable, reproducible, and trustworthy: + formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). + ]) + + #uncover("3, 4", [ + ▸ But reduction is problem-specific, and involves complex transformations: + _focus of our work_. + ]) + ] +) + +#let reduction-slide(step) = [ +== Reduction from geometry to SAT +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 1, + self => [ + #set text(size: 23pt) + #uncover(if step == 1 { "1" } else { "2" }, [ + 1. Discretize from continuous coordinates in $ℝ²$ to boolean variables. + ]) + #uncover(if step == 2 { "1" } else { "2" }, [ + 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 + ``` + ]) + #uncover(if step == 3 { "1" } else { "2" }, [ + 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 + ``` + 4. But $φ_30$ is unsatisfiable. + ```lean + axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat + ``` + ]) + ] +)] + +#reduction-slide(1) + +== Discretization with triple-orientations + +#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(20%)) + 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)) +})) + +#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 + +#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 + +#reduction-slide(2) + +== Symmetry breaking + +#[ + #set text(size: 22pt) + *Lemma*. WLOG we can assume that the points $(p_1, ..., p_n)$ are in _canonical form_, meaning that they satisfy the following properties: + + ▸ *($x$-order)* The points are sorted with respect to their $x$-coordinates,\ i.e., $(p_i)_x < (p_j)_x$ for all $1 ≤ i < j ≤ n$. + + ▸ *(CCW-order)* All orientations $σ(p_1, p_i, p_j)$, with $1 < i < j ≤ n$, are counterclockwise. + + ▸ *(Lex order)* The first half of list of adj. orientations is lex-below the second half: + $ [σ(p_(⌈n/2⌉+1), p_(⌈n/2⌉+2), p_(⌈n/2⌉+3)), ..., σ(p_(n-2), p_(n-1), p_n)] succ.eq \ + [σ(p_(⌈n/2⌉−1), p_(⌈n/2⌉), p_(⌈n/2⌉+1)), ..., σ(p_2, p_3, p_4)] $ +] + +#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: config.colors.secondary.transparentize(50%), 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(30%)) + // 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: 2pt, 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, + ) +]) + +// WN: Hid this slide, it doesn't add much +/* +== Symmetry breaking: result + +Points now in normal form. #pause + +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 +``` +*/ + +#reduction-slide(3) + +== Running the SAT solver + +CNF formula produced directly from executable #lean definition. #pause + +To verify $h(6) ≤ 30$:\ #pause +▸ CNF with 65#(thin)092 variables and 436#(thin)523 clauses\ #pause +▸ partitioned into 312#(thin)418 subproblems\ #pause +▸ each subproblem solved by CaDiCaL 1.9.5\ #pause +▸ unsatisfiability proofs checked on-the-fly by `cake_lpr`\ #pause +▸ 25#(thin)876.5 CPU hours on Bridges 2 cluster of Pittsburgh Supercomputing Center + +== Lower bounds + +To prove $n < h(k)$, +find a set of $n$ points with no $k$-holes. #pause + +Naive checker algorithm is $cal(O)(n^(k+1)log k)$ time. #pause + +We verified an $cal(O)(n^3)$ solution\ +from #cite(<90dobkin_searching_empty_convex_polygons>, form: "prose"). + +== Hole-finding algorithm + +#slide(align: center+horizon, repeat: 7, self => cetz.canvas({ + import cetz.draw: * + + let radius = 0.2 + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: radius)) + set-style(line: (stroke: (thickness: 3pt))) + let pts = ( + ((-9, -2), (-5, 7)), + ((7, -4), (18, -3), (16, 0), (12, 1), (23, 3), (11, 3), (17, 8), (9, 5), (2, 4)) + ) + let (left, right) = pts.map(pts => pts.map(((x, y)) => (x/2,y))) + let chain = (0, 3, 5, 7, 8).map(i => right.at(i)) + for (x, y) in left { + circle((x, y), radius: if self.subslide > 1 { 0.15 } else { radius }) + } + if self.subslide == 7 { + line(..((0,0), ..chain), fill: aqua.transparentize(30%), stroke: none) + } + if self.subslide > 1 { + line((0, -4), (0, 8), stroke: (dash: "dashed", paint: config.colors.neutral-darkest)) + } + if self.subslide == 5 { + line(right.at(0), right.at(3), stroke: (dash: "dashed", paint: aqua, thickness: 4pt)) + line(right.at(4), right.at(7), stroke: (dash: "dashed", paint: red, thickness: 4pt)) + } + if self.subslide == 6 { + line(..chain, stroke: (dash: "dashed", paint: aqua, thickness: 4pt)) + } + for (n, (x, y)) in ((0,0), ..right).enumerate() { + if self.subslide > 3 { + let (nx, ny) = if n < right.len() { right.at(n) } else { (0, 0) } + let thick = if self.subslide == 6 and n == 8 { 1pt } else { 4pt } + line((x, y), (nx, ny), stroke: (paint: config.colors.neutral-darkest, thickness: thick)) + } + if n != 0 { + if self.subslide == 3 { + line((x, y), (0, 0), stroke: (paint: config.colors.neutral-darkest)) + } + circle((x, y), name: str(n), radius: if self.subslide > 1 { 0.3 } else { radius }) + if self.subslide > 2 { + content((x, y), [#set text(fill: config.colors.neutral-lightest, size: 20pt); #str(n)]) + } + } + } + circle((0, 0), name: "p", radius: if self.subslide > 1 { 0.4 } else { radius }) + if self.subslide > 1 { + content((0, .13 /* HACK */), [#set text(fill: config.colors.neutral-lightest, size: 20pt); $p$]) + } +})) + +== Hole-finding algorithm: verification + +#align(center, [ +#image("./proof.png") #pause +expands to #pause +#[#set text(size: 15pt) +```lean +theorem of_proceed_loop + {i j : Fin n} (ij : Visible p pts i j) {Q : Queues n j} {Q_j : BelowList n j} {Q_i} (ha) + {IH} (hIH : ∀ a (ha : a < i), Visible p pts a j → ProceedIH p pts (ha.trans ij.1) (IH a ha)) + (Hj : Queues.OrderedTail p pts lo j (fun k h => Q.q[k.1]'(Q.sz ▸ h)) Q_j.1) + (ord : Queues.Ordered p pts lo i (fun k h => Q.q[k.1]'(Q.sz ▸ h.trans ij.1)) Q_i) + (g_wf : Q.graph.WF (VisibleLT p pts lo j)) + {Q' Q_j'} (eq : proceed.loop pts i j ij.1 IH Q Q_j Q_i ha = (Q', Q_j')) : + ∃ a Q₁ Q_i₁ Q_j₁, proceed.finish i j ij.1 Q₁ Q_i₁ Q_j₁ = (Q', Q_j') ∧ + Q₁.graph.WF (VisibleLT p pts i j) ∧ + (∀ k ∈ Q_i₁.1, σ (pts k) (pts i) (pts j) ≠ .ccw) ∧ + lo ≤ a ∧ Queues.Ordered p pts a i (fun k h => Q.q[k.1]'(Q.sz ▸ h.trans ij.1)) Q_i₁.1 ∧ + (∀ (k : Fin n) (h : k < j), ¬(lo ≤ k ∧ k < a) → Q₁.q[k.1]'(Q₁.sz ▸ h) = Q.q[k.1]'(Q.sz ▸ h)) ∧ + Queues.OrderedTail p pts a j (fun k h => Q₁.q[k.1]'(Q₁.sz ▸ h)) Q_j₁.1 := by +``` +] +]) + +== Lower bound: 29 points with no 6-holes @03overmars_finding_sets_points_empty_convex_6_gons + +#slide( + // Hide header by making it background-coloured + // config: config-colors(secondary: config.colors.neutral-lightest), + align: center+horizon, + repeat: 2, + self => cetz.canvas({ + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2), + line: (stroke: config.colors.neutral-darkest)) + scale(.1) + let pts = ( + (1.2, ((1-10, 1260+10), (37-10, 0-10), (1259+10, 320))), + (1.2, ((16, 743), (22, 531), (777, 194), (754, 697))), + (1.2, ((306, 592), (310, 531), (371, 487), (516, 467), (552, 502), (496, 579), (396, 613))), + (1.0, ((366, 552), (374, 525), (450, 498), (492, 502), (489, 537), (446, 565), (392, 575))), + (0.8, ((410, 539), (426, 526), (449, 518), (458, 526), (453, 542), (434, 552), (416, 550))), + (0.9, ((436, 535),)), + ) + on-layer(1, { + for (i, (radius, cycle)) in pts.enumerate() { + for (j, (x, y)) in cycle.enumerate() { + circle(((y+x/4)/5, x/11), radius: radius, name: str(i)+"-"+str(j)) + } + } + }) + if self.subslide > 1 { + for (i, (_, cycle)) in pts.enumerate() { + let cycle = range(cycle.len()) + cycle.push(0) + line(..cycle.map(x => str(i)+"-"+str(x))) + } + } +})) + +== Final theorem + +#[ +#set text(size: 24pt) +```lean +axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat + +theorem holeNumber_6 : holeNumber 6 = 30 := + le_antisymm + (hole_6_theorem' unsat_6hole_cnf) + (hole_lower_bound [ + (1, 1260), (16, 743), (22, 531), (37, 0), (306, 592), + (310, 531), (366, 552), (371, 487), (374, 525), (392, 575), + (396, 613), (410, 539), (416, 550), (426, 526), (434, 552), + (436, 535), (446, 565), (449, 518), (450, 498), (453, 542), + (458, 526), (489, 537), (492, 502), (496, 579), (516, 467), + (552, 502), (754, 697), (777, 194), (1259, 320)]) +``` +] + +== Conclusion + +We used Lean to fully verify a recent result in combinatorial geometry +based on a sophisticated reduction to SAT. #pause + +Upper and lower bounds for all finite _hole numbers_ $h(k)$ +followed with additional effort. #pause + +Open problems remain: + +▸ Horton's construction of $h(k) = ∞$ for $7 ≤ k$ hasn't been verified. #pause + +▸ Exact values of $g(k) < ∞$ for $7 ≤ k$ aren't known. #pause + +▸ Trust story for large SAT proofs could be improved. + +== Bibliography + +#bibliography("main.bib", style: "chicago-author-date", title: none) diff --git a/flake.lock b/flake.lock index fd85f3d..9b66e4e 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1705309234, - "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1705883077, - "narHash": "sha256-ByzHHX3KxpU1+V0erFy8jpujTufimh6KaS/Iv3AciHk=", + "lastModified": 1725534445, + "narHash": "sha256-Yd0FK9SkWy+ZPuNqUgmVPXokxDgMJoGuNpMEtkfcf84=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "5f5210aa20e343b7e35f40c033000db0ef80d7b9", + "rev": "9bb1e7571aadf31ddb4af77fc64b2d59580f9a39", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index cd8760d..d106b60 100644 --- a/flake.nix +++ b/flake.nix @@ -16,6 +16,7 @@ fontconfig gcc python3 + typst ]; FONTCONFIG_FILE = pkgs.makeFontsConf { fontDirectories = [