Order type / orientation encoding of planar point sets (CC-systems, chirotopes, and the Aichholzer–Aurenhammer–Krasser database)

Statement

Let $P=\{p_1,\dots,p_n\}\subset\mathbb R^2$ be a finite point set in general position (no three collinear). For every ordered triple $(i,j,k)$ define the orientation predicate $$\chi(i,j,k)=\operatorname{sign}\det\begin{pmatrix}1&x_i&y_i\\1&x_j&y_j\\1&x_k&y_k\end{pmatrix}\in\{+1,-1\}$$ (+1 = counterclockwise, −1 = clockwise). The (labeled) order type of $P$ is exactly the function $\chi:\binom{[n]}{3}\times S_3\to\{\pm1\}$ this determinant produces — equivalently, a rank-3 acyclic chirotope / rank-3 oriented matroid on $n$ elements. Two point sets have the *same* order type iff there is a labeling under which every corresponding triple has the same orientation.

This is provably equivalent to two other formalizations, both important for how the concept is *used*:

- Allowable sequences (Goodman & Pollack, 1980s): rotate a directed line through $P$ and record, as a sequence of adjacent transpositions, the permutation of the points' projections onto the line as it sweeps $180°$. The resulting combinatorial sequence of permutations determines and is determined by $\chi$. - CC-systems (Donald Knuth): a purely combinatorial, coordinate-free axiomatization. A ternary relation $pqr$ ("$p,q,r$ counterclockwise") on a finite set is a CC-system iff it satisfies five axioms — cyclic symmetry ($pqr\Rightarrow qrp$), antisymmetry ($pqr\Rightarrow\neg prq$), nondegeneracy ($pqr\ \vee\ prq$ for all distinct $p,q,r$), interiority, and transitivity (en.wikipedia.org/wiki/CC_system). Every order type of a point set in general position is a CC-system, but not every CC-system is realizable as an actual point set (see Facts).

