Automated Symmetric Constructions in Discrete Geometry

Bernardo Subercaseaux; Ethan Mackey; Long Qian; Marijn J. H. Heule

REVIEW 1 major objections 4 minor 28 references

Automated Symmetric Constructions in Discrete Geometry

T0 review · 1 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proves that the smallest odd-sized everywhere-unbalanced point set has 21 points, and that symmetric 16-point hexagon-free sets need 4-fold or 5-fold symmetry.

desk verdict The positive constructions are real, but the encoding as written cannot produce the paper's own collinear witness, so the minimality claims are unsupported. read the letter →

arxiv 2506.00224 v1 pith:5FNE57G7 submitted 2025-05-30 cs.DM cs.CG

Bernardo Subercaseaux , Ethan Mackey , Long Qian , Marijn J. H. Heule This is my paper

classification cs.DMcs.CG MSC 52C1005D10

keywords rotationalsymmetrySATsolvingErdős–Szekeresproblemeverywhere-unbalancedpointspointrealizabilityconvexpolygonscombinatorialgeometry

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper presents a computational pipeline for discovering rotationally symmetric point sets that satisfy discrete geometric constraints, and uses it to settle two minimality questions in combinatorial geometry. For the everywhere-unbalanced-points problem, which asks for point sets in which every line through two points has an imbalance of at least 2 between its two sides, it proves that the smallest possible set has 12 points, that no odd-sized set with at most 19 points exists, and that a symmetric 21-point set exists, making 21 the minimal odd size and improving on the previously known 23-point configuration. For the Erdős–Szekeres problem, it produces 16-point sets with no convex hexagon that are 4-fold or 5-fold rotationally symmetric, and refutes the existence of a 3-fold symmetric version. The method encodes the geometry as a boolean satisfiability (SAT) problem with rotational symmetry built into the encoding, then realizes abstract solutions as concrete coordinates using a dedicated local-search solver. If the claims are right, previously asymmetric extremal examples gain readable symmetric witnesses and a reusable technique for imposing symmetry in geometric SAT problems.

What carries the argument

The load-bearing device is a set of dynamic point-ordering axioms for the orientation variables, which record for each triple of points whether the triple is oriented clockwise or counterclockwise. Earlier signotope encodings require a fixed left-to-right order of the points, incompatible with rotational symmetry; here the solver itself chooses a linear order through dedicated ordering variables, and the signotope-style clauses are applied relative to that chosen order. Together with the basic CC-system axioms, these clauses are shown to imply the full CC axioms, with the proof reduced to the five-point case. A separate family of collinearity axioms then forces consistent orientations when three points lie on one line, which is essential for the everywhere-unbalanced problem because its configurations necessarily contain collinearities. Symmetry is imposed by merging every orbit of orientation variables under the rotation into a single representative, and redundant constraints are removed orbit by orbit. A purpose-built local-search solver, called Localizer, turns the abstract orientation assignments into explicit coordinates for general-position sets, while the collinear cases are realized by extracting abstract lines and tuning the remaining free coordinates with a numerical global optimizer.

What would settle it

Exhibit a 2-everywhere-unbalanced set with 19 points, with explicit rational coordinates and every pair-line verified to have imbalance at least 2, or exhibit a realizable 3-fold symmetric 16-point set with no convex 6-gon; either would contradict one of the paper's refutation claims.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is twofold. For everywhere-unbalanced points, the previously known 12-point configuration is shown to be the minimum possible size for imbalance 2, and the odd case is settled exactly: no 2-everywhere-unbalanced set with 19 or fewer points exists, while a 3-fold combinatorially symmetric 21-point construction, given by explicit coordinates, does, so 21 is the minimal odd size. For the Erdős–Szekeres problem, the paper finds 16-point general-position sets without a convex 6-gon that are 4-fold and 5-fold rotationally symmetric, enumerates all symmetry-normalized solutions (66 for 4-fold and 948 for 5-fold, with 18 and 92 realizable, respectively), and proves that no 3-fold symmetric such set exists. It also reports that among the 310,187,713 non-isomorphic SAT solutions for a 4-fold symmetric 32-point set without a convex 7-gon, the inner 12 points always form one of six configurations, none realizable, so no realizable 4-fold symmetric 32-point 7-gon-free set exists.

