From 290e2cf5aaf28c79ff0327fc58a7e94c3c19cbb9 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 5 Sep 2024 21:44:06 -0400 Subject: [PATCH 01/22] feat: start on slides --- ITP/main.bib | 38 ++++++++ ITP/slides.typ | 248 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 286 insertions(+) create mode 100644 ITP/slides.typ diff --git a/ITP/main.bib b/ITP/main.bib index 53681cd..2fb4238 100644 --- a/ITP/main.bib +++ b/ITP/main.bib @@ -689,3 +689,41 @@ @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} +} \ No newline at end of file diff --git a/ITP/slides.typ b/ITP/slides.typ new file mode 100644 index 0000000..7c0f315 --- /dev/null +++ b/ITP/slides.typ @@ -0,0 +1,248 @@ +#import "@preview/touying:0.5.2": * +#import "@preview/cetz:0.2.2" +#import themes.university: * + +// Some slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf + +#show: university-theme.with( + config-info( + title: [Formal Verification of the Empty Hexagon Number], + author: [ + Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio,\ + Cayden Codel, *Mario Carneiro*, Marijn J. H. Heule + ], + date: [ + Interactive Theorem Proving | September 9th, 2024\ + Tbilisi, Georgia + ], + institution: [Carnegie Mellon University, USA] + ) +) + +#title-slide() + +== Empty $k$-gons + +Fix a set $S$ of points on the plane. +A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior. + +#components.side-by-side( + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: blue, 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), fill: black) + circle((angle: 240deg, radius: 1.5), fill: black) + }) + line("a", "b", "c", "d", "e", "a", fill: green) + content((0, -1.5), "5-hole ✔") + content((0, -2.0), "convex 5-gon ✔") + }), + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + on-layer(1, { + circle((angle: 0deg, 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), fill: black) + }) + line("a", "b", "c", "d", "a") + content((0, -1.5), "4-hole ✘") + content((0, -2.0), "convex 4-gon ✘") + }), + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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: 30deg, radius: 0.2), fill: black) + }) + line("a", "b", "c", "a") + content((0, -1.5), "3-hole ✘") + content((0, -2.0), "convex 3-gon ✔") + }), +) + +== Empty 4-gons + +#slide(repeat: 10, self => [ + #let (uncover,) = utils.methods(self) + + *Theorem* (Klein 1932). // WN: I don't think a citation exists for this + Every 5 points in the plane, no three collinear, + contain a 4-hole. #pause + + _Proof._ By cases on the size of the convex hull: 5, 4, or 3 points. + + #components.side-by-side( + uncover("3-", context align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: blue, 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") + }) + line("a", "b", "c", "d", "e", "a") + if 4 <= self.subslide { + line("a", "b", "c", "d", "a", fill: green) + } + }))), + uncover("5-", context align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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: green) + } + if 6 <= self.subslide { + line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: blue) + } + }))), + uncover("8-10", context align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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 10 <= self.subslide { + line("a", "x", "y", "c", "a", fill: green) + } + if 9 <= self.subslide { + line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: blue) + } + }))) + ) +]) + +== The Happy Ending Problem + +*Theorem* @35erdos_combinatorial_problem_geometry. +For a fixed $k$, every _sufficiently large_ set of points, +no three collinear, contains a convex $k$-gon. + +What about _$k$-holes_? + +*Theorem* @hortonSetsNoEmpty1983. +For any $k ≥ 7$, there exist arbitrarily large sets of points, +no three collinear, containing no $k$-holes. + +The $k$-th *hole number* $h(k)$ is the least number +such that any set of $h(k)$ points, +no three collinear, +necessarily contains a $k$-hole. + +Horton ⇒ $h(7) = h(8) = … = ∞$ + +== The Complete Story + +- $h(3) ≤ 3$ (trivial) ✔ +- $h(4) ≤ 5$ (Klein 1932) ✔ +- $h(5) ≤ 10$ @Harborth1978 ✔ +- *$bold(h(6) ≤ 30)$ @24heule_happy_ending_empty_hexagon_every_set_30_points* ✔ +- $29 < h(6)$ @03overmars_finding_sets_points_empty_convex_6_gons ✔ + +We formally verified all the above results using $L∃∀N$. +// TODO(WN): Should we stress more that +// verifying Heule/Scheucher was the hard part; and +// the other upper bounds follow from the encoding with not much effort; and +// then we also verified the pointset checker to establish lower bounds. + +Upper bounds via reduction to SAT. + +Lower bounds by checking explicit sets of points. + +== SAT-Solving Mathematics + +- *Reduction.* Show that the mathematical theorem of interest is true + if a concrete propositional formula φ is unsatisfiable. +- *Solving.* Show that φ is indeed unsatisfiable using a SAT solver. + +*Solving* is reliable, reproducible, and trustworthy: +formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). + +*Reduction* is problem-specific, and involves complex transformations: +focus of our work. + +== Reduction from Geometry to SAT + +#set text(size: 23pt) +1. Any set of points, no three collinear, + can be transformed into a _canonical form_ + without removing $k$-holes. + ```lean + theorem symmetry_breaking {l : List Point} : + 3 ≤ l.length → Point.ListInGenPos l → + ∃ w : CanonicalPoints, l ≼σ w.points + ``` +2. $n$ points in canonical form with no $k$-holes + induce a propositional assignment that satisfies $φ_n$. + ```lean + theorem satisfies_hexagonEncoding (w : CanonicalPoints) : + ¬σHasEmptyKGon 6 w.toFinset → + w.toPropAssn ⊨ hexagonEncoding w.rlen + ``` +3. $φ_30$ is unsatisfiable. + ```lean + axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1)).isUnsat + ``` + +// TODO: Marijn describes the entire encoding. Should we, +// or should we focus more on the verification; +// for example our adjusted symmetry breaking? + +== Lower Bounds + +Checker checker +// TODO: Say something about pointset checker verification + +== Final Theorem + +#rect(height: 100%)[ +#set text(size: 24pt) +```lean +axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1)).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) + ]) +``` +] + +== Bibliography + +#bibliography("main.bib", style: "chicago-author-date") \ No newline at end of file From 05687fd9ea0b4e4a861db0ccb292244c7ed7052d Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 7 Sep 2024 01:27:40 -0400 Subject: [PATCH 02/22] feat: more slides --- ITP/main.bib | 17 +++ ITP/slides.typ | 304 +++++++++++++++++++++++++++++++++---------------- flake.lock | 12 +- flake.nix | 1 + 4 files changed, 227 insertions(+), 107 deletions(-) diff --git a/ITP/main.bib b/ITP/main.bib index 2fb4238..0a72c5c 100644 --- a/ITP/main.bib +++ b/ITP/main.bib @@ -726,4 +726,21 @@ @article{03overmars_finding_sets_points_empty_convex_6_gons 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/slides.typ b/ITP/slides.typ index 7c0f315..2b4a8b3 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -1,93 +1,111 @@ #import "@preview/touying:0.5.2": * #import "@preview/cetz:0.2.2" -#import themes.university: * +#import themes.metropolis: * -// Some slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf +// Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf -#show: university-theme.with( - config-info( +#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, *Mario Carneiro*, Marijn J. H. Heule + Bernardo Subercaseaux¹, Wojciech Nawrocki¹, James Gallicchio¹,\ + Cayden Codel¹, *Mario Carneiro*#h(0em)¹, Marijn J. H. Heule¹ ], date: [ - Interactive Theorem Proving | September 9th, 2024\ + _Interactive Theorem Proving_ | September 9th, 2024\ Tbilisi, Georgia ], - institution: [Carnegie Mellon University, USA] + institution: [¹ Carnegie Mellon University, USA] + ), + ..config-colors( + primary: rgb("#eb811b"), + primary-light: rgb("#d6c6b7"), + secondary: rgb("#23373b"), + neutral-lightest: rgb("#fafafa"), + neutral-dark: rgb("#23373b"), + neutral-darkest: rgb("#23373b"), ) ) +#show: metropolis-theme.with(config) +#set text(size: 23pt) #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. -A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior. +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. -#components.side-by-side( +// PERTURB THE POINTS +#align(center, components.side-by-side( cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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), fill: black) - circle((angle: 240deg, radius: 1.5), fill: black) + circle((angle: 30deg, radius: 1.5)) + circle((angle: 240deg, radius: 1.5)) }) - line("a", "b", "c", "d", "e", "a", fill: green) + line("a", "b", "c", "d", "e", "a", fill: config.colors.primary.transparentize(20%)) content((0, -1.5), "5-hole ✔") content((0, -2.0), "convex 5-gon ✔") }), cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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: 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), fill: black) + circle((angle: 200deg, radius: 1.2)) }) - line("a", "b", "c", "d", "a") + line("a", "b", "c", "d", "a", fill: config.colors.primary-light.transparentize(20%)) content((0, -1.5), "4-hole ✘") content((0, -2.0), "convex 4-gon ✘") }), cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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: 120deg, radius: 1), name: "b") circle((angle: 240deg, radius: 1), name: "c") - circle((angle: 30deg, radius: 0.2), fill: black) + circle((angle: 30deg, radius: 0.2)) }) - line("a", "b", "c", "a") + line("a", "b", "c", "a", fill: config.colors.primary-light.transparentize(20%)) content((0, -1.5), "3-hole ✘") content((0, -2.0), "convex 3-gon ✔") }), -) +)) + +// TOOO: speaker note: our points are never collinear -== Empty 4-gons +== 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 5 points in the plane, no three collinear, - contain a 4-hole. #pause + Every 5 points in the plane contain a 4-hole. #pause - _Proof._ By cases on the size of the convex hull: 5, 4, or 3 points. + _Proof._ By cases on the size of the convex hull. #components.side-by-side( - uncover("3-", context align(center, cetz.canvas(length: 33%, { + uncover("3-", align(center, cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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") @@ -97,13 +115,13 @@ A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior. }) line("a", "b", "c", "d", "e", "a") if 4 <= self.subslide { - line("a", "b", "c", "d", "a", fill: green) + line("a", "b", "c", "d", "a", fill: config.colors.primary.transparentize(20%)) } }))), - uncover("5-", context align(center, cetz.canvas(length: 33%, { + uncover("5-", align(center, cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + 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: 90deg, radius: 1), name: "b") @@ -113,16 +131,16 @@ A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior. }) line("a", "b", "c", "d", "a") if 7 <= self.subslide { - line("a", "d", "c", "x", "a", fill: green) + 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: blue) + line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: config.colors.primary) } }))), - uncover("8-10", context align(center, cetz.canvas(length: 33%, { + uncover("8-10", align(center, cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: blue, stroke: none, radius: 0.05)) + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) let xθ = 20deg let yθ = xθ + 180deg on-layer(1, { @@ -133,103 +151,188 @@ A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior. circle((angle: yθ, radius: 0.3), name: "y") }) line("a", "b", "c", "a") - if 10 <= self.subslide { - line("a", "x", "y", "c", "a", fill: green) - } if 9 <= self.subslide { - line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: blue) + line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: config.colors.primary) + } + if 10 <= self.subslide { + line("a", "x", "y", "c", "a", fill: config.colors.primary.transparentize(20%)) } }))) ) ]) -== The Happy Ending Problem +== 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)) + 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 ✘]) + } +})) + +/////////// DONE ABOVE +/////////// WORK AREA BELOW -*Theorem* @35erdos_combinatorial_problem_geometry. -For a fixed $k$, every _sufficiently large_ set of points, -no three collinear, contains a convex $k$-gon. +== The Happy Ending Problem -What about _$k$-holes_? +// TODO(WN): make #pause-gray gray out the things that came before -*Theorem* @hortonSetsNoEmpty1983. -For any $k ≥ 7$, there exist arbitrarily large sets of points, -no three collinear, containing no $k$-holes. +$g(k) =$ least $n$ s.t. any set of $n$ points must contain a *convex $bold(k)$-gon* -The $k$-th *hole number* $h(k)$ is the least number -such that any set of $h(k)$ points, -no three collinear, -necessarily contains a $k$-hole. +$h(k) =$ least $n$ s.t. any set of $n$ points must contain a *$bold(k)$-hole* #pause -Horton ⇒ $h(7) = h(8) = … = ∞$ +We just showed $h(4) ≤ 5$ and $9 < h(5)$. #pause -== The Complete Story +*Theorem* @35erdos_combinatorial_problem_geometry. +For a fixed $k$, every _sufficiently large_ set of points contains a convex $k$-gon. +So $g(k)$ is finite. #pause -- $h(3) ≤ 3$ (trivial) ✔ -- $h(4) ≤ 5$ (Klein 1932) ✔ -- $h(5) ≤ 10$ @Harborth1978 ✔ -- *$bold(h(6) ≤ 30)$ @24heule_happy_ending_empty_hexagon_every_set_30_points* ✔ -- $29 < h(6)$ @03overmars_finding_sets_points_empty_convex_6_gons ✔ +*Theorem* @hortonSetsNoEmpty1983. +For any $k ≥ 7$, there exist arbitrarily large sets of points containing no $k$-holes. +So $h(7) = h(8) = … = ∞$. + +== The complete story + +#table( + columns: (auto, auto), + inset: 5pt, + stroke: none, + [$h(3) = 3$ (trivial)], + [$g(3) = 3$ (trivial)], + [$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)], + [*$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 + +Upper bounds by combinatorial reduction to SAT. #pause + +#[ +#set par(first-line-indent: 1em, hanging-indent: 1em) +▸ We focused on $h(6)$.\ #pause +▸ $g(6)$ previously verified in Isabelle/HOL @10maric_formal_verification_modern_sat_solver_shallow_embedding_isabelle_hol.\ #pause +▸ Efficient SAT encoding of Heule & Scheucher speeds up $g(6)$ verification. #pause +] -We formally verified all the above results using $L∃∀N$. -// TODO(WN): Should we stress more that -// verifying Heule/Scheucher was the hard part; and -// the other upper bounds follow from the encoding with not much effort; and -// then we also verified the pointset checker to establish lower bounds. +Lower bounds by checking explicit sets of points. + // TODO: Is this the first verification of the hole-tester algo? -Upper bounds via reduction to SAT. +== SAT-solving mathematics -Lower bounds by checking explicit sets of points. +*Reduction.* Show that a mathematical theorem is true +if a propositional formula φ is unsatisfiable. -== SAT-Solving Mathematics +*Solving.* Show that φ is indeed unsatisfiable using a SAT solver. #pause -- *Reduction.* Show that the mathematical theorem of interest is true - if a concrete propositional formula φ is unsatisfiable. -- *Solving.* Show that φ is indeed unsatisfiable using a SAT solver. +▸ Solving is reliable, reproducible, and trustworthy: +formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). #pause -*Solving* is reliable, reproducible, and trustworthy: -formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). +▸ But reduction is problem-specific, and involves complex transformations: +_focus of our work_. -*Reduction* is problem-specific, and involves complex transformations: -focus of our work. +== Reduction from geometry to SAT -== Reduction from Geometry to SAT +// TODO: make text shorter +// TODO(WN): pauses for the list #set text(size: 23pt) -1. Any set of points, no three collinear, - can be transformed into a _canonical form_ +1. Points can be put in _canonical form_ without removing $k$-holes. ```lean - theorem symmetry_breaking {l : List Point} : - 3 ≤ l.length → Point.ListInGenPos l → - ∃ w : CanonicalPoints, l ≼σ w.points - ``` -2. $n$ points in canonical form with no $k$-holes + 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.toFinset → - w.toPropAssn ⊨ hexagonEncoding w.rlen - ``` -3. $φ_30$ is unsatisfiable. - ```lean - axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1)).isUnsat - ``` + ```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 + ``` + +== 1. Symmetry breaking + +// TODO: add teh content + +The sequence of six steps from Fig. 5 +(transformation into `CanonicalPoints`); +make it an animation. + -// TODO: Marijn describes the entire encoding. Should we, -// or should we focus more on the verification; -// for example our adjusted symmetry breaking? +== 2. SAT encoding -== Lower Bounds +// TODO: add teh content -Checker checker -// TODO: Say something about pointset checker verification +- Introduce $σ$ variables +- Show scary picture of full encoding (?) +- Talk about cap-cup clauses; copy slide 14/21 from Marijn -== Final Theorem +== 3. Running the SAT solver + +// TODO: add teh content + +How many clauses, how long it took, cluster compute amount (from 'Running the CNF') + +== Lower bounds + +// TODO(MARIO): put someting in this slide, without describing the algorithm +// TODO(Bernardo): draw pictures of the algorithm + +$cal(O)("sth")$ time, $cal(O)("sth")$ space algorithm @90dobkin_searching_empty_convex_polygons + +We verified it, and used it to check the lower bounds. + +== Final theorem -#rect(height: 100%)[ #set text(size: 24pt) ```lean -axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1)).isUnsat +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 [ @@ -241,8 +344,7 @@ theorem holeNumber_6 : holeNumber 6 = 30 := (552, 502), (754, 697), (777, 194), (1259, 320) ]) ``` -] == Bibliography -#bibliography("main.bib", style: "chicago-author-date") \ No newline at end of file +#bibliography("main.bib", style: "chicago-author-date", title: none) \ No newline at end of file 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 = [ From 99b245ebc7bb3c4f58189eb35f573da6f0b00637 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 7 Sep 2024 01:32:44 -0400 Subject: [PATCH 03/22] minor --- ITP/slides.typ | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ITP/slides.typ b/ITP/slides.typ index 2b4a8b3..ee959d2 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -330,6 +330,7 @@ We verified it, and used it to check the lower bounds. == Final theorem +#[ #set text(size: 24pt) ```lean axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat @@ -344,6 +345,7 @@ theorem holeNumber_6 : holeNumber 6 = 30 := (552, 502), (754, 697), (777, 194), (1259, 320) ]) ``` +] == Bibliography From 37c1bd934b5699c61bf2ab5d21c263591e104260 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 7 Sep 2024 01:35:27 -0400 Subject: [PATCH 04/22] fix: wording --- ITP/slides.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index ee959d2..8435a5f 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -222,13 +222,13 @@ 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 $g(k)$ is finite. #pause +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) = … = ∞$. -== The complete story +== Known tight bounds #table( columns: (auto, auto), From 81a0c800406c06492124bd7520aa9740b2c051d2 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 8 Sep 2024 03:40:51 -0400 Subject: [PATCH 05/22] feat: pictures --- ITP/slides.typ | 311 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 254 insertions(+), 57 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 8435a5f..c20faf7 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -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 = ( @@ -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: * @@ -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") @@ -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)) @@ -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, @@ -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 @@ -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 From 357d79fdf01f8ab2e3fa4a713bd80198e619ab7c Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 8 Sep 2024 03:45:53 -0400 Subject: [PATCH 06/22] fix: clause count --- ITP/slides.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index c20faf7..46a032e 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -510,7 +510,7 @@ structure CanonicalPoints where CNF formula produced directly from executable #lean definition. #pause To verify $h(6) ≤ 30$:\ #pause -▸ CNF with 444215 clauses\ #pause +▸ CNF with 65092 variables and 436523 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 From e671f81ae6fe5c826db9ac2af47961591ee5d597 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 9 Sep 2024 12:27:07 -0400 Subject: [PATCH 07/22] fix: colors --- ITP/Monokai Dark.tmTheme | 410 +++++++++++++++++++++++++++++++++++++++ ITP/slides.typ | 43 ++-- 2 files changed, 434 insertions(+), 19 deletions(-) create mode 100644 ITP/Monokai Dark.tmTheme 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/slides.typ b/ITP/slides.typ index 46a032e..28b297c 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -33,7 +33,7 @@ } } -#let lean = $"L∃∀N"$ +#let lean = "Lean" // Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf @@ -53,16 +53,17 @@ institution: [¹ Carnegie Mellon University, USA] ), ..config-colors( - primary: rgb("#eb811b"), + primary: rgb("#fb912b"), primary-light: rgb("#d6c6b7"), - secondary: rgb("#23373b"), - neutral-lightest: rgb("#fafafa"), - neutral-dark: rgb("#23373b"), - neutral-darkest: rgb("#23373b"), + 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() @@ -88,7 +89,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. 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%)) + 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 ✔") }), @@ -102,7 +103,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. 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%)) + 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 ✘") }), @@ -115,7 +116,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. 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%)) + 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 ✔") }), @@ -137,7 +138,8 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. uncover("3-", align(center, cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + 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") @@ -153,7 +155,8 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. uncover("5-", align(center, cetz.canvas(length: 33%, { import cetz.draw: * - set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + 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") @@ -166,13 +169,14 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. 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: config.colors.primary) + line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: (paint: config.colors.primary, thickness: 2pt)) } }))), 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)) + 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, { @@ -184,7 +188,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. }) line("a", "b", "c", "a") if 9 <= self.subslide { - line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: config.colors.primary) + line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: (paint: config.colors.primary, thickness: 2pt)) } if 10 <= self.subslide { line("a", "x", "y", "c", "a", fill: config.colors.primary.transparentize(20%)) @@ -202,7 +206,8 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. repeat: 4, self => cetz.canvas({ import cetz.draw: * - set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2)) + 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 = ( @@ -354,7 +359,7 @@ _focus of our work_. } }) - let (cg, cb, cr) = (green, blue, red).map(c => c.desaturate(50%)) + 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)) @@ -414,7 +419,7 @@ _focus of our work_. 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")) + 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)) @@ -439,7 +444,7 @@ _focus of our work_. // Convex regions on-layer(-1, { set-style(line: (stroke: none)) - let colors = (red, orange, blue, green).map(c => c.transparentize(70%)) + 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) @@ -465,7 +470,7 @@ _focus of our work_. 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))) + set-style(line: (stroke: (thickness: 2pt, dash: "dashed", paint: red))) line((x4, yf), (x4, yt)) line((x6, yf), (x6, yt)) } From 4c6919ac7ee7e2c4634429a6f2426e50478cd59d Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 9 Sep 2024 12:30:49 -0400 Subject: [PATCH 08/22] dash --- ITP/slides.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 28b297c..9eb3e6a 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -169,7 +169,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. 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: 2pt)) + 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%, { @@ -188,7 +188,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. }) 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: 2pt)) + 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%)) From acf7656bdc16edfc66d79c497539dd6f5a98143b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 9 Sep 2024 15:27:38 +0400 Subject: [PATCH 09/22] slide tweaks --- ITP/slides.typ | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 9eb3e6a..c84ef6b 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -25,7 +25,7 @@ line((x, fly), (x, tly), ..style) x += step } - + let y = fy while y <= ty + eps { line((flx, y), (tlx, y), ..style) @@ -34,6 +34,7 @@ } #let lean = "Lean" +#let thin = h(3em/18) // Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf @@ -44,7 +45,7 @@ title: [Formal Verification of the Empty Hexagon Number], author: [ Bernardo Subercaseaux¹, Wojciech Nawrocki¹, James Gallicchio¹,\ - Cayden Codel¹, *Mario Carneiro*#h(0em)¹, Marijn J. H. Heule¹ + Cayden Codel¹, #underline[Mario Carneiro]#h(0em)¹, Marijn J. H. Heule¹ ], date: [ _Interactive Theorem Proving_ | September 9th, 2024\ @@ -130,7 +131,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. #let (uncover,) = utils.methods(self) *Theorem* (Klein 1932). // WN: I don't think a citation exists for this - Every 5 points in the plane contain a 4-hole. #pause + Every set of 5 points in the plane contains a 4-hole. #pause _Proof._ By cases on the size of the convex hull. @@ -348,7 +349,7 @@ _focus of our work_. 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") @@ -358,7 +359,7 @@ _focus of our work_. 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)) @@ -412,7 +413,7 @@ _focus of our work_. ) scale(3.2) - + // Grid and axes let ((efx, efy), (etx, ety)) = extents.at(self.subslide - 1) on-layer(-1, { @@ -464,7 +465,7 @@ _focus of our work_. line(..r, fill: c) } }) - + // Equal-x marker lines if self.subslide == 1 { let ((_, yf), (_, yt)) = extents.at(0) @@ -475,7 +476,7 @@ _focus of our work_. line((x6, yf), (x6, yt)) } }) - + #let captions = ( [Starting set of points.], [Rotation ensures distinct $x$.], @@ -515,11 +516,11 @@ structure CanonicalPoints where CNF formula produced directly from executable #lean definition. #pause To verify $h(6) ≤ 30$:\ #pause -▸ CNF with 65092 variables and 436523 clauses\ #pause -▸ partitioned into 312 418 subproblems\ #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 876.5 CPU hours on Bridges 2 cluster of Pittsburgh Supercomputing Center +▸ 25#(thin)876.5 CPU hours on Bridges 2 cluster of Pittsburgh Supercomputing Center == Lower bounds @@ -538,17 +539,18 @@ We verified it, and used it to check the lower bounds. 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 [ + 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) - ]) + (552, 502), (754, 697), (777, 194), (1259, 320)]) ``` ] == Bibliography -#bibliography("main.bib", style: "chicago-author-date", title: none) \ No newline at end of file +#bibliography("main.bib", style: "chicago-author-date", title: none) From 25743f00b0d4731b97a34f1e12316882c590780b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 9 Sep 2024 15:27:56 +0400 Subject: [PATCH 10/22] add another diagram for the 29 point configuration --- ITP/slides.typ | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/ITP/slides.typ b/ITP/slides.typ index c84ef6b..1c84e38 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -551,6 +551,39 @@ theorem holeNumber_6 : holeNumber 6 = 30 := ``` ] +#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)) + 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))) + } + } +})) + == Bibliography #bibliography("main.bib", style: "chicago-author-date", title: none) From 1efa4ce22dd2a31699abf489aeb9a04094a853fa Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 9 Sep 2024 16:01:52 -0400 Subject: [PATCH 11/22] shape --- ITP/slides.typ | 45 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 5 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 1c84e38..c937a47 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -524,12 +524,46 @@ To verify $h(6) ≤ 30$:\ #pause == Lower bounds -// TODO(MARIO): put someting in this slide, without describing the algorithm -// TODO(Bernardo): draw pictures of the algorithm +// TODO(Bernardo): draw pictures of the algorithm <----- -$cal(O)("sth")$ time, $cal(O)("sth")$ space algorithm @90dobkin_searching_empty_convex_polygons +For $… < h(k)$, we verified algorithm to look for all $k$-holes. + +Naive solution is $cal(O)(n^(k+1)log k)$ time. + +We verified an $cal(O)(n^3)$ algorithm from @90dobkin_searching_empty_convex_polygons. + +#align(center, cetz.canvas({ + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.2)) + circle((0, 0), name: "p") + content((0, 0), [$p$]) + + let pts = ( + // TODO not collinear + (-3, 0), (-4, 2), + + // TODO sort ccw around p + (1, 0), + (5, 1), + (5, 2), + (6, 3), + (7, 5), + (4, 3.5), + (3, 4), + ) + for (n, (x, y)) in pts.enumerate() { + circle((x, y), name: str(n)) + if n > 1 { + line((0, 0), (x, y), stroke: config.colors.neutral-darkest) + if n + 1 < pts.len() { + let (nx, ny) = pts.at(n + 1) + line((x,y), (nx, ny), stroke: config.colors.neutral-darkest) + } + } + } +})) -We verified it, and used it to check the lower bounds. == Final theorem @@ -558,7 +592,8 @@ theorem holeNumber_6 : holeNumber 6 = 30 := repeat: 2, self => cetz.canvas({ import cetz.draw: * - set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2)) + 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))), From f5d9fc7cbbf8d2fafc9691193c66cfba7a3bc4fc Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 10 Sep 2024 01:37:26 +0400 Subject: [PATCH 12/22] diagram for the lower bound algo --- ITP/slides.typ | 72 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 28 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index c937a47..58cbec2 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -524,44 +524,60 @@ To verify $h(6) ≤ 30$:\ #pause == Lower bounds -// TODO(Bernardo): draw pictures of the algorithm <----- - -For $… < h(k)$, we verified algorithm to look for all $k$-holes. +To prove theorems of the form $n <= h(k)$, we must show that there is a set of $n-1$ points with no $k$-holes. Naive solution is $cal(O)(n^(k+1)log k)$ time. -We verified an $cal(O)(n^3)$ algorithm from @90dobkin_searching_empty_convex_polygons. +We verified an $cal(O)(n^3)$ algorithm from\ @90dobkin_searching_empty_convex_polygons. -#align(center, cetz.canvas({ +#slide(align: center+horizon, repeat: 7, self => cetz.canvas({ import cetz.draw: * - - set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.2)) - circle((0, 0), name: "p") - content((0, 0), [$p$]) - + + let radius = 0.2 + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: radius)) + set-style(line: (stroke: (thickness: 3pt))) let pts = ( - // TODO not collinear - (-3, 0), (-4, 2), - - // TODO sort ccw around p - (1, 0), - (5, 1), - (5, 2), - (6, 3), - (7, 5), - (4, 3.5), - (3, 4), + ((-9, -2), (-5, 7)), + ((2, 4), (9, 5), (17, 8), (12, 3), (23, 3), (12, 1), (16, 0), (18, -3), (7, -4)) ) - for (n, (x, y)) in pts.enumerate() { - circle((x, y), name: str(n)) - if n > 1 { - line((0, 0), (x, y), stroke: config.colors.neutral-darkest) - if n + 1 < pts.len() { - let (nx, ny) = pts.at(n + 1) - line((x,y), (nx, ny), stroke: config.colors.neutral-darkest) + let (left, right) = pts.map(pts => pts.map(((x, y)) => (x/2,y))) + let chain = (0, 1, 3, 5, 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(1), right.at(4), 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 == 1 { 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$]) + } })) From eab4d312c661d8807280257961b7ba8dfd2ab97a Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 10 Sep 2024 01:43:41 +0400 Subject: [PATCH 13/22] perturb x corrds --- ITP/slides.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 58cbec2..6191baf 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -538,7 +538,7 @@ We verified an $cal(O)(n^3)$ algorithm from\ @90dobkin_searching_empty_convex_po set-style(line: (stroke: (thickness: 3pt))) let pts = ( ((-9, -2), (-5, 7)), - ((2, 4), (9, 5), (17, 8), (12, 3), (23, 3), (12, 1), (16, 0), (18, -3), (7, -4)) + ((2, 4), (9, 5), (17, 8), (11, 3), (23, 3), (12, 1), (16, 0), (18, -3), (7, -4)) ) let (left, right) = pts.map(pts => pts.map(((x, y)) => (x/2,y))) let chain = (0, 1, 3, 5, 8).map(i => right.at(i)) From 506e60b2740ce3b457be0ea1b69e3b8a3604f47d Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 10 Sep 2024 01:49:54 +0400 Subject: [PATCH 14/22] ccw goes the other way --- ITP/slides.typ | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 6191baf..25f8aa1 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -538,10 +538,10 @@ We verified an $cal(O)(n^3)$ algorithm from\ @90dobkin_searching_empty_convex_po set-style(line: (stroke: (thickness: 3pt))) let pts = ( ((-9, -2), (-5, 7)), - ((2, 4), (9, 5), (17, 8), (11, 3), (23, 3), (12, 1), (16, 0), (18, -3), (7, -4)) + ((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, 1, 3, 5, 8).map(i => right.at(i)) + 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 }) } @@ -553,7 +553,7 @@ We verified an $cal(O)(n^3)$ algorithm from\ @90dobkin_searching_empty_convex_po } if self.subslide == 5 { line(right.at(0), right.at(3), stroke: (dash: "dashed", paint: aqua, thickness: 4pt)) - line(right.at(1), right.at(4), stroke: (dash: "dashed", paint: red, 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)) @@ -561,7 +561,7 @@ We verified an $cal(O)(n^3)$ algorithm from\ @90dobkin_searching_empty_convex_po 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 == 1 { 1pt } else { 4pt } + 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 { From 0c2c0e5f4a052aa6451ade4cc230c90b9db799fa Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 00:32:33 -0400 Subject: [PATCH 15/22] fix: citation --- ITP/slides.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 25f8aa1..ea8daa9 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -296,7 +296,7 @@ Upper bounds by combinatorial reduction to SAT. #pause #[ #set par(first-line-indent: 1em, hanging-indent: 1em) ▸ We focused on $h(6)$.\ #pause -▸ $g(6)$ previously verified in Isabelle/HOL @10maric_formal_verification_modern_sat_solver_shallow_embedding_isabelle_hol.\ #pause +▸ $g(6)$ previously verified in Isabelle/HOL @19maric_fast_formal_proof_erdos_szekeres_conjecture_convex_polygons_most_six_points.\ #pause ▸ Efficient SAT encoding of Heule & Scheucher speeds up $g(6)$ verification. #pause ] From 9c20010dec2a1078d7325788795b910ea85e1452 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 00:43:32 -0400 Subject: [PATCH 16/22] feat: add conclusion --- ITP/main.bib | 15 ++------------- ITP/slides.typ | 16 ++++++++++++++++ 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/ITP/main.bib b/ITP/main.bib index 0a72c5c..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}, @@ -706,8 +695,8 @@ @inproceedings{24heule_happy_ending_empty_hexagon_every_set_30_points 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}, + 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} diff --git a/ITP/slides.typ b/ITP/slides.typ index ea8daa9..bb00698 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -635,6 +635,22 @@ theorem holeNumber_6 : holeNumber 6 = 30 := } })) +== 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 some additional effort. #pause + +Open problems remain: + +▸ Horton's construction for $h(7) = h(8) = … = ∞$ has not 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) From b4d485aad23dd89b02068c7168984ca2c7b060cc Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 00:44:11 -0400 Subject: [PATCH 17/22] Wording and titles --- ITP/slides.typ | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index bb00698..3cc624f 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -524,11 +524,15 @@ To verify $h(6) ≤ 30$:\ #pause == Lower bounds -To prove theorems of the form $n <= h(k)$, we must show that there is a set of $n-1$ points with no $k$-holes. +To prove $n < h(k)$, +find a set of $n$ points with no $k$-holes. #pause -Naive solution is $cal(O)(n^(k+1)log k)$ time. +Naive checker algorithm is $cal(O)(n^(k+1)log k)$ time. #pause -We verified an $cal(O)(n^3)$ algorithm from\ @90dobkin_searching_empty_convex_polygons. +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: * @@ -601,6 +605,8 @@ theorem holeNumber_6 : holeNumber 6 = 30 := ``` ] +== Lower bound: 29 points with no 6-holes + #slide( // Hide header by making it background-coloured // config: config-colors(secondary: config.colors.neutral-lightest), From 150daf0f3bdc7710da9f4c402bb751193cbaa515 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 01:05:51 -0400 Subject: [PATCH 18/22] tRaNsItIoNs --- ITP/slides.typ | 151 +++++++++++++++++++++++++++++++------------------ 1 file changed, 95 insertions(+), 56 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 3cc624f..e2691af 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -273,75 +273,110 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. == Known tight bounds -// TODO: This slide is too wordy - -#table( - columns: (auto, auto), - inset: 5pt, - stroke: none, - [$h(3) = 3$ (trivial)], - [$g(3) = 3$ (trivial)], - [$h(4) = 5$ (Klein 1932)], - [$g(4) = 5$ (Klein 1932)], - [$h(5) = 10$ @Harborth1978], - [$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 #lean. #pause +#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]), + ) -Upper bounds by combinatorial reduction to SAT. #pause + #uncover("1, 6", [We formally verified all the above in #lean.]) -#[ -#set par(first-line-indent: 1em, hanging-indent: 1em) -▸ We focused on $h(6)$.\ #pause -▸ $g(6)$ previously verified in Isabelle/HOL @19maric_fast_formal_proof_erdos_szekeres_conjecture_convex_polygons_most_six_points.\ #pause -▸ Efficient SAT encoding of Heule & Scheucher speeds up $g(6)$ verification. #pause -] + #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.]) + ] -Lower bounds by checking explicit sets of points. - // TODO: Is this the first verification of the hole-tester algo? + #uncover("5, 6", [Lower bounds by checking concrete sets of points.]) + ] +) == SAT-solving mathematics -*Reduction.* Show that a mathematical theorem is true -if a propositional formula φ is unsatisfiable. +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 4, + self => [ + #let (uncover, only,) = utils.methods(self) -*Solving.* Show that φ is indeed unsatisfiable using a SAT solver. #pause + #uncover("1, 3, 4", [ + *Reduction.* Show that a mathematical theorem is true + if a propositional formula φ is unsatisfiable. + ]) -▸ Solving is reliable, reproducible, and trustworthy: -formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). #pause + #uncover("1, 2, 4", [ + *Solving.* Show that φ is indeed unsatisfiable using a SAT solver. + ]) -▸ But reduction is problem-specific, and involves complex transformations: -_focus of our work_. + #uncover("2, 4", [ + ▸ Solving is reliable, reproducible, and trustworthy: + formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). + ]) -== Reduction from geometry to SAT + #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: (self: none, body) => box(scale(x: 0%, body))), + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 1, 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 - ``` + #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 @@ -382,6 +417,8 @@ _focus of our work_. // WN: I think cap-cup here would be too deep into the weeds +#reduction-slide(2) + == Symmetry breaking #slide(repeat: 6, align: center+horizon, self => [ @@ -511,6 +548,8 @@ structure CanonicalPoints where lex : σRevLex rest ``` +#reduction-slide(3) + == Running the SAT solver CNF formula produced directly from executable #lean definition. #pause @@ -647,11 +686,11 @@ 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 some additional effort. #pause +followed with additional effort. #pause Open problems remain: -▸ Horton's construction for $h(7) = h(8) = … = ∞$ has not been verified. #pause +▸ Horton's construction for $h(7) = h(8) = … = ∞$ hasn't been verified. #pause ▸ Exact values of $g(k)$ for $7 ≤ k$ aren't known. #pause From c66665109ac6bcdea9f20ce3e55efb1321a9d8da Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 01:17:44 -0400 Subject: [PATCH 19/22] clearly --- ITP/slides.typ | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index e2691af..0d6dbf4 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -531,7 +531,8 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. ) ]) -// TODO: Maybe rm this slide? It's not adding much +// WN: Hid this slide, it doesn't add much +/* == Symmetry breaking: result Points now in normal form. #pause @@ -547,6 +548,7 @@ structure CanonicalPoints where oriented : rest.Pairwise (σ leftmost · · = .ccw) lex : σRevLex rest ``` +*/ #reduction-slide(3) @@ -623,6 +625,29 @@ from #cite(<90dobkin_searching_empty_convex_polygons>, form: "prose"). } })) +== 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 +``` +] +]) == Final theorem From 14c16d41e698aca45d24b66d83af19f9dadfd1cd Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 01:19:08 -0400 Subject: [PATCH 20/22] fig --- ITP/proof.png | Bin 0 -> 32305 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 ITP/proof.png diff --git a/ITP/proof.png b/ITP/proof.png new file mode 100644 index 0000000000000000000000000000000000000000..f0b9757b5cf3f48a503b9efc7cf80e3486377c3d GIT binary patch literal 32305 zcmZ^}1y~$Q(>A<|1$TFc;1b+D1Pku65ZqyL4=zE2ySrQP;O_200*gBYOTNuH@B4hu z^~?0t(>*<1E!8#MRd-F~M`bxQWMX6h0Dva{URn(RfNh874GozPyOoi@~WcYJFe-G@=m(1yGHpue!sXLh*?f$w>_W( zDj2?*I^$O$h_^6mW8*=_)8gYtDBWPWUdmyGOvZoyjL^lx$_J$6-(URPL<<~Qt90k8 z4!HlbTrfqje+dw$rc~ZJylkKnMFbcP;wZQPDaSnLkJ?O$!tksArjI8V0rOmlu49Cah!;K{1+Pd95JUk!nv0(%XNx3bICBkX&B&tG zE9RzO2P>~_zf%w6Y1?Q5Ri#CD#=nLL?6RCs{NX11)A7ktKHOL5dqox-QdHt3(ZQM4 z!2%|cR@gV~uh{tL^#}tLA--)Q1B^U|#JH7pa(7+=c4^#sX!WqUCj>C{q65H!s=65o zQ94b+??Hq$nBXvuR2g$RE6cjef;w((-a$s@00z9R7!Lk$Rb z#-%9y!B1%){Jj;02Q(rkuS1+cn3dvoxk*H1Tvps{V%cQ8pJ);%Osw6PqXqLO*7|0v+5)|#rQ<%-zQL1B@ZVLV;p`q#E;OamlFJ(g_JMlx`Xoa zg6BHi4qvbWk;ul_HP~hx)X8F+iXvX{H7? z!w#-Cb1uKmNO($rQ-;uPDn*2_m4!Jbx9JaWFva;$9@${fXEoW6zKmL8aT@ii&g5DNKc9wQ7)_Ok zruclm9a{c5rD&KAw;!2KSus5YxZ?{&W)H`jq6G%=n0?V9aaRlr*IveXJSM)zr;B62 zIY#`m;|Q4=<4WKAcrvqhDKneOoJQp%3wy6|r5MS0u-{cBKA!fhOH?Ce(U~0T9l7gMbk0d-ypMxN?Zx`e)}N3lFDT@GF4dBaI<>|1H0P zJJt8n5T*_5_V1W!FwFcEaz9{%12Hb&^iq-z1j2C;$>yRjx4|jCY3zmh2>0PTavg$3 z;1?5=6`*_YYaWmko}rh>3CjRsx!3TUcl&pgnKxTO(}P!VZ6{SvL>@8C{G86F33EIYf+OVkc|TOr5hp) z#Mx*rXek(ssl;dkO3G9x-kyJTLeAw%YRGCxo|A5qJ}U4nsZeJv&siX}L2v^$XX(j_ zD0RvC6&4kJD%dZ^K6Xat0Qwy{;U=L zI|@B&*3_05Eh!-xAMxirN$q;=ow7^KgK~|Eg-QceuksJ7Jlf{v%371!tm-0p-tx`b zUkWVphqU%8CN(QHgsR-ttBtd3L}f(`MD+d2pOo)zjyH*E(NNF=(7I*whw#6s6UQA9 zZhoCAxq+Y@=^vFI8D>Z;DJaESgjqx$I83@vin5}yGF0uBGjt5zvhLbS$efSuyr{G`VN3#&Kw6nUg z2&6owG^adNS!r!)%~w@a*XZI@r!S>1om8{0=kZSQ9`PpgrrN3M6X@rkd9TN+hNwCe zN*7khZ8oX5n63U?U0f4sT5iE;X0LOs3lLbd1MfnT3#Vg$AN)9t|5>-Vb58h$v)2rH z=-n5uGpoH3*D7!)ZwfE3$!TZ(7c*mlRY9aIUj9v&5}`N`qy3HDm&L(FnO(KRxjmbM zj8naz-bv-7F(z#0Ij%I{9@{5fg^urMHwQ(Q{d%5_$=%7*$%RDPhjn9dV%7!E>q{dU zmR%byO9}d!S8bEDOIz#tmOIv-6XMD-wklwyJ5!{s}-@Er)#NDgSK z=#l8EF>O zV(($M(%q}v=6Y3VVXzjl@cpwb2dxaF|%QND7)siSm@=_N;j~+8BPB> zpH_(^w!dDaHD_FeanpItbR()5m+5a3_Jlec(~{21ojT#0LJ|LGoy8a5QES|8ZxzKt zEUQ1G(Tk0X&)i{Lc-|}Yrv2c})OLMfJEd#y1w1-@F}x$e5W5}IJH{;IU%yhn8{0%{ zMA6Fd5qPnzeIqnxG1%z-beia<(2aK!&Hk1D>(^vo-7$Udon_9Rls|%XEN;5bE~!6B zv@o?Jv^I2(x?JSSy{-L^_B8jj7i%r5*oj%SVW))dzy*PO9nusRx8wm1y7 zv*R7%Ei?NuKWH3jvzB}J#Vh-eyYadhWt!~ z&ZpPtXzTDf@nLg?qM_#};6{8?;wD%#912MMjdP7*C%Jpqp6uxteZC|I_pROSgXWgxkjzP;B~5_`K}OPbIM%hN@VrjOP%ER35pXimu_zxIR7(92&9@u!}z6 zzn1^DTvVt`ee>t~v9j7x(s-G9v@&Q}VH?uD`g`ffULipGPq4@8g=i1^@4RQwu-w6L zWA3h)$g}V(%8|mO_DQYMwq*Av$p|?irYoJnV<`ZEIU@u4`^gz#1{;vqe?#O}u=~Qm z9l)P*lY#h|0$dr_n!Y-dI1l6Qv|A!pjzfvp`K zDF3z#GIewVi%?Vl?dU((zvDFbwEn+6Ik^7Mw4f7Y|NDlWlZ}J@KW#%vh5wccezf*9 zx6_rjwukZz+J~qBm+(K;|6ecuZ-@UysPkWhJn#OS^1t5vKPfd`&0VA%?V&w_MgQ+= z{SWbfzx*FUVfMch|1U=T%jJJcp==gK7H0p?l8GXZ6X7mESCQ0OT15kzLS^iqiw$~b zgvP%qGzxUBlRlI{(@1$~2@Ox+X|_ii{^H$mZQgC{ZA()!I&wsT^l1boOhJL{DJ!wk zX{2b6m?=vneTEfF1HrH1DCi5^DTeD!d`>&?r+lcGL`COl; zS~hIHLj&a=kJIH3iDu6$)4QjW+RCH((v#<-rRq##PScR%t*#Ei-@o>_f0Lh~>HJrq zHHO89&>J7#NBuhvPHU6xZal)_u0mi) zUKkol$&}y;%j9W}=Wb+$L7U5wKXZ%U|IX)cYFz|G0ne9l+o@L}{0*J&>g?Bf?|!Bl zSJaygS7=shdHKf6{T4K}4U4^RA^A)iW%2b7 zRwNGpJ$qj?oxDun>~&_ne`YgK1a#3Bd%2Xl8)L353q>Iqx?NZN#bxsFJqR|6M$(9l zYP`$mLF-{Vphxgw!&S5RLo(NnmK{m;KO_5hd~?!JUX;kotyuiapnU|^ay4I-w@35+YlHR3? z=>@Y1P;-45{vhH10MiC+BG;z z^3-dMx(cA3eq8lhC{wk$-XFDro>mz_WE>`e?LR)F+;+DBHszD(%T+`lrC%@mF@mN> zQ<=1Ds+2_^Ke>(4rCPar?2jbaOl1jR1#FkAGw8=K6@;CJ|F(iW07^Q`h8^xQ_GJ3kX~;u%vpCX-h6tzF854JaGNp`nvw_PYZ2kK%E)S=xIQw6p zgm67u%0gwqrT1YyDp4sI|TM zr0kf-7Qz^2)*Vmp_!VbZy%lnuAUGlQ3QnSrsQ}CB3 z7;|TeGgkc;t8i*>tBr5t7}&3X}X=RsAl^= zSy$xaUN$896YIS7x>oPWsnDv?DUZ586DtY&Ld+ZgTgcGuctb|BT=72EL0 zBR-#|zv3nh->$Jps}Z}waR|5XffG`yT2~|yj37t;KB^28VOTU0kqWG_g(~QbRWK~T z|9gLj=gt=8uvCrlOkUfOQjiW6bK3A-J|n8P!m>}~((i_Qfob$T|C6QaHHAsn+vCdG z3ij?_lAGXprDN#BQWcxog17bf8sz=d>#oULM#h;v%of^2%z_CW+RilOQ4or2t1FvF zZmwnChh!%2Sej1)stu<74>l(?ozmG`51kxsLhvhW1WvbqcSs^`3kU?ghvFk^$NK0d z7^}{mA-l*%z6Vp#f$oktaCCBdn|>;abW}UHEXDs%7t@+PSg}9j!$`n(<1_NgS#<^? zjdr!{U5K#$umOJv-?5gMYO_NYSzr2#ibTE8()*=>fIrXMf|lFXmTK=WGHh#92@Jsr zHnRnxIhkXhUxU?2yXriiY-_tp)><8F{U67TE0(JD2}r~y7FR+iGPS-AAt_gZz>>!( zG5kV!mu=c(XnRp^Z%)-TvtsD54m_tQ267$*#q24)gG7}U4W<7Vihxal{nwZ;2?|)5*Sw@pb-~QhL1xEC2U4aI+-h0Xf_Lm?{qz!Y8Ue|!UnR8C3c^6dD{XGcOOhcxX}yo{7q4) znW%G}hlr3kvz%U7bn3*v5OEK=vYX&Prm*TCTYg5Kl~_W!=(rE?*i2cp*=s@jZT$WR zgO~nw$Y^%4#bj1Kv|0&oG}R7#tRfC0?GW)&yBo9HhllfwRr`gq`o|S=^)euGF9?Sf zbN$m|#iGsd)YnXpo)uO=*UpC9SleMvDO!$Oa6jY`ru!qB8cdX%$RMZ_eS9 z#Hm;9O|ZKERkX3yhNNMP2BQ1%H|M=~4*de?WikP$=F>X+TZE1#%+#n{5(O}Z^tl8^ zo)Y0IGm*0)1~6$ACp8_)huWmVo*%m&4>FITLlA}e8jem@;m~!bC6acD{4L$E6TuVb zBY*JWx?|6x5i7lnFuer)H0sv(o&N9>^j@p)X&)GNf_zTvhnxHhnooM)P-w)7K3PR} zDa}qfieae0#`w@LLXT*JxPV&jo2m`>b^GHr+uFsgdN66O(HUFy1;~W+fn!=VeiYFa zf!vkU^;VZ2>EB-w^qX+HeZJ214}HoqybsDkACEx&3+=*1jbVrE7n0}tC)2S{$*puxdNypz zoSdjHR8rwqX3L$9apm*h`!+(ah5e{wGY#x3e+)Royz>~37!W+nYFs3;yjNA)zo=NO zG>>s@G>fjOuqjUDG;k34W-L`83_Xp#W1~K;@8I&fs_UAtN4`AmQT!=GxtAfbf3d_U>{%h83x=naCE>4(PU7WI7yvawKKsFLd~}gWz_M zZh3qsif@tX->>TWXG-S7FlC z`?l+EE-?fm_d;)ls8MBO2=lW)9(cs_NK=7^VPYrS<3xUfh3lqn1nzOSRl-8h!B>)d zUVSDzj<^vI#NX}cxjKP%UK0Gs$OC!KFf-}gmNvD2#*&%czHw&YjbdeeHuBn3{9H*}eg`3sda>;LPX5x)G+eQB&B+PRZehbx0op zhD_+nLU0baSEkqu+tXUPchk_t3Bu`A1vuJ_{qB<80bZf*Kr7&iFwSANM~;QlFQF={ z@Wo6m`K$6D&%eVqd+{M*)w2uP>;d}S?i>626Y~@2&?9uAn>v6&n1u~A!4Sz^-nxJ4 zel*8pmbUrSOk7@tz=~5~hXU?evfgcD1EBd^ZZq! zRw4u@5a30Z@RGreJ+VAidL6j__oSM+w<%rZbg;|14St* zU=r*0177wh*0!8sHs2pcK;h;Efy1mq*U`xDCYz;~$0s$2Y^UWpB0d#w$UVgymlLLl zmMq@_+lTb~Ci^U~&>^TQjpEB4KK77?R-?HqL#VM+uid#0mlUo3MGpqhK&OymHC_D3 zYowKBE**wB7m}Ln#f(Es7RWaBp#?p^;rQ!Y^(Jm0Sw|=jz>)Wk>=Jozk-mBG2+r;A zHq+Sshu&Hr(W|-A$sNhBVY?{TF_1XO|Qt7B+P7+g)TbPeOR+(Q4tu75Kxtc(b`M_IpB3 z+)-ynY!E$tKCYM+zL`jXu~#PJ%5kFq7!GiBU)i%Q0c={?CO3*i{w4`at*ehr64exo zlK8=Z4|%et_uHDz?h)^L`0bPEBifY70cY@2uPUw z_gm~w2lUs^A38c;@7LRT(J2RPhjHx059|O~yi_|a=DIlnzrF4rdj1#&^Och8JnP<2 zSO1A|9Kzj;am(S9t6_5s(YXjlj$y+~wMJ0|8Kj=bVb@IRjW^dqXPkCMWCV7?(D@`(2!@dJ<9*mTnN7=M%aneDfwSp|3a zT8zf;x>lzZYJl`XR)b|}3lMD=*CTzG_jA>bUI>%iqo2Y&5-vAI{ho@t`a|V&qL%kV zO<8^+RUHzK*3)=|drh*k_@0`r^aKQujls>o58YM7JWy#t&O>|y>gUJ0+7%4#q$Sko zYaXf3zvg@(ZPCfoHz>r1;4jP3_cVyNe(I8IN4%NE1$Is-VKPr~_)`m)-AAEWAC!Rg zX%yTK69Pid#NkkRdA)+5j5%qY|R_nT!*~RM!RD1YKuIEWU`+5>|tU)!#d)f-$ri}kQX=i&3qCF## zz43`o&Dp4YFS&ZbkmK2xIy(3ZhIAgN3^Fakxk3;Wxev5UV~Cm4cW9H*R##}PC`ZM- zjd+8Y{|ZTZ&ad|L@xRI3h6I>{K6~8T(*KzZiFSoJ20Ujf|9WUApyzr@5sm?$=&w!l z7f}Lp)R@k8W~jg7I?^moybZw6!N~NwnbVZt+FLDH6T-tZOOM!G?(>P2keEV8QKLtG z9i<-j3|VzUj+LWEc50{P(hCtlW1vSx2jw{Qey7xkKCZysMf5Sym0hlOeimdwlZI{o z8OL6GmV!U2Z&j*h{MKE)(BexSTkg!w4?7jyLR;ck?!+=2_Z25>hCnoGD<=dq%2b|S zdW)%{Eq6h{`-^XfIX>VtE8Tf{mWSs#1@@y2Lz|s%q0W#^Ov8bv z-uGed$jfm3go$x9&opN0z?y!{{(Wq$=MC5Cqq7d`>{Q+$9;;||&&gOy6NXdK){oWc zAFcXMowcyu;)kp@i}NAR6sr-0(R2Rr1jW=DA06ff)aatD5Yc#2A#x5_^}!Am9lc~f z8ZpHY26)PtBw-?;crh!!)UmwuCyn;hq4j8Nd06-GqN5a0MJNJTyphmJp71UV1@Bnx z!$-|YuMIdwuVA<$xgW1cvF7?+;Q@-$X_cwnrhd~fn}x)MDj;{FI6@`m-Xuk7;EgRc z85_&ziA8`zU)e_A=jhp9gKRoYE-$hYojj5f-m|tW;s^w=^R>s(oUWMV*T&;){_E8blm=af5cvj|K0BYf^!+&53}t*gjJi*^ibXWbw;m{wha9`xz}AaRVJ@k zaJ;B+m?D)zD^;Lncy9|=CBBkB?n!Pjk(PhMa~bg?-HB-e1Cpp6{t&V)RPLHa-x+i? zvj231CzW+c*1{(MRpRdgFQ04twrwb}h#6VMQ>~CBZ4h^QorlDZ0hppE$CWU9ra*9 zW+zTUxkRvNqK3`9Ntr>3p-cPtedUrcna&2|Hxb2HkV>__R6NXQg;z8WNUyL@7rDCt;Iu2}sDGTs6D)Db(M6gN#F3!h$1AoSie-}ij$_R>` zAlp;3{(x$ubEjMSlb`LM*Fa3M@#i3i41=Phu0qFWr!Jyo>jG@ zR`!VzZi@YRoL>9p9!A|*j8wmmTh#Z9rTl?z3%$9gm6(y4*aX|}nOpFyq)sh2+FUtS+GY^!8=I1Z-Mo6_!{QR8wzgUYCCt)~m=6hZu{4bVHZJYNF){xK;c{Tkp>^R719aA@t#4G00 zSSdcl;)9C0kr3<5WT$8&E88nEWyn(1MP0Sg^HBMQ1ciW$&>6s7ZRb;z>6ss_?a~YrnLy_^tIL0-d5f5FQha%% zeibA36&cCaJsQ5<;mfB3TNE&N<2G0RB6I+f?5n&fGH95^gZ?dXBKK()Mw^0+DB`IQ z?Y@S;aM+26Pd}oj`^jvl1#=bD)H-?11$M}evCPmJIIT5V3mT&zq`U}p0xg&^3n?EG z(EDjXgob6F6=BVe+oEUpqd$#IqVU;`463M`+DeIeY|6N&h1In|+!w262UdY~c=zZu zz60qby#ta^08|VL|9=(W+qbdS1+?#{#Iq%gil<`I_m!sEu2gNY#>nv&SqitK*^hMAMsBvcrF<5Puhu{Kslu|_R? zdbS{V;c@*Zsf;o}Qx3`u&Ay?MSsxGYh&Db#cy9pO&xZ%xl zY!Bg+t-5Rb1RuQj`(njRo3A`$S9^nfqO~S`Y zVMVc~qgu%0d_nvHimJ_5vAOb3quWzrWVq9gAvm`Vb}CzQGTpb*wq*6bnJK%-Up0((C{ zO>j>`l-eh!buhisC_H}vd3=94-M9~tvCe3=lLG(=HbDz--phgh2qUWjmYmzag+3;p z!IJx4N{}J#{T7Z{)@U9Ai5uZ6E4J1h38QR^JZu!koloPu3L?(1vM_3JTlklXdIo$& z?~f{0;x`I6;?>AryV1}rwz+jib+q8mZzz?O~L#97;;BE`Qk%~30C4B!}nyzNl3XPH{7!J>+Op#EHm{FL|uz` zsmA$wt=5JUoE(nl!bjl`i@x;|_vZq7#=RFsUj`+(oxTsMl^qCc&etzHrirI!ATAgO zEjZ!x-P$I3iD{8wgb&|Li`C{py%AllWdbVlvAEcO6_)0p*hV(H-YvS?t4M~Nh}AY( zhrbI^b?9!{0Wg-9Q=@!~4~kQt@)&1rh1}0*OZ@zc`M2frBg`pb1Hrw_A;+IVvazJ) z!`v5FooP`+r|IKsBrU;3P!C?P?WyvTUk;sRM(M2B^5odq9O2$yobn8@gY`h~0D{n7 z^&DvMw?+*GJ%n%h3s{kG27b^?XJ?e-S#C$b898#DHfqn!H1MkiF|S=28bc?ZL9J9c z`XK#FVh&%ogXi=mDVy_PT+6ciLi8rLuB4C_tSg~P?q z9rfK7wy;B@fK0#JG@(wH?DX{&zPLj?Gep?H!yK!uPp72>NRZt+7>-{511Rn$?ss#* z%2{6E|LWaf>7#vR#HY>>Az`PZN*({rqxHKq6yMWm1hloGfW^+&nx99OcR}ErqBE4x zNm$5K4)-%=ush{1;&FFE>Gzxg9>*KH&6sh%KbZ!XFKEz`#iF9_k^1XoSq&&PCyRF> zFwWq81?R*>L`4UJa;{BW3xivoQf0&B&6Y1P5ne#F>+hmOeo-=rD znPQ`JDr)Qod$|{M)|R>reKZdT+6QBnJ6XNvQWZXJu*64%t=d#qp*>48$i4)g=k$r# z{EWi0399R@lV~gG(b2UgOx)2nq>EkTT|1`|3_RpyV33p3zGOMa_zvNbYoE1OF?#<1YkMED`+N`8R?ERm_3MiKPE*mjSLb6@>h_>kjEN*lESiPFIMIw0{k%{lFz_qCTm7qv+H3;IWj49~6_VO<-p*Y1WcozDmnE#z68I_W z87VKZIb~OU+0Y|3W2e4{0r?1fG)WuH~?AL_%r4}Qy|@s^{7O9;Rh5tLjK}1)V8Xe)3usGoqM`FD&rKjqZ zlk+rU&rg4jdrW-6&ME}lhFtvR2(2^pz;UlDL?L*o$3MR>{wySG8y)!y?F3}ncub2v zR~adKp51@sW;@c)5`9tf#A*+u8o{mqM^>j-p~g%J5fDI+l9xLlFB9iQblJ!K#*84$ zBlR|BwotBe*~mu;Ryqfs{esJk+-cmvGM4|gtSHVo*(wqai~?ukFSMu6V{uE^3|@Wk z?*9EY?4$9TQH`&_YgH;cgAewY+VThS*FYd_vuma7B=PXZ*0d=H8Na8v{Yssx5 z`jMQD5zQ6A5b)e_(Or2kkzII?*x`1`P)^T=;P!FH2vW#`WY}G2EVihfX81ij7qG_J zITZ8wzB(aZP}2N$C~#X~;`wJ=%S5_t+^T)!Vqg%g20Li1a*=I#DZ34MM6$D08%xt!}WoB?VeMFkf9$hgI!bQ;+YZ?w9PRH0w zZh!-4-!ryH%LJIiLrf1<2NFeWBMl_vluN(Bw+~9Cg1`!_GlOX$7=)1@WPN$g1hL2{ zkVF!A+o3x|R=9UWKL{^q2~I9XBVqP;kJ8^+Cl(|&-B3liiw3ggPy$pN;4W}?TIq*z z@4vR-q&WA&6Ii7PTj^gqT!z=>!MTKM7* zQ-aNEBu=n&7LJyf#4HX^&t>VaY*l3fbrCQ8=#{!{-$#Y#d5}+If2?Y2kex{Oa=yYI zwN1vFke+2BnzpON66RYrSSKBAHH)?IJ7c68^q)9a9v#kR zL7iblS~qNU=z8>G98RJ&_PG4fThSVmd`ylG3vRKRl?2|o^3Y6Y;W0B4H|2K~q4f`z zBd;6gn}*VeF+)|4Apmb53n++S)Oqk4&n8ZIy*`2jlGriqN$m#+7G`%m;Z)W+e5@Bh zoIGEsPqIK5eFir?Ob~&7LK^)0xv+yIMSw1D!Tiz%ob4+lEBF&KS-Aq7`0)n|;m;S+ zu!c3^Nr)X00(hlxW}hMaYHHL1Z(j&E@v!N>KceQF*a>f`d^OoKW5;fZ#^fCE!89yS z;UIzEsu7F$2 z+ulP1*d3}Lt}DUs`yL*%^>edQIb{*wnZ*bvNFy)5!QA0Ikl^)>a#unD7g{qu=4PTz zLA_0yWZnaCXBI!L@%FekUBKnIUnJy2SrD-HI3lE274xERBG+IS^uBWxq8+rM&t)C~ zz#d5A&j%fji^F|oti~+{2c6VJu)R{gG@F+1@;c<_^y#C`Fd2Hif#J{hC^+YU;(8cE zdrArm7bJbw4Rue5k?AMI><73;ebobq1$MjdZ?D73Mmmu)hc2nGsvDnjxOTBu@W&_n z9)!DGzx%c&%N44L1EYR~_CVpaZu4;qd+wM&o}Ig^u`(Ot(Ep@fE37U=)8`K$S&s%p zI1~2%b5*+PZV6Mvze5ARdN3S>JQ?B>k-Gs(BDAswASZoYM6Q%f-;Q<{b0N3-I|5kE9^ zBdFbZ0Xo6r{8SKvfJ&IxuQ{JjXxR|Rrs^Zjh}HZC@@3E+y&&LJ<)BesmEd_viR(9y4xC0FQJ-pTK4jj7M!F_CB#k8VjEJ2|mZXZCPZi1R*2BE;`# z{+znl{l|~sc7d}d3&B!G5pMENj1^C9F>9J}cbWVAfl%B7`YYF3G%AhM%DYq4o$>k) zOhIf2u(Ny$_^ev42a}77F1n5zFf)}5s4^s+#K+`DJ=f9?nKo0>B>2dU(evi1As83QqQ50b5i6Ig@SWV6IKDpm%g2IX z4d)SD+<-LFc(|uq#bmh9-Ea|$!KVN>(FN+ORQ4D1!Jlx5l}2H~YY9-`lq27{Wo^_O zs{xSF5g%(Lqa~fFf`k546Y&%aM*;1GLmcevUAKuj z`yBUP>}62ASVMjEIS0O-4#jYYa8TlMN#D^roc!jS4?4zNH1x9$>9CQjtm0wTW+5<} z%$yvC-PA>-+$xjC@_>`sQ_>kjx{#nXCqsOFsjV8|_H}FmU znv!}fsgV0A$keKL9xeMG4fGv!4tdPz!Q>*|6(Fhb3VdDN!6oa! z6}dt&H3hgbpCG#>kEQ!0<*}v5zWrnGP>wwo_C$N{r~yJ@Mp^6M_r5%L%<@!E;6&5s zTn<`QaRQo*mJ7TY@%0D%Gfj1<2Us@Xot_XUb@L_$yUXNHVfnG-ogK*ANJ zyvk3tCmL5X^Q3qG10(OrSAD2;#koRc8TO^mYS^EecE0n_E}UY9t|Fuizu<#YOZtrQ zjed^t3QroVoizJ%d^-ilCx01Lbs#uhy?%70u{2S1KQ0NC>wy3lGGwzS@y#SamZ=2J zGbEWWR7NRtqP_`exWrHTjz86z%M2Fg+RGw?$F{`YO`L8Im6s38G{|AJDMKyqWcgDd ze(~&87Qe3Q?&heW`7V+W?e|(%iS6N}_ix>GRM`R2Y;W6??@pGNy>LA1Xo$i$C?2!w zzK&v}uKdN7FUppAbOSHj6O-186;jhGI5ThR(|!bPo~tJ$A+POYW-v_zVs)!*C8vIG zNyv=G3Hg{V?LD^wmno@7I8q-4-(GLSaXr?adX z_$`M_%?i7DbTn@t~&okKT7?B0%* z^>IIun|GxJNoYpboM^qK7?*rNOGP7J^(n_KRUjima>c)P!(iTG973!_DyRo_jZ)D0 zA|Vv6?f%l<~(f$Yl+Gnoy=%pL+DK1e9+ zK5?8olp(`E?CCUC6aYi~Vk1)D(*yZfu|8jY3Ob(^W}icZlx8}#%kx;xP+~Eu{1V{C zg3MXuz@t)1rd&Pw5QX`VDbUWqE2;(t3wvdGPY_H*L*eUyri333>QMDb(}B~9vr43TU;gHSd2VI}P`)O5$R;4#BD*~X$XW3yj7u+4|pWj}+e9w9W2S!o} z9X(@0A6siavAUlcb>Mtx48Mf_l?SeYC=R8Bz>oxKR#UH|^cvhI7f}06A6F`a_m795 zHf=_k_zG4QI!BzwO86#N0eZYssANASpYJu>E|VRb5uWoG$;F*>;j^ip(RQ|`;Cl7) zyC1WY1+gW!0-Zt{9q|r^t#*qa?vh~Qy9RbtYmNMXZFnN-28A_q=wQ%+Q>VH> zPShj-k)e!5K|Gb1bH#mOu{UQoH}@-k-uSOD4&X+Ee|>lzw|RUUmWjeUirJDFywbBA z)Vy(Gm3(bd!7Ae>VCI4f%M5ExdI-=ESLsePO-z_hLkac6;WKAD2fSUR#2wqz$^<`QqNE&m#%jte>tIXedP!1`s6K2LTijv39phb1*TK0X!_ zqfN5Oo4U*8S*^Q|q#JJifE|c8O_QT&35MSzh7Gh#800kSjV}?TnT`V8?1@-5ZCg^$ zgc9)}5Ro6~gvxXk#jxGrp|W`$v;3-KpK_M{b9K7q|9rM46+0iZ5kRULLfcMO&x86czFoHYru2pXXV^rJUF+*kpZdK0 z@%xUt-2ME!d4bjg;r%o<9?vkqzVB$W+qg5=!$;EMIDU?kXtN00#wuc^ZCQFq}Q6)Kw?-Nf%E&efVEMob!kVT?~2~Sd{$0Ux^#exmK2YKUAO}Eu* zz8gW+7&dptAMif#9KjsuptA|vc?7We{VzA!^<+Aze-iz9GN*KwHYt#eh4F-b(3DEW z39}YMWj&i3`Amq^ zB~}rZy~|egqmixvOB%?FYO;FMrq#Jk z^)~xMfO@I&qP{HvAsfUV=+{RC2qnA>5s!a!@&;U~Sy_T6bB+-f5^zKv;uIej#8+Nq zZ}u5z;z`7{!O*4?gV%_76?o$ZNKYjU#6?)S7VPo*D`|p*3Ew?$nLdWpG&DBeagU}b z-!g#eJehRiI^moY81p*_5e`iyt92VK>M=!YUE#dq{26>B%EG0ESQUL(X1=h>r8<42 zR$Wm8S|U$3+z7DQiW9I4<=MpTt9$?K&vBB3w@1{hQIlWlE)30`_!Uh6Neuo!y`5!H zTtWBdad&rj8Qg*mZo%DyCuneoL4&)y1PJanXmFQ6u;3mv2?2ud<$eFPwOh5HxB6?s z^u67E`rJOh=jl#v@8pIeD+UE2{qv;fUzXCHW+fq@qOOK_iEFLK_ReE@u5nSYdYxJ} zaD=$`+0XR^l4-|FQGIZ2c&wS>X(!Xug0 z0DFaPDj32&1C(ySKp?SELSS$6ww#8DgwIVk}H-5sS zl?nlQktR^slZJ@&t3vR&{XV5L(V6W!lXV%yI%h-6nDX^Z&Ue)& z^8*wA)Pvw#(6B3t%g!Co!;wh+;LzJ++8Xjb+#+;(WS_5D%4OWoLnkYDniwreD%?KwJ zlIMpt`i0-GR+W`ZT#{;isi+j=i%#+h0jWi<4isq-aOn42GJIg%sq(ooZh2pqkokpH zviSW1Ad30>xT9OSk~n`YTDbh66J^GJS0ai?ut#9lX;}vP)vi~C;2)8k>yCg3J$&FE zu9>wuxO@Ie9~!l*(wB7dWv~o_aUZQPfCMe)6eeR<&HD0udr01k*t!lD0+`O3BYJ{I z2iKu`L(a}lUcI<9M)~FS<|`B#bndV6?kQYMYjM{E4G{XwS&PwzohU)eAjNV9QHAyv zUTFEOVi$e=$_Hu-;^Y`aK9z7X4wi738{AV)FTxvfYZ%(86_0mhj&HI|&MF&jCk4(0 zMvK79vf&bszXspr&p!4tD3p-(v)60{rMFs%aQTgp!hi@15VV{A}WrL7!jd=Mczt?aD^KT`bA8C+j~b_0)sPPIlX^INR)U2!??f5 zOU1*>1Bv3Lnc`1>O$Vgl8-}~kN#MDKiNU4V=pNV~2C$C@GGIQ|zv?u8428-^kqjrZ zgoZJ1WG`6%%}D^ayB#R6ZFg!&ue_O{Fl*Lx${&2cMsdiK4Q`K-eY;37n19q~(pk!p z@emYaEkU!@R@4Bd6#F>$)ELh0{|Q8WHH_l2KQ)Pq%!UNmaS+tRs@Yrj?;co_StIB`*`>)&;VzoorWMMhliJS<-Oc6?Rb=9U z?vH1{6j21DvSrdX)?A; zE^8VgYcTy&i(iXeB@FcN1QKva(dPP5Pn*B60v{+1XGtJsiC$G@`;&a?9_{dm{Vkme zubzggMtsOLVyE#Hg&`9wV@c%DaNn?FETZ&;_a~-pqIuuCUtKnEFwk4h_M3Yi8>;-7 z0slDClX@Nk+WT1j_XW_`F>)<+t>U(sHu{G?e(tT)s-O4(?XK?0TuRm_IZ+)mh z|4Ho3${7bzyOwC8m#Y|TC01njx$N=Qty^K3(YQGgs5-Tu&wn$1J9}JOZKsbns>W|| zp}0(8dPwFKL&Jtl9(RY0YzqL)D0?d5xEyu4ckxH-jn7MP8wLVIcMrhn=0je-XjI$a zxReL7Rn$?`BC?}|oj8U;AU9?W>*;%520}2ghPn}XWk!&Ir)B4@&YI5)HVn+m%bf6q zC=85%<*O+3Jl{Ky@cZg0b=e?@GJ^@kVmhJ4S!58k(oj@VZctL5H6&Xat@L;qPi7U% znqwI~l0eu%8-pwN?x!5WhnT;cx&I`#WM4LEjf zGA1S1vEg*RNPz^{%yP+;=1wAUCb=|dRU{x^FJxK@v=;^AYEbF zc=H;wR^?5L0^WROj*C%M4LeA@oNZ6!w#AY8uJj4#O(E9kO7F1LY0Gu_$_v%pp zUk_U^i@h$x;4B5mE?>YT#;CRGW9&wk*J)PfM7TH8*h#Ac+v5zesIJ*Ntn<}o{S;h) zu6Uz2Bl!YHD(2I`ueHfgGMy`!>-p>HrI%|m1N7a~zq+4Y@_U`Ov6|kqSNqYTAlIFDO68&#o8go9y|wZ6N>v8F&RB3e5(#^p@J?xkkp32`Dd@i_6Q~N$~b1 zU2%S|FVI_hb4Z9KZhBJGn63w&lRT=EVmS(_$rE4WM(40h8GpkWnLHtRhm-)&cV;8cOm{ ze4Dfk1KlKv8%^=UR&S4{HLS-j9vG9R1=tHMoZh*^ek^WyRY}KDi16N&Q{EOt&ooQp z<-P#YB&UAR>{*2g9Q3(&b=GmHhLwdn8$Kv>8AXQ0WJdH->}B@D69uA&FY^jIfb>{{ z(FYuWc(Snesc3{^4s%zz`|{-YVYNig{inxSquW3<^8}!SEpuIniAl*9^_m#E-Ap|q z{ENtn*Fi3AlPl;1h!pP!$ZS6RXgg=qsmpL;iSN6Y|KJ#WxyVWdoRv&qY#ueTksz_+ zIQoA_JYGAJ()0lmy-GT--0sIelY|gw?4{*cg^8k&u+P1r>m6y6;AIJT*W{BmJjQ?7fx69sj|GEN<+R`_Y+s?-$SgajlJqRGe9k*|-LiDW= zE;>Cj`FF%p6bqiO*5|sL@$RLsDDbOl0VL}5Ru>TGe;pA|F|AZ8Lejy2YR$8oOr;hE zQJn$f6! zC{}~TtWw0vr(cTJ@s_nG3l-`koLyMQ<-Bgu^_3WNa)uaVPn);B6+jU)JCNNFUV676 z;>FTNERF=A(Veq_x5}0e&b&o&5WFM=lW)f&;|U|l$Pv&A75C4S$Jsp`zrHy_YRS8O z{7wL5iJw$V5=5vb$w_>bM9HO(Cx2+tJCdzqX_G`@9v&V(EPR@wnlFJnc{0*53F$!k z`1P{VS>i@wlb+0uBd!HoV*)`A*7P1BX)tF333Wx**dTq#GQ8`>eO8>={cwsWmsd}# z&YhQ$57$d~V;?NJTez4FDU*Sj=JBfnMYI_$lPH9pojm4R}y!Y(4LFiwQ+&@ID;Guy7aDO+Zm~DN7`gE z_;P!(@UadO#kb@KUIo&UIQ`K-2kaA_j{0`7&a1KyThuTcfKG25SzmPVScgo0uy=CIWZ_^`fNhHSP;KEKR*5T`F~)@VOzSm}|}Z zvTH>!H=K`NOB-|zBiOQ$%>=`;jTEm*Vv!8n@q1RC1FL0c%Vci*Dgb4FsI|_ZaUl4^ zMB%CjjB!h1IVU~=qQ}n#O$ACDACHU9qZ}SY3OzG%=MAGn`!KkO2xd}g z|4|a$%ke`9J56Y7nNA4ENE$&M!iP>LX1~bd+MVBHu1ir3KX)KLNEYw52k=ztjW0T(0x+t|@YZQ$bvqK3B z31%a*O7R`_<4M1Mm5(sN;H4+5WF7?cfT72H!~J}NH(`9ke^Xr4Kylgmh}m#JiEy0a z5{ZKYBgZrbyYbge1ml>l8CNTeklGNf6w@KQY>@KU2%YQqE(se-Iy~P$R5?Lq%{b3} z?XlOjd-&hATM7ZySunuTNYE^Vr(>RD{2ok{eC}|iMn8oI6W_*P2HkcMs>y7ZV@l2; zLd<**(&4B-Mq~O(vGEgKp%bwP((PgcNyFu6ca>WO@ETdzx98h+I%JAu!24w`gh@kX zZatOIYFvVgjy)`kLAj3yqzyTHc=1}1KC>N-x4O%di$-;Ta5B?#J^J}?g=7R1olGU9 z9p#c!nfcJ7X(EvYWVO+}WJ5r2kg4f-H*V;G?aIJL3S|DV999u!J88wt)i_={q@sH; zugvin!06F#B%am{_&yrkH|5GcO6^ws-rLfgP1N6?$ z=x(5YJm)NdIE%KzU{i_7`rV#XMyH{DkF99qclx%-0&l-mg(4=%N;3rLltZR7PlApr z0$`wRvoK8`w96-QU3xxnbU6t8MZLWc2FDv5+uA3O+T>Xq7yxSh*utUI#)Z6=f<+2-u zIG2d>ya0Gxd?VbfFa}$8%=Gmw>qN<Si9h^Z7Ef9PS-t zIV-){_j`mq6)pR!J#}Ul2=}SEv`z=SbHj`=9cl=+dsJmhZQM;<_^aVh2oOd+g5qTr z6rpa2L2kzqo60%9OO$b{6z^<_xPLnA5p#_GMxXp3JLW4mGt#n zyLxoe6Db$0Gjv?Da$f@1Aou`6R`&^HE#(afmE3g#?|^FdJ1tg~_DaGPW`pAJK!8#jbD^Jt{Eh zc&@l|i+fuc*#kanfFU~9lhm8uglx-a57UZ}0kK1JDb;vi%eNS!0J`fW{d*V`l; zDjq%qxW#-iaZGi}yd`Leza7T$9F#kai`6b?NjP;Azt;OXekn};k#zW8#Trj8$jj*V@gTP8xCDV*>>mUE0Im+*xaf^0c-bEmyhj@5upXU* zm?QFCgLBku()k(=x+NxlDcUrojOb`S3LL#swOh! zXtd6G8I^q2RP)8^7#2r-4!L%g@~GWMoWwFN33n0glG{v(+9n}#rak%`FK%jOqR;8(DBGHa(4<# zdTE*IH_9a_99=)7L}KBfQ^9zNn&!C0xV7%kjjDkHNvt{G06UU@DXZHOQH_x?kTA(1 zPID>%6=j@S?OwydFNn=wEZSM)Jti5qhTj)Yq6P<6d~kd8VbJ>@b+t@G?8&L>B8D-s zu~zZdZ))R3JWu#JHTh;2G1~*nd+=1pzSX-(9%%2?z?p)LRS+*tJygYihwn}E;Z@j= z!*0mreFO`MAtPLJx_*MtxW&EujhQkJ?C&m1#a0q{Dbb6*#I3Cp;tlNdBK{PUeWG@J{+Oea1XhJ!&`uaPZET^|hh*pXm zhksQXw>!IK*alv%c4dxlzKvr#Eic?27W9;Q@%T-5FyCeC?6d)`J!>h^ljD7y+93-Q zFliQPS4N-P=y7QO`A}onOz7B6TUbQ{^`0#bEIAvY4Q|n<3C@TN!w|K~g7URUz#xA>9&V=c7w=m|`8m>&*oPiAA%sKH`JHNcLaR(0z;=)HSCf3Ui0 z{##7CGpq*ppbm4a=W0gOX0zKjq#*n|>G7^FYT`Cw6KW?#2@7=yXyV-x+z1)F1nMas z?iJN6Om~3>5&)WgH;kQb4U~N@6Qd6toeODUd+5)S7-yw_ApvZI-O#(UOohr ziY=A;S%M)N2Eit$AOYQz9pTzkbE>-bF(xu9fs-vRvGMk$Q_6SQ?Cl&{tU`c|J& z3J0aC*f7-BJXVx|T!j|Yq?!GT57Wbyv9x8D_nM4O^vwa2k9k-nP1j%2LkgdCr3qi!g z=A)^UL}qo(*@g(FIsrvkjg1hHKP{XeHRTl+nf}V>4_1i&(Gg$4hbNh5rgw+XxH;8n zZEH45&t$^KM(FdAcwPu75_zA;C&E$MM}^>ke$FOdHi$t*45^@q0`I01R_#})n@rmH zSM;hXcDogS<~L1;^fIXkXhkZPtwl+Un}&Grd0v#P$5u+L>o9;1D>oJ#Vlm4h6m6IM zTWlC3Qn;}&^37#8Pl%bMW^JT(Jwp^a{2viS51ufqN}5I(9%4v#(Wh!PaHh3{HTv@o zcJMLvp#Amg$i)s30*{EVEm4X!ivCAS7}m-^rPNPjLtRYnfi| z+Q><}HepS9^l(m&iYaZRYjdq-j+a?yjRi5PYND*-vIkxP+ zpM26$vC``DzATOzb1%zWYH|7kXOR#6RI^os2&oeHzs>T}oZ5XBR_O8R?q}1D1@Tm* z@mkcLt#`({`eVUWu!Ko!PF^@zjj;6RKJ`gd%IRF8{zJ8)Su(Kq7g~mPdtMtFtFtOA~gA!PgDnkZ#Z4I2qgA z$C2`?_23h6J=d6^@&#|<2j0MMTpO)LX%si^jbt~8Mb}L-0EAW)ueyxRIHX~{NGec7 z>#G49zu_cf&&>&mA=I(baX#nkn4*`N{}1+`#&nrxZk2zR8tW>E9(5`K9B+WnffTj) z8Gs(hutSS(aV}E8dA`y>HF_RDcF zUSzC4MJW~({dA1aXmX7Iz)dr%&JZbE{w^Pdeu-_DT{DVSGJe5(Q045yFBBC}@TU+Y ze^Uv#4PnE~?8~!DgN|{=uf6KWS|Hp@6khI2j7u!4)NYj^ODE909#e~{Sq^_dSN`iSg-k7;)il!z0hl63v^=zzZTeIDZX2OX2y^?tO$ z!%vgmOh7;%`hp&_TRAUhq0Ud*haKv*cbvIRWM(74-s^VvU8IC2c)b)-`Q`4Wk zSc|!+T?}@rf`iQ#gvAKc-Tn~l;otKccSPW(6kAd&_Jo(7WbaRxbn2pJ^Y>g?9^E2z z8tYBZi*=>@jK2aocO^@;Y+`?x&8ZjHs&WbcaV$K-He08Rpr&$gDRRqqeC6FxG0jri z4gZeael2jq%I9QMIh7|Ov+->)rCK^tzhN6H5$NYYjb#7Uk@&*`G@exxKRpiZ`8Nio zs0Trs+>ltR2x*8zG&EsQa_Ndug`mZ0gKiUAPe{f8mG}<$CTL5GJXxx(j*h>qRK|Bf zI!8z(`gcv%3gucB(KmWy$`mL(9;b`5^#}GCZ!Kc#QyFHg#Dm{lH?ZpHj;-=#m$m~f zH}lI$`x{N@{C|MF*aT0}eK%h_+4t;9rr?%{(gT z9rB@3A7Wk%yG9`x80h$_!!GM2HM(`*-h05B9*Ug8ToDfQJivnvrB0>SAfT}vVrr+5 zTX};+s=&XRrLJf(;;k59MOhVuiBWMld1E?T^g|e`kA;Y>ubxPJAVf2%uLUlNDA_}} z7`obGTrBvhUL+bW4>ymFRHc?4*u=5Uf}=F~w-W1s90z7^bGVB|HFV`zRP!;GmwTCTS$1&^Hl4Rq!-R7U5hmiMm!S7)h`kQdiN ziSceB+dleS!=wi10R>)-RZ>S~^cx<;`=&<3R$^AGpBy3Rtg~asVighmj@Gy&1^~?b zj6*J_z_jJS8KK|v>In2LMGfOWWDOq`&M%O9Q&I19_`4f17#B%IXvdu9?xA8jyzNX* zZN|91YR%senCDf8(gdR8g7QmiDXHRsVm*m}Z+`dO>bz5)(mxD%fqfDP@{>hu|NEx( zR55G-uCn&B70W9El$7pQVY|FpkCs}0EqORVei9w2aoBqJz%_LJfN_mRS_0=mPbds) zd3`Fxy_%HT`s+`ey5w~WTF4~4Z$T_L(-Y2cmQ9n1t;ql1&Zp^anWeX~Q~JA3O52K$ zoJ$7#N^2#N9g?SRC0_pudQM-D@C>_lBsXox@@vdDpT4$PSms}w!I;)4utc#no2_|; zC7fxWsigToo|?bd*St6D{1J@#4sn%?2EI|DvCTa^N&kJKM)<4Xx%}kQ9qrc_7%3g4 zuhO=tt2u%@0xxG|%AA(>QDwqWUzXLj41{Qdw?gYGPcC;2JTxD7Iz0h-9Z8(#_rR*R z58Zrxi}aD+Q8A!*t=wWr5(7DtB%{%TmD^Ej3N9g@sPwZI%9(LmB+RfS<-TXCq#I z*+F8l3Uj8F6XD6PYw2zi41Sm(D~Kw*!|;H$Rb7Phh;uF*|4v-fA}`JDOR za>a6$Ye)MnlafH?GxDg!4%vaWT`nijb#|& zUE+Od#zviv5)*6vn%>Ya8*198YeY3rp(m$kWoErhceV_e zXX0&3JB9sc9PbCcwD|#_l^RIM$qw=st7uJGaeq_@C%H%Zbq{1K&Nc2oaaI%)EUd;? zFrJ2t;xh7l2jpeDag^M6Rn3-d{4dXcv`wZ}YVUI*{+#kW*}B;3Q*Yhvk|FH4xi6w8 zv$-i!J8_GH#4)xvSQM}RxOs1Kg4RmW!?#0u2S!ZAJPoU*l{#O$jA|c>@L2?EPOba7 z6v!w;))qm(hv#|CZ_n#JpD%T7W~c%)p4e)_QK#CRUK-0YjH|RO>NF$sf<}J2O^jD4 zHXjlqMpI6VD%r0FK3%(_{maOWLEXIXdiGkl>rAhcGjIn=yKL@9Q-mm5$#7i!G4A4O8;vUAOf0JBoEy z!Z9c{{%4*Hb2V%-Xs1GGtD^$XzX9t(e&@={?)tyifW?~7Df_u*)l~>Gm11WJ(gXYh z*#jc)n=hApK-^T zwkMd{|BxOxfi1@wc`)DMl$mD9^Xf|Qjd1+2rWjJ5FwhsQ4bm~s`V@ybE1CMr>~BCDnWmsnfv{*mkEKu) ztBdc82O06p9)nWbNyz07-eZDknTUn4VtP(BLjuhl8 zIJt!1maB?Izek@Ge!y|CDo34UcpQE}(Kk0n3=djaG3ipbSe+S>NJmrGIN6Jrsg#md z@{z!Z%Ki*wUiWb+k*+0acvmDM%#ND}{Bx?eG%$JNQwka4rx__1{zFcQQpH%@=k6U#9NmwfWR?y(0w%AoU`RfDD!9u-B&_nrQX&P@Nc6tdl;Scb&}^|3hJeuccccD& zN{_zf;@B+ZwXzx|BPLra+A(V8$4AIwKBdbRStZCy3{pWQ7rsjBwLp~eQDFwYI$LgE z3-+BtJ8Y{ZG)1SE=#9+`<#b*iA<#Z8BWB0213!)q>tD5H3g0Qd9F6cWsa%0up?({h zt_!k12kv2KNh*XvT^&zLIt~=Br5!&?gjqE8^~JK@c>g>L4tFcGJ9)O6Xsj&r?lR*3 zm4((!@V!6OxVo*ATH0BZFiUd|lhmzgs8JZNR3-E?Pkk?w`4?js9Ll+)kpshAA-#OE zU!37s_Jtya-tBFFV9_0tLJu8UN1BN)wPOP)dL!4hN+1_!+0FcQ4}{s(F|p@tX~nWA zd(|&yar6P@L_C-DFWmwePe;gs2~Edq4u01sti;u~CVfFqsvHeZ5*IxAU}6yz70e>k z>eS%cm>;E^5gNruf( z5bc@lna;y3m??Y~z;MGxaNlj!?SL~oB8n3(IZ%*%OI5&a`+S|z_CB@kF5Wxxku%)I z6tHI;c@nQV@93j#e*$nKp+@M~W{`A!V5=iy}@ka6=%e34mbarqMQw*R5{= z!GMlCi2?~`Oc+;^jG0KtFo9<&{B48MAD8X^5T*={RWB`(Eh8^iO_|>VeljK*j4;A= zVpB2*u~o;$z@a~+;X9gi^zS?Yhqfu5$%`D6NoRId?nV7nISbty!|HN=%~OfGGXqHX zc*)1hVIwh@XR*>+vzGU+o!!JKv{O zB}`isQ+1|!*Pa1?c;pM2n}U`^#7vBQPu&#-sc*#{25Xex%_3f8P@T^@r4%6OkY_$l z!WO58wjyl|>;|#LYGZX3>}vtnCWZ%PS?j?OPM4z@O8E~_bj8kKbC|riAI$c;H;4F2 zi_R;znqcpIwt1pT&nPXeg~fPM2QS{D+G1#v_oeHYmb0b0fLfNTTI3(xV>)Eqipe(- z-$qAHn6B3I96~@lE(SlNt}u5cd5ItRm%2JaB~aHiri#-BMU!r`1bW#}XC-So({4)Y zr?xu!*MD%Kdl&}4$4+EggMa)C*zg@puSl-QkT&Z`@e!G<4M-=54f$nrTIPd6VENG; zH4xoqUjQ9VZ*xyj`(M zB>g%OR9Ht(B#!5}9&k0yBrjxo&a{9PiaS8RN$1>Uxt1Z8Xemr-iPuy(uG;q(E$RpvlD|7%(#0>G`ihulV z)xlx|IAMt_3Z+{r$JJjl#U#Jh$k%cKFrBgPQ#*C7VnZzqyznI~Ae$INS5US)FwYux zOoqE|v>M5wphX#Hem~G22^%>0Js@;MB9Zz4f4QW0#)qV{gV?mgGFZ4*f z3+QQuTv*5VB3eBX#*-i;-u|LO9IU8mo3B#}Ds_PcComp{S&b;PI=BzX&XzSw@4gz? zu|MaiLK>wTerLddH7ru;$och>s)|lfJYccJh#xkQ;=M6T52tgpefUh;2f)crR)C|+ z$Vso|u-j@UyPtY(=>>FX-QufLjq8_6oD9=~2;n+-bIP|XviOLm24PXd@$hT-f&_oy z!NI*yEqVj5^KZJT#sa#rhP!w+x%?MCzjx*2pM{lc!7QJ`@K(>(iy7+{E!D(#^6zK# zBLPI1bEC^s=wi)cNvvkNFbFzlEwNF5G3iuNz@?C%v zg`m~xhrE=tOYKVlORO_HAzB!ogWPo|Ko>7Db(d%%dKhFykq?LBGo5}VwtV{KgUToD z;|mGRX{Dfj<9ODy{Q1NTc(*4k1x;Tq>Jgr0zsF2s{BL?=g?Nok9I^5u zO__3@pr+a!(WMIrXEuZu+c4iVxiwcD596z!F=dp9>;?THff@EVjtc*h02A7`;x zQ^25~BOcd@sEisKfzMBdT#fi%diRIuAPd#Q8xKiW`#^7aV2*L)B*DX(mdu5kp+dseh#tuu;SJd;e} zl=zwCJ#d|CKkSAHd2-b$HfZzxOCtedXS)%5OuHamk1M$SWMrr{z~>{3!ycVya^cH3 z9Br{a31!UH5`%$p`=k`&SP)&vimUz4p^16zjf}>(Bft57wOdJw7CDIQBqYEmz~7C* zB70cHku71Kh-kiGng`XNB1t?Aalv@iE~Q<;LjPrGzY`s^K~e$zMq9-7+80i$ra*y% zqDXw+sF*PUEzeKu79865MYYp9Cm3Z~yWikDyABN|t>O$9Fyi^fQHihZyS)qii?1xc zq{N%}V}<8MB>Nu)^Qjxt{m#XX@b*#v(zLO4-biil=ij|)k;>5?rX#bK{g7u~<-J({ z_uVFM)@K3A-~<1<+-rA527vC;Bf*`H00?880C6lx54&Ej-D)%eX+MP_Ecm@z^bdxG zEm>8pFs?3Qk{>@r{_~`rQ?QbAjHQ&>{@JJ2zZrw*IY<>jlDVhGzE}+C9!iji3Umj` z7e~PSfN+?4JoRi%F+fj)$J;+hmzr{})*h?tM*9H#2IAc1<%HRB{?ylDvU|X0HQqYA z3(zUyqHlmv-KT#YRT6=wzzxr3Q|UtmyxxCS%PR;`(WF(Y7h_Q6cY>>9V{Qt*_%C-i zURcLQY8_S}_kL^-rEg$c_om;;ka6nVg2~z4d!m^T>kv?e$qBB+{c$PNJT4me((h9> zpABmk7sTWc?bN0X;Ak9OH#dZ0;D5qE!}xdBS!#vnbyHn|`v;hvE_2|anx#iU-V`4x z#%!>Ji^zH25YYDlmJb+nm=pIlT+GJgL?HezL!Gd3VH}+(!3JMHdY0cTC^6?-=YCWe z4awVs@w8(t=YzJ(|VgE}o->lYkQm-k+~GPZa&o9m~oAxq*dD^E}R9*MW5y zJl3)NM{&>`BW}8?yZZgPY!L}KE+XvS1ts<-C(5~_kP^9R0G7kUhu5GCQySZyC_+uJ z*4@xTUZ96HWBuW>&-^r`*U{45urG8>^v1xhahsP*c*|kDb@|QzOz<5FpgNo!aH{JT=MPxdO>OCcZrGs>=#nldg;yE^*iGH!ye61V~U+8#E z_c@?HcRxFfy7s%$kiT{y^b~kd?y;vc;celhWs3d>1brKm3~Ik)S^!ki50^f##4BJM z{Dhqe+z2qk0ICLrXhtc!pVz4U^WmWx_!n6Y6kjmr7&#z*ou+TRGwu_a5DVj^$FWrnOq(-rWDmX(d+$;Pkp@7O%4sUBUY?#Y0mnJtYCVp(+T*YOp54Gr zl)Z!Vr#2ltKYmbb24^@)BSbo{q^aQ4p!(lxzvNAkvvg1iZKB!oXcMCONrGE z*RZ!FFA3d(UU80V9jq<6EYnF__h=nL0}B) z+<=f7l}u}U?#a0?0T8d*BJSmmYb~tYzhnAHmFxeWtu73e7uz^3l*eO`3%+ge`pidP z^3r?J{NMl2MnR+J{rK;W`dK&8;!Bv}5Qy{~M;2;RZm;@rwTbwnbG|le?qgPzFRC>A*uB8Qrq~wL2=v=M5e{L)+@&qCj?wfM{|5_Ur_6a!Oo5wDSb0U(nFd@(_iv2G>RYvttaya&#NFIVPX8eMI(ce5Yg?IOrr| zp5|*_V-Bhos-0k!=$aA6GQiqaYIHaPtu|V9QOr3WODz_e1+u<3_+n<6hEugBMqQiR zmRxE?fb2OKcmynCU?CH~&UdcJanEo6Szf?nQ&Jc-*(W=$_tH|Tb_!A;S8*ce5DI2m zt$Eb7%^p!r0sn6M*ER$m`e{_StHJ{qy4UuP8d=ZzpNXE6$q@Ur_1eBi!~5S}&hP6u*qqLAHrW+2ZM&6ys#^F3wNna( z2YPMX)yr=`XJ8}OOd!}CUaWK!hybDd|J6SC16#HByPU3}|9L&HG3ftn|G&Bs@`9Z28m#5aj_`VI PBaD)qnrxl)yU_myM6>UD literal 0 HcmV?d00001 From 6d0b0132102709d81bccd5c0b6e3b164a3edff88 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 10 Sep 2024 10:24:33 +0400 Subject: [PATCH 21/22] add theorem statement --- ITP/slides.typ | 65 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 39 insertions(+), 26 deletions(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 0d6dbf4..985a007 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -349,10 +349,10 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. repeat: 1, self => [ #set text(size: 23pt) - #uncover(if step == 1 { "1 "} else { "2" }, [ + #uncover(if step == 1 { "1" } else { "2" }, [ 1. Discretize from continuous coordinates in $ℝ²$ to boolean variables. ]) - #uncover(if step == 2 { "1 "} else { "2" }, [ + #uncover(if step == 2 { "1" } else { "2" }, [ 2. Points can be put in _canonical form_ without removing $k$-holes. ```lean @@ -361,7 +361,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. ∃ w : CanonicalPoints, l ≼σ w.points ``` ]) - #uncover(if step == 3 { "1 "} else { "2" }, [ + #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 @@ -421,6 +421,19 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. == Symmetry breaking +#[ + #set text(size: 22pt) + *Lemma*. WLOG we can assume that the points $(p_1, ..., p_n)$ 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: * @@ -649,27 +662,7 @@ theorem of_proceed_loop ] ]) -== 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)]) -``` -] - -== Lower bound: 29 points with no 6-holes +== Lower bound: 29 points with no 6-holes @03overmars_finding_sets_points_empty_convex_6_gons #slide( // Hide header by making it background-coloured @@ -705,6 +698,26 @@ theorem holeNumber_6 : holeNumber 6 = 30 := } })) +== 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 @@ -715,9 +728,9 @@ followed with additional effort. #pause Open problems remain: -▸ Horton's construction for $h(7) = h(8) = … = ∞$ hasn't been verified. #pause +▸ 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 +▸ Exact values of $g(k) < ∞$ for $7 ≤ k$ aren't known. #pause ▸ Trust story for large SAT proofs could be improved. From 3bd3138db4cdbfa1a628104c09efb97d259cb51f Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 10 Sep 2024 11:27:49 +0400 Subject: [PATCH 22/22] tweaks --- ITP/slides.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ITP/slides.typ b/ITP/slides.typ index 985a007..edb900b 100644 --- a/ITP/slides.typ +++ b/ITP/slides.typ @@ -423,7 +423,7 @@ A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. #[ #set text(size: 22pt) - *Lemma*. WLOG we can assume that the points $(p_1, ..., p_n)$ satisfy the following properties: + *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$.