Key structural fact that makes this the right encoding: the order type of $P$ determines — and is exactly the amount of information needed to determine — every property of $P$ that is invariant under order-preserving continuous deformation (any homeomorphism of the plane that never flips a triple's orientation). This includes: which subsets of $P$ are in convex position, the convex hull, every triangulation of $P$, the crossing pattern of the complete straight-line graph on $P$, $k$-sets, and the answer to any Erdős–Szekeres-style Ramsey question. It does not determine metric quantities (distances, areas, angles).

Facts

- Growth-rate gap between "abstract" and "realizable." The number of combinatorially distinct CC-systems on $n$ points grows like $3^{\Theta(n^2)}$ (bounded above by $3^{\binom n2}$), while the number of *realizable* order types grows only like $2^{\Theta(n\log n)}$ (en.wikipedia.org/wiki/CC_system) — most abstract orientation data satisfying the axioms is not geometrically realizable at all. - Small cases are all realizable; larger ones are not. Goodman & Pollack showed every CC-system on $\le 8$ points is realizable as a point set. Bokowski & Sturmfels constructed infinitely many minimal non-realizable simplicial rank-3 oriented matroids/CC-systems, so the gap above is not vacuous — non-realizable "phantom" combinatorial configurations exist and must be screened out in applications that need actual points. - Realizability is hard, not just non-trivial. Mnëv's universality theorem implies that deciding whether a given (abstract) order type / allowable sequence is realizable is complete for $\exists\mathbb R$ (the existential theory of the reals), with $\mathrm{NP}\subseteq\exists\mathbb R\subseteq\mathrm{PSPACE}$ (both containments believed strict) — realizability is as hard as deciding satisfiability of a system of real polynomial equations/inequalities, strictly believed harder than NP. Scheucher (arXiv:1801.05992) extends this universality to allowable sequences and uses it to prove $\exists\mathbb R$-hardness of related recognition problems (abstract convex geometries, visibility graphs of polygons with holes). - Coordinate blow-up. Goodman, Pollack & Sturmfels showed every realizable order type *can* be realized with integer coordinates, but some order types provably require doubly-exponential coordinate size — so "just search small integer grids for a realizer" is not always an option even when a realization exists. - The Aichholzer–Aurenhammer–Krasser database. Aichholzer, Aurenhammer & Krasser ("Enumerating Order Types for Small Point Sets with Applications," *Order* 19(3):265–281, 2002 / SoCG 2001, dl.acm.org/doi/10.1145/378583.378596) built, via an order-type-extension (reverse-search-style) enumeration algorithm, a complete verified catalogue of all realizable order types on $n\le10$ points, each stored together with an explicit small-integer-grid realizing point set; later extended by the same group to $n=11$ (≈2.3 billion order types, ~96–103 GB, queryable/downloadable at the TU Graz page ist.tugraz.at/aichholzer/research/rp/triangulations/ordertypes/). Approximate counts for $n=3,\dots,11$: $1,2,3,16,135,3315,158817,14309547,2334512907$ (moderate-confidence figure, WebSearch-synthesized). - Applications of the database as ground truth. Used directly to brute-force-verify or compute exact small-$n$ values for: triangulation counts, simple polygonalization (Hamiltonian-polygon) counts, counts of plane geometric graphs, $k$-set counts, and rectilinear crossing numbers — because every property depending only on order type can be evaluated by iterating over the finite, complete database instead of over an infinite space of coordinates. - SAT-search backbone. Because $\chi(i,j,k)\in\{\pm1\}$ is a single Boolean variable and the CC-system axioms are compact first-order/clausal constraints over these variables, any question about point configurations of a *fixed* size $n$ can be compiled directly into CNF, entirely bypassing floating-point coordinates. This is the literal mechanism behind Heule & Scheucher's resolution of the empty hexagon number $h(6)=30$ (arXiv:2403.00737: $O(n^4)$-clause CNF built from order-type/CC-system axioms plus the convexity criterion for 6-subsets, UNSAT-for-$n=30$ found after 17,300 CPU-hours; independently re-derived inside Lean by Subercaseaux et al., arXiv:2403.17370), and it is the encoding used by Balko–Valtr (2017) and Bogdan (arXiv:2512.24061, 2025) in their ongoing SAT attacks on $\mathrm{ES}(7)=33$ (Erdős #107 — exact Erdős–Szekeres convex-polygon constant). See SAT/CP-SAT-based finite counterexample search and verification for the general SAT/CDCL/cube-and-conquer machinery this feeds into.

How order type is actually used to prove things (the transferable moves)

1. Reduce an infinite geometric search to a finite combinatorial one. Any statement about a fixed-size point set $P$ that depends only on order type ranges over an *infinite* space of real coordinates but only *finitely many* possible order types — this is what makes bounded-$n$ Erdős–Szekeres-type questions decidable and SAT-attackable at all (Cook–Levin reduction target, via SAT/CP-SAT-based finite counterexample search and verification). Introduce one Boolean variable $x_{ijk}$ per point triple for its orientation, and encode the target property (e.g. "some 6-subset is in convex position and empty," or "no 7-subset is in convex position") as a clause set over these variables. 2. Add CC-system axioms as clauses so satisfying assignments are internally consistent orientation data, not arbitrary sign patterns — this is what a "known order-type/CC-system axiom" encoding buys you (cyclic symmetry, antisymmetry, nondegeneracy, interiority, transitivity as clauses over the $x_{ijk}$). 3. Exploit the realizability-gap direction that works for free. Because every realizable order type satisfies the CC-system axioms (realizable order types $\subseteq$ CC-systems), an UNSAT result over the CC-system-axiom encoding is automatically a proof about the smaller, harder-to-characterize set of *actually realizable* point sets too: "no CC-system of size $n$ has property $X$" $\Rightarrow$ "no realizable point set of size $n$ has property $X$." This is exactly why proving $\varphi_{30}$ UNSAT (no 30-point CC-system avoids an empty convex hexagon) is a fully rigorous proof of $h(6)=30$ for genuine point sets, with no separate realizability check needed — the ideal shape for "every configuration of size $n$ has property $Y$" universal statements. 4. The reverse direction needs an extra step. A SAT result (a satisfying assignment exists) over CC-system axioms alone only proves an *abstract* CC-system with the desired property exists — it does not by itself prove a real point set realizing it exists, because non-realizable CC-systems are common for $n>8$ (Bokowski–Sturmfels). Existence-type questions (e.g. "does a 33-point configuration with no convex 7-gon exist?", the live open direction of $\mathrm{ES}(7)$) therefore require an additional realizability certificate — either checking the witness against the Aichholzer–Aurenhammer–Krasser database directly (for $n\le11$), or an independent stretchability/realizability argument — on top of the raw SAT witness. 5. Use the enumerated database as exhaustive ground truth for $n\le10$–$11$. Instead of encoding-and-solving from scratch, many small-$n$ extremal or enumerative questions (exact triangulation counts, rectilinear crossing numbers, small Erdős–Szekeres/happy-ending sub-cases) can be settled by directly iterating over Aichholzer et al.'s complete, pre-verified, pre-realized order-type list and checking the target property on each entry — a strictly cheaper move than building a fresh SAT encoding when $n$ is small enough that the database already covers it. 6. WHEN this technique applies. Any open problem whose truth value depends only on the combinatorial/order structure of a finite planar point set in general position — convex position and convex polygons/empty polygons (Erdős #107 — exact Erdős–Szekeres convex-polygon constant, Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7)), $k$-sets, crossing numbers of straight-line drawings of $K_n$, Ramsey-type "must some structure appear" questions on point sets, positive-fraction/clustering arguments that Ramsey-color $k$-tuples by which of the finitely many $k$-point order types they realize (Pór–Valtr positive-fraction Erdős–Szekeres theorem: dense clusters, not just points, in convex position). Does not directly apply to genuinely metric statements (distances, areas, angles, unit-distance-type problems) unless the metric content can be isolated from a separate order-type-only combinatorial core.

Related

- Erdős #107 — exact Erdős–Szekeres convex-polygon constant — Erdős–Szekeres convex-polygon problem; the order-type/CC-system SAT encoding (Balko–Valtr 2017, Bogdan 2025) is the live attack route on the open $\mathrm{ES}(7)=33$ sub-case, directly modeled on the resolved sister problem below. - Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7) — the empty hexagon number $h(6)=30$, fully resolved by exactly the CC-system-axiom SAT encoding + UNSAT-certificate + Lean re-derivation pipeline described in Technique steps 2–3; the clearest worked example in this wiki of order type as proof machinery, not just a data structure. - Erdős #651 — higher-dimensional Erdős–Szekeres convex-position numbers are subexponential for d≥3 (disproved) — higher-dimensional ($d\ge3$) Erdős–Szekeres convex-position numbers; order type as defined here is specifically the *planar* (rank-3) case, but the same triple/orientation-predicate idea generalizes to rank-$(d{+}1)$ oriented matroids in higher dimensions, the natural next step if this page's machinery is pushed beyond the plane. - SAT/CP-SAT-based finite counterexample search and verification — the general SAT/CDCL/cube-and-conquer + DRAT-certificate methodology that order-type/CC-system encodings feed into; this page supplies the specific geometry-to-Boolean-variable encoding, that page supplies the solving/verification engine. - Pór–Valtr positive-fraction Erdős–Szekeres theorem: dense clusters, not just points, in convex position — uses "there are only finitely many order types on $k$ points" as a pigeonhole/Ramsey-coloring device (color $k$-tuples of clusters by the order type their transversal realizes) to force positive-fraction convex clustering; a direct example of order-type-finiteness as a *proof* ingredient rather than a *computational search* ingredient. - Incidence geometry: Szemerédi–Trotter theorem, the crossing lemma, and Zarankiewicz-type bounds — sibling combinatorial-geometry toolkit; distinct from order type in that incidence questions (point-line/curve incidences) are governed by algebraic/polynomial-method and Szemerédi–Trotter-type machinery rather than orientation combinatorics, but both are "encode the finite combinatorial skeleton of a point configuration" strategies.