Load-bearing premise

The refutation claims depend on the new ordering rules and collinearity rules never accidentally ruling out a real configuration, and on the SAT solver being right when it reports that no solution exists, since those reports come without independently checkable certificates; the existence claims are coordinate-verified and do not share this risk.

Editorial extensions

If this is right

The even minimum for imbalance 2 is now known to be 12 points, and the odd minimum is 21 points.
The 4-fold and 5-fold 16-point hexagon-free sets give structured, human-readable witnesses that 16 points can avoid a convex 6-gon, alongside the older asymmetric construction.
The dynamic-ordering axioms remove the need for a fixed left-to-right point order, so the same SAT approach can impose rotational symmetry in other discrete-geometry searches.
For the 32-point 7-gon-free case, the enumeration shows every symmetry-normalized SAT solution fails realization at its inner 12 points, so the non-existence is not an artifact of incomplete search.
The 21-point and 16-point existence constructions come with explicit coordinates, so they can be verified directly without relying on the SAT pipeline.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The same symmetry-aware pipeline is a natural first attack on 3-everywhere-unbalanced sets: impose a rotational ansatz, solve the abstract design, then search for coordinates.
The enumeration data suggest a cheap realizability pre-filter: among symmetric hexagon-free solutions, high counts of convex quadrilaterals and low counts of convex pentagons make realization more likely, so a future pipeline could score solutions before spending time on realization.
If the observed tendency for small extremal constructions to admit symmetry continues, proving symmetric constructions for every parameter value at least 7 could give a structured route toward the conjectured Erdős–Szekeres bound.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short take: the paper's positive constructions are real, but its headline minimality claims for the everywhere-unbalanced problem rely on an encoding that, as written, cannot even represent the paper's own 21-point witness.

Credit where it's earned. The dynamic-ordering axioms are a genuinely useful idea: replacing the fixed left-to-right order in signotope axioms with a SAT-chosen order removes a real obstacle to imposing rotational symmetry, and the clause-count improvement over CC systems is significant. The 16-point 4-fold and 5-fold hexagon-free configurations come with explicit coordinates and look correct. The 21-point 2-everywhere-unbalanced configuration in Table 3 is also an explicit, checkable construction. Localizer's reported speedup over the earlier local-search approach is plausible from the evaluation.

The soft spot is load-bearing. Equation (4) in Section 4.1 says that for any four points, if i precedes j,k,l in the dynamic order, then at least one of the triples (i,j,k), (i,j,l), (i,k,l) is oriented counterclockwise. For four collinear points, all three a-literals are false because the collinearity literal c holds for each triple. The antecedent can always be satisfied by choosing i as the least point under the total order. So the Section 4.1 axioms exclude any configuration with four collinear points. Section 4.2 explicitly says the collinearity axioms are added 'in addition to' those axioms, yet the paper's own 21-point 2-EU set in Table 3 has five points on the line y = -1. If the EU encoding really included (4)-(5), the SAT solver could not have produced that model. If (4)-(5) were dropped for the EU runs, then the paper does not actually describe the axiom set used for the UNSAT proofs, and those proofs have no certificates. Either way, the claims that 12 is the minimal even size and 21 the minimal odd size are not supported as written.

The 3-fold no-hexagon-free-16-point result is also an UNSAT claim without a certificate, though it uses general position and so is not contradicted by the same issue; it still deserves checking. The explicit coordinate constructions stand regardless.

This paper is for researchers using SAT in combinatorial geometry and for people following the Erdős-Szekeres and everywhere-unbalanced problems. The methodology is interesting and the positive results are worth engaging with. But the refutation results need a major rewrite: give the exact axiom set used for the EU encodings, or provide certificates, or both.

Recommendation: send to peer review, because the ideas are good and the constructions are real, but expect substantial revision on the soundness side. A referee should ask the authors to reconcile Section 4.1 with their own witness before any minimality claim is accepted.

Referee Report

1 major / 4 minor

Summary. The paper presents a computational pipeline for discovering rotationally symmetric point sets in discrete geometry. It introduces dynamic-ordering axioms that replace the left-to-right ordering of previous signotope encodings, a symmetry-reduction scheme that unifies equivalent orientation variables, and a local-search realizability solver called Localizer. The methodology is applied to two problems: the Erdős–Szekeres problem, for which the authors report 4-fold and 5-fold symmetric 16-point sets with no convex 6-gon and a classification of all realizable such configurations (9 and 46 non-isomorphic examples), and the everywhere-unbalanced-points problem, for which they report a 21-point 2-everywhere-unbalanced configuration and claim it is the minimal odd-sized solution, while also claiming Alon's 12-point construction is the minimal even-sized solution. Explicit coordinates for the main constructions are given in Appendix C, and the code is publicly available.

Significance. If the minimality results were established, the paper would settle the minimal even and odd sizes for 2-everywhere-unbalanced point sets and would introduce a broadly applicable method for embedding rotational symmetry into SAT encodings of geometric problems. The explicit coordinate lists for the 21-point construction and for the 16-point 4-fold and 5-fold no-hexagon configurations are concrete, checkable contributions, and the public release of Localizer with its reported performance is a useful engineering asset. The symmetry reduction via variable unification is a genuinely interesting technique. However, the non-existence and minimality claims rest on UNSAT answers from an encoding whose published description is inconsistent with the paper's own witness, so the headline claims are not currently supported.

major comments (1)

[Section 4.1, Eq. (4); Section 4.2; Appendix C, Table 3] Section 6.2: the conclusion "there does not exist a realizable 4-fold symmetry on 32 points without a 7-gon" is stronger than the evidence described. The footnote explicitly states that the realizer tool "can only determine realizability, not unrealizability," and that for "several" configurations the authors found known unrealizable 10-point subsets. To conclude non-existence for all six inner-12 configurations, the paper must provide a proof of unrealizability for each of those configurations (e.g., an explicit unrealizable subset together with a citation or a formal proof), not merely report that Localizer failed to find a realization.

minor comments (4)

[Appendix D, Proof of Proposition 2] The proof of Proposition 2 concludes by stating that a SAT solver reported Ψ to be unsatisfiable, but no certificate is provided. Since this is a foundational lemma for the completeness of the dynamic-ordering axioms, please include a DRAT certificate or a reproducible script with the exact solver version and parameters.
[Section 5.2] The ad-hoc method for realizing collinear configurations is described only at a high level. The extraction of "abstract lines" from τ, the determination of dependent points, and the exact objective used in the differential_evolution step should be specified so that the coordinates in Table 3 can be independently verified without using the authors' code.
[Section 3.2] The sentence "we can assume without loss of generality that all points whose index is 1 mod 5 are in the bottom-left quadrant" appears in the 4-fold symmetry subsection and seems to be a typo for "1 mod 4"; please correct it.
[Throughout] The manuscript contains numerous missing spaces and typos (e.g., "DR-complete" for ∃R-complete, "MackBook", "weuse", "theset"). A careful proofreading pass is needed.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: coordinate-verified constructions and an imposed symmetry ansatz make the central existence results independent; self-citations are non-load-bearing, while the EU encoding consistency issue is a soundness concern, not a circular reduction.

full rationale

The paper's central existence claims are not circular. The 16-point 4-fold and 5-fold Erdős–Szekeres constructions are verified by explicit coordinate tables (Appendix C, Tables 1 and 2), and the 21-point 2-EU construction is likewise supported by explicit coordinates (Table 3). These results do not derive the target statement from itself; they exhibit a concrete witness. The imposed rotational symmetry is an ansatz constraint built into the SAT encoding, not a parameter fitted to the answer, so the symmetric solutions are not predictions-by-construction. The minimality and nonexistence claims (12-point minimal even, no odd 2-EU set with at most 19 points, no 3-fold 16-point hexagon-free configuration) are UNSAT results, and their validity depends on whether the SAT axioms faithfully capture all geometric configurations. That is a soundness question, not a circularity question. However, as a flagged manuscript-level concern: Section 4.1's dynamic-ordering axiom (4) is proved only for general position, while Section 4.2 states that collinearity axioms are added 'in addition to the axioms in Section 4.1'; as written, a collinear quadruple would falsify axiom (4) under any total order, and Table 3's witness contains five collinear points, so the exact axiom set used for the EU UNSAT refutations is under-specified in the text. This deserves correction or clarification, but it is not a reduction of the geometric conclusion to its own premise. The self-citations ([13], [21], [22]) are motivational, comparative, or machine-checked formalization and are not load-bearing; the Lean formalization in [22] is independent support. Overall, the derivation chain is not circular.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

No new physical or mathematical entities are postulated. The only hand-chosen numbers are solver hyperparameters, and the main unproven premise is the soundness of the collinearity clauses used for the UNSAT claims.

free parameters (1)

Localizer search hyperparameters
Radii, restart threshold, and leaderboard size in Algorithms 1 and 2 are hand-tuned. They affect runtime and search success, but not the correctness of the final explicit coordinate constructions.

assumptions (5)

domain assumption Any finite point set with distinct x-coordinates satisfies the dynamic-ordering axioms from Equations 4 and 5.
Proved as Proposition 1 in Appendix D; needed for the UNSAT minimality arguments to be sound.
domain assumption The collinearity axioms in Section 4.2 are satisfied by every real collinear configuration.
The paper gives an intuitive geometric description but no formal proof. The refutation claims for the everywhere-unbalanced problem depend on these clauses being necessary.
domain assumption The SAT solver, CaDiCaL with all-solution enumeration, returns correct UNSAT answers.
The minimality results are derived from UNSAT results, and no independent certificates are shipped.
ad hoc to paper The inner 12-point configurations in Section 6.2 are unrealizable, as claimed from the realizer's failure and known unrealizable subsets.
The 32-point 7-gon-free conclusion depends on this; the paper does not exhibit a formal certificate for each of the six configurations.
standard math Carathéodory's theorem in the plane: a set in general position is in convex position if and only if every 4-point subset is in convex position.
Used in Section 4.3 to encode the absence of convex k-gons by forbidding convex 4-tuples.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Automated Symmetric Constructions in Discrete Geometry." pith.science (2026). https://pith.science/paper/5FNE57G7

@misc{pith2026250600224,
  author       = {Pith},
  title        = {Pith review of: Automated Symmetric Constructions in Discrete Geometry},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5FNE57G7}},
  note         = {Machine review of arXiv:2506.00224}
}

abstract

We present a computational methodology for obtaining rotationally symmetric sets of points satisfying discrete geometric constraints, and demonstrate its applicability by discovering new solutions to some well-known problems in combinatorial geometry. Our approach takes the usage of SAT solvers in discrete geometry further by directly embedding rotational symmetry into the combinatorial encoding of geometric configurations. Then, to realize concrete point sets corresponding to abstract designs provided by a SAT solver, we introduce a novel local-search realizability solver, which shows excellent practical performance despite the intrinsic $\exists \mathbb{R}$-completeness of the problem. Leveraging this combined approach, we provide symmetric extremal solutions to the Erd\H{o}s-Szekeres problem, as well as a minimal odd-sized solution with 21 points for the everywhere-unbalanced-points problem, improving on the previously known 23-point configuration. The imposed symmetries yield more aesthetically appealing solutions, enhancing human interpretability, and simultaneously offer computational benefits by significantly reducing the number of variables required to encode discrete geometric problems.

Figures

Figures reproduced from arXiv: 2506.00224 by the authors.

**Figure 1.** Examples of geometric constructions with and without symmetry. that such symmetric solutions can be found automatically. We will consider two problems in discrete geometry described below. Erdős-Szekeres. For each integer 𝑘 ě 3, the problem is to find 𝑔(𝑘), the smallest integer such that any set of 𝑔(𝑘) points in the plane, without three on a common line, contains 𝑘 points in convex position. This long-standing prob… view at source ↗

**Figure 2.** Symmetry breaking predicates for pointsets with a 4-fold symmetry. Orientations in red are failing to satisfy the symmetry-breaking predicates. We can then add analogous CL-clauses to enforce that points 9, 10, 11, 12 are inside the convex hull of points 5, 6, 7, 8, and so on. Furthermore, we can assume without loss of generality that all points whose index is 1 mod 5 are in the bottom-left quadrant. To see this, no… view at source ↗

**Figure 3.** Experimental evaluation of the Localizer realizability solver, over orientations obtained from random realizable sets of points (independently uniform in [0, 1] 2 ). Previous approaches took up to 100s for 16 points [21]. (a) 4-fold symmetric. (b) 5-fold symmetric [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Figures from the paper (4 more)

**Figure 4.** Figure 4: Constructions of 16 points in general position without a convex 6-gon. 𝐿 P L is a maximal set of indices (so 𝐿 Ď {1, . . . , 𝑛}) such that 𝜏(𝑖, 𝑗, 𝑘) = 0 for all 𝑖, 𝑗, 𝑘 P [PITH_FULL_IMAGE:figures/full_fig_p011_4.png]

**Figure 5.** Figure 5: The number of 4-gons and 5-gons in realizable and (likely) unrealizable configurations with a 4-fold symmetry (left) and a 5-fold symmetry (right). for 𝑠 P {3, 4, 5}. The formula enforcing a 3-fold symmetry is unsatisfiable, while the formulas with a 4-fold and 5-fold…

**Figure 6.** Figure 6: A 2-everywhere-unbalanced construction on 21 points [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]

**Figure 22.** Figure 22: A 21-point 2-everywhere-unbalanced configuration with simple coordinates [PITH_FULL_IMAGE:figures/full_fig_p020_22.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

[1]

Order,19(3):265–281,September2002

OswinAichholzer,FranzAurenhammer,andHannesKrasser.EnumeratingOrderTypesforSmallPoint SetswithApplications. Order,19(3):265–281,September2002

work page
[2]

Kleitman and Combinatorics: A Celebration,257(2):599–624,November2002

NogaAlon.Researchproblems. Kleitman and Combinatorics: A Celebration,257(2):599–624,November2002

work page
[3]

ArminBiere,TobiasFaller,KatalinFazekas,MathiasFleury,NilsFroleyks,andFlorianPollitt.CaDiCaL2.0. InArieGurﬁnkelandVijayGanesh,editors, Computer Aided Veriﬁcation - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I,volume14681of Lecture Notes in Computer Science,pages133–152.Springer,2024

work page 2024
[4]

DavidConlonandJeckLim.Everywhereunbalancedconﬁgurations,2025

work page 2025
[5]

DiscreteAppliedMathematics ,109(1):67– 94,April2001

StefanFelsnerandHelmutWeil.Sweeps,arrangementsandsignotopes. DiscreteAppliedMathematics ,109(1):67– 94,April2001

work page
[6]

From summetria to symmetry: The making of a revolutionary scientiﬁc concept

GioraandBernardRGoldstein. From summetria to symmetry: The making of a revolutionary scientiﬁc concept. Archimedes: NewStudiesintheHistoryandPhilosophyofScienceandTechnology.Springer,NewYork, NY,2008edition,July2008

work page
[7]

Symmetry in Solutions.Proceedings of the AAAI Conference on Artiﬁcial Intelligence,24(1):77–82,July2010

Marijn Heule and Toby Walsh. Symmetry in Solutions.Proceedings of the AAAI Conference on Artiﬁcial Intelligence,24(1):77–82,July2010

work page
[8]

Journal of Combinatorics,8(3):391–422,June 2017

MarijnJ.H.Heule.Avoidingtriplesinarithmeticprogression. Journal of Combinatorics,8(3):391–422,June 2017

work page 2017

Show all 28 references

[9]

Marijn J. H. Heule. Schur number ﬁve. InProceedings of the Thirty-Second AAAI Conference on Artiﬁcial IntelligenceandThirtiethInnovativeApplicationsofArtiﬁcialIntelligenceConferenceandEighthAAAISymposium on Educational Advances in Artiﬁcial Intelligence,AAAI’18/IAAI’18/EAAI’18...
[10]

In Bernd Finkbeiner and Laura Kovács, editors,Tools and Algorithms for the Construction and Analysis of Systems,pages61–80,Cham,2024.SpringerNatureSwitzerland

MarijnJ.H.HeuleandManfredScheucher.HappyEnding: AnEmptyHexagoninEverySetof30Points. In Bernd Finkbeiner and Laura Kovács, editors,Tools and Algorithms for the Construction and Analysis of Systems,pages61–80,Cham,2024.SpringerNatureSwitzerland

2024
[11]

AUTOMATED SYMMETRIC CONSTRUCTIONS IN DISCRETE GEOMETRY 15

DonaldE.Knuth.AxiomsandHulls.InDonaldE.Knuth,editor, AxiomsandHulls ,LectureNotesinComputer Science,pages1–98.Springer,Berlin,Heidelberg,1992. AUTOMATED SYMMETRIC CONSTRUCTIONS IN DISCRETE GEOMETRY 15

1992
[12]

Extremalproblemsincombinatorialgeometry .Lecturenotesseries.AarhusUniversitet, MatematiskInstitut,1979

YakovShimeonKupitz. Extremalproblemsincombinatorialgeometry .Lecturenotesseries.AarhusUniversitet, MatematiskInstitut,1979

1979
[13]

Master’sthesis,CarnegieMellonUniversity,2025

EthanMackey.Pinwheelsandpolygons: Symmetricrealizationsofpolygon-freepointplacementsviasat. Master’sthesis,CarnegieMellonUniversity,2025

2025
[14]

Bulletin of the American Mathematical Society,37(4):437–458,2000

W.MorrisandV.Soltan.TheErdos-Szekeresproblemonpointsinconvexposition–asurvey. Bulletin of the American Mathematical Society,37(4):437–458,2000

2000
[15]

SIGPLAN Not.,17(9):7–13,September1982

AlanJ.Perlis.Specialfeature: Epigramsonprogramming. SIGPLAN Not.,17(9):7–13,September1982
[16]

Discrete & Computational Geometry,30(3):415–435, September2003

RomPinchasi.LinesWithManyPointsOnBothSides. Discrete & Computational Geometry,30(3):415–435, September2003
[17]

Gansner,editors, Graph Drawing,pages334–344,Berlin,Heidelberg,2010.Springer

MarcusSchaefer.ComplexityofSomeGeometricandTopologicalProblems.InDavidEppsteinandEmdenR. Gansner,editors, Graph Drawing,pages334–344,Berlin,Heidelberg,2010.Springer

2010
[18]

Computational Geometry,91:101670,2020

ManfredScheucher.Twodisjoint5-holesinpointsets. Computational Geometry,91:101670,2020

2020
[19]

Computing in Geometry and Topology,2(1):2:1–2:13,March2023

ManfredScheucher.ASATAttackonErdős-SzekeresNumbersinR^dandtheEmptyHexagonTheorem. Computing in Geometry and Topology,2(1):2:1–2:13,March2023
[20]

Towards an optimal CNF encoding of boolean cardinality constraints

Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In Peter van Beek, editor,Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings,volume3709of Lecture N...

2005
[21]

BernardoSubercaseaux,JohnMackey,MarijnJ.H.Heule,andRubenMartins.Automatedmathematical discoveryandveriﬁcation: Minimizingpentagonsintheplane,2024

2024
[22]

BernardoSubercaseaux,WojciechNawrocki,JamesGallicchio,CaydenCodel,MarioCarneiro,andMarijn J.H.Heule.FormalVeriﬁcationoftheEmptyHexagonNumber.InYvesBertot,TemurKutsia,andMichael Norrish, editors,15th International Conference on Interactive Theorem Proving (ITP 2024), volume 309...

2024
[23]

Computer solution to the 17-point Erdős-Szekeres problem.The ANZIAM Journal,48(2):151–164,2006

George Szekeres and Lindsay Peters. Computer solution to the 17-point Erdős-Szekeres problem.The ANZIAM Journal,48(2):151–164,2006

2006
[24]

Handbook of Discrete and Computational Geometry.ChapmanandHall/CRC,NewYork,3edition,November2017

CsabaD.Toth,JosephO’Rourke,andJacobE.Goodman,editors. Handbook of Discrete and Computational Geometry.ChapmanandHall/CRC,NewYork,3edition,November2017
[25]

Nature Methods,17:261–272,2020

PauliVirtanen,RalfGommers,TravisE.Oliphant,MattHaberland,TylerReddy,DavidCournapeau,Evgeni Burovski,PearuPeterson,WarrenWeckesser,JonathanBright,StéfanJ.vanderWalt,MatthewBrett,Joshua Wilson,K.JarrodMillman,NikolayMayorov,AndrewR.J.Nelson,EricJones,RobertKern,EricLarson,CJ Car...

2020
[26]

TobyWalsh.SymmetrywithinandbetweenSolutions.InByoung-TakZhangandMehmetA.Orgun,editors, PRICAI 2010: Trends in Artiﬁcial Intelligence,pages11–13,Berlin,Heidelberg,2010.Springer

2010
[27]

Symmetry.PrincetonScienceLibrary.PrincetonUniversityPress,Princeton,NJ,December 2016

HermannWeyl. Symmetry.PrincetonScienceLibrary.PrincetonUniversityPress,Princeton,NJ,December 2016

2016
[28]

php?title=Happy%20ending%20problem&oldid=1282669476,2025.[Online;accessed12-May-2025]

Wikipedia.Happyendingproblem—Wikipedia,thefreeencyclopedia.http://en.wikipedia.org/w/index. php?title=Happy%20ending%20problem&oldid=1282669476,2025.[Online;accessed12-May-2025]. AppendixA. Realizationsof4-FoldSymmetricConﬁgurations Below are the nine non-isomorphic realizable...

2025

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Order,19(3):265–281,September2002

OswinAichholzer,FranzAurenhammer,andHannesKrasser.EnumeratingOrderTypesforSmallPoint SetswithApplications. Order,19(3):265–281,September2002

work page

[2] [2]

Kleitman and Combinatorics: A Celebration,257(2):599–624,November2002

NogaAlon.Researchproblems. Kleitman and Combinatorics: A Celebration,257(2):599–624,November2002

work page

[3] [3]

ArminBiere,TobiasFaller,KatalinFazekas,MathiasFleury,NilsFroleyks,andFlorianPollitt.CaDiCaL2.0. InArieGurﬁnkelandVijayGanesh,editors, Computer Aided Veriﬁcation - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I,volume14681of Lecture Notes in Computer Science,pages133–152.Springer,2024

work page 2024

[4] [4]

DavidConlonandJeckLim.Everywhereunbalancedconﬁgurations,2025

work page 2025

[5] [5]

DiscreteAppliedMathematics ,109(1):67– 94,April2001

StefanFelsnerandHelmutWeil.Sweeps,arrangementsandsignotopes. DiscreteAppliedMathematics ,109(1):67– 94,April2001

work page

[6] [6]

From summetria to symmetry: The making of a revolutionary scientiﬁc concept

GioraandBernardRGoldstein. From summetria to symmetry: The making of a revolutionary scientiﬁc concept. Archimedes: NewStudiesintheHistoryandPhilosophyofScienceandTechnology.Springer,NewYork, NY,2008edition,July2008

work page

[7] [7]

Symmetry in Solutions.Proceedings of the AAAI Conference on Artiﬁcial Intelligence,24(1):77–82,July2010

Marijn Heule and Toby Walsh. Symmetry in Solutions.Proceedings of the AAAI Conference on Artiﬁcial Intelligence,24(1):77–82,July2010

work page

[8] [8]

Journal of Combinatorics,8(3):391–422,June 2017

MarijnJ.H.Heule.Avoidingtriplesinarithmeticprogression. Journal of Combinatorics,8(3):391–422,June 2017

work page 2017