Pith. sign in

REVIEW 3 major objections 7 minor 1 cited by

Constructing Optimal Kobon Triangle Arrangements via Table Encoding, SAT Solving, and Heuristic Straightening

T0 review · 3 major / 7 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read The paper reports new optimal Kobon triangle arrangements for 23 and 27 lines, reaching the known upper bounds of 161 and 225 triangles.

desk verdict Solid computational pipeline, but the claimed proofs for n=23 and 27 rest on heuristic straightening with no exact certificates, so treat the headline results as strong conjectures. read the letter →

arxiv 2507.07951 v1 pith:5LXCV2Z7 submitted 2025-07-10 math.CO

Pavlo Savchuk This is my paper · ORCID
classification math.CO MSC 52C30
keywords KobontriangleslinearrangementspseudolineSATencodingcombinatorialtablesheuristicstraighteningupperboundscomputationalgeometry
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

The paper takes on the Kobon triangle problem, which asks for the largest number of non-overlapping triangles that n straight lines can form. It introduces a compact table notation for pseudoline arrangements, turns the search for optimal tables into a satisfiability (SAT) problem, and then numerically straightens candidate tables into genuine straight-line arrangements. Its headline results are new optimal arrangements for 23 and 27 lines, which meet the known upper bound N(n) = n(n−2)/3 and therefore give N(23) = 161 and N(27) = 225. The same machinery also exhaustively settles several small cases and shows that no pseudoline arrangement with the optimal 33 triangles exists for 11 lines.

What carries the argument

The load-bearing object is the table: a row for each line listing, in order, the other lines that cross it, with groups for multi-line intersections. The table is a combinatorial description of a pseudoline arrangement and supports symmetries and parallel lines. The argument runs through three mechanisms: a CNF encoding with variables expressing which line occupies which column of a row, which line immediately follows another, and which line lies somewhere after another, plus clauses enforcing consistency and optimality; a SAT solver that finds satisfying assignments, i.e., candidate optimal tables; and a heuristic straightening step that represents each line by an angle and a signed distance and minimizes a sum of squared violations so that the prescribed intersection orders hold. The last step is where the combinatorial candidate becomes a concrete arrangement of straight lines.

What would settle it

Run an independent exact-arithmetic check on the Appendix C tables for 23 and 27 lines: attempt to solve for line angles and offsets so that every prescribed crossing order and triangle-side condition holds with zero violation, or produce a realizability certificate for those tables. If no such exact configuration exists, or if a consistency contradiction is found between the table and the geometry of straight lines, the central claims N(23) = 161 and N(27) = 225 are false.

Watch

Extended reading notes

Core claim

The central claim, stated on the paper's own terms, is that the search for optimal Kobon arrangements can be fully automated and that this automation yields new extremal configurations. For line counts n with n mod 6 ∈ {3, 5}, an arrangement attaining the upper bound must use every finite non-overlapping segment as the side of some triangle, which lets the author encode optimality directly as ordering constraints in CNF. A SAT solver applied to those constraints produces candidate tables, and a constrained numerical minimization over line angles and signed distances recovers straight-line drawings. The outcome is a table for 23 lines realizing 161 triangles and two tables for 27 lines realizing 225 triangles, matching the upper bound in each case, together with complete enumeration for n = 3, 5, 9, 15, 17 and a nonexistence result for the 11-line optimum.

Load-bearing premise

The load-bearing premise is that the heuristic straightening step really produces straight lines satisfying the table's ordering constraints for 23 and 27 lines; the paper gives no exact coordinates or certificates, only near-zero values of a numerically minimized target function, and if that fitting fails the claimed proofs of N(23) = 161 and N(27) = 225 collapse.

Editorial extensions

If this is right

  • If the 23- and 27-line constructions are accepted, N(23) = 161 and N(27) = 225, both equal to the upper bound n(n−2)/3, so no arrangement with more triangles can exist for those counts.
  • The 24-line arrangement with 172 triangles, built by inserting a line into the 23-line solution, provides a new benchmark for even n and suggests similar insertions from other odd solutions.
  • The SAT-based search can certify nonexistence: for 11 lines no pseudoline table with 33 triangles exists, so the optimal 33-triangle configuration cannot be realized even before straightening.
  • Because the same pipeline reproduces previously known optimal arrangements and can enforce mirror or rotational symmetry, it gives a transferable method for attacking larger n.

Reading between the lines

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

  • If the table-and-SAT pipeline were extended to other residue classes by systematically adding missing-triangle variables, the same machinery could test whether other known upper bounds are sharp for small even n and for other congruence classes of n.
  • Because the straightening step is heuristic, a numerically fitted table is evidence rather than proof; replacing it with exact algebraic verification or a realizability certificate would turn these constructions into fully verified theorems.
  • The table notation is close to an order-type encoding, so linking table realizability to oriented-matroid theory could let the SAT search exclude unstraightenable pseudoline arrangements at the combinatorial stage.
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.

Referee Report

3 major / 7 minor

Summary. The paper introduces a compact table notation for encoding pseudoline arrangements and a SAT-based CNF model for searching optimal Kobon triangle arrangements, together with a heuristic straightening method based on numerical optimization. The authors report new optimal arrangements for 23 and 27 lines, claiming that these establish N(23)=161 and N(27)=225, and they also report the absence of a 33-triangle arrangement for 11 lines, along with several other computational results. The tools are released as open-source repositories, and the paper includes reproduction of many previously known optimal arrangements as a sanity check.

Significance. If the 23- and 27-line claims are correct, the paper settles two open instances of the Kobon triangle problem and demonstrates a potentially powerful computational pipeline combining pseudoline table encodings, SAT solving, and numerical straightening. The reproduction of known optimal arrangements and the n=11 negative result are useful validations of the framework. However, the claimed proofs currently depend on a heuristic optimization step that does not provide exact coordinates or certificates, and the CNF-to-table equivalence is asserted rather than rigorously established. The framework is promising, but the central claims are not yet backed by complete mathematical evidence.

major comments (3)
  1. [Section 4.4 and Table 1] The claimed proofs of N(23)=161 and N(27)=225 require an actual straight-line arrangement attaining the upper bound, but the bridge from the Appendix C tables to straight lines is a heuristic numerical optimization that explicitly accepts nonzero target-function values, and for n=27 it requires a hand-chosen coefficient (0.5, Table 1 footnote). Since the Appendix C tables are only order data for pseudolines and not every pseudoline arrangement is stretchable, the existence of the required straight-line arrangements is not established. Please provide exact coordinates (or a rigorous stretchability certificate, e.g., rational coordinates verified by exact arithmetic) for the 23- and 27-line arrangements, and a programmatic check that all 161/225 triangles are bounded and non-overlapping. Without this, the statements 'proving N(23)=161' and 'proving N(27)=225' in Section 3.3 and Appendix C should be weakened to computational evidence.
  2. [Section 3.2, Rule 12] The soundness and completeness of the CNF encoding are asserted without proof. Rule 12 is described as enforcing 'Consistency + Optimality' by using the same clauses for G and X, but no theorem states that a satisfying assignment corresponds exactly to a table of an optimal Kobon arrangement, including the handling of parallel lines and multiple-intersection points. This is load-bearing for all SAT-based results, including the n=11 unsat conclusion in Section 5 ('cannot be built even with pseudolines') and the enumeration claims for n in {3,5,9,15,17}. Please provide a precise formal statement and proof, or at least a rigorous argument, that the clause set is satisfiable if and only if a valid optimal table exists for the specified n values.
  3. [Section 3.3 and Conclusion] For n=23, Table 1 records the search as non-exhaustive ('≥ 65', '≥ 6', footnote d), which is acceptable for an existence proof, but the paper's broader enumeration claims need careful scoping. In the Conclusion, the statement 'for n ∈ {3,5,9,15,17} we enumerate all possible Kobon arrangements' is ambiguous: it must specify what 'possible' means (all missing-triangle multisets? all symmetry classes? all tables satisfying the CNF model?) and must be conditional on the CNF model's completeness. Without this, the enumeration claim is unsupported. Please specify the exact scope of each exhaustive search and the configurations covered.
minor comments (7)
  1. [Section 3.1] In the definition of variable X(r,i,j), the text says 'line j is somewhere after line j'; this should read 'line j is somewhere after line i'.
  2. [Section 2.1] The table construction for multiple-line intersections is under-specified: clarify how groups are ordered when more than three lines meet at a single point, and explain how parallel lines are handled in the CNF model in Section 3.
  3. [Table 1] Table 1 is very hard to parse: the columns for -M, -R, -L, tabs, fit, and the various timing columns are not cleanly aligned, and the footnote markers are ambiguous. Please reformat the table with separate flag columns and numeric count columns, and ensure each row is legible.
  4. [Section 4.4] The statement that 'nonzero values often correspond to perfectly acceptable solutions' needs a precise fail criterion; state the tolerance used and how the final arrangement is validated (for example, by recomputing the triangle count with a separate routine and by checking that all ordering constraints are satisfied).
  5. [Appendix A] The arrangements in Appendix A are given as decimal approximations and symbolic epsilon values; since these are claimed to be straight-line realizations, provide exact rational expressions for the coefficients or state clearly that they are numerical approximations only.
  6. [References] Reference [1] is incomplete: it lists only 'Handbook of discrete and computational geometry. chapter 5, page 126' without authors, editors, or title; please complete the citation.
  7. [Abstract and Conclusion] The abstract mentions 'several other new results' without specifying them; please enumerate these results explicitly in the Conclusion (for example, the 24-line 172-triangle arrangement and the 22- and 28-line variants mentioned in Section C.2).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the upper bounds are external, the SAT search is contentful, and the straightening is a numerical construction rather than a restatement of the target.

full rationale

The paper's derivation chain is: cite external upper bounds N(n) <= n(n-2)/3 for n congruent to 3 or 5 mod 6 from [3,5]; encode candidate pseudoline arrangements as tables; use the external optimality fact that an arrangement attaining the bound has every finite segment as a side of a triangle ([5]) to write CNF clauses; run Kissat to obtain tables; then use a separate SciPy minimization (Section 4.4) to realize the table by straight lines. None of these steps defines the target result in terms of itself. The CNF model does not assume the existence of a 23- or 27-line solution; it searches for it, and for n=11 the same model proves nonexistence of an optimal table. The upper-bound results [3,5] are not self-citations. The only self-references, [14,15], are software artifacts for reproducibility, and the mathematical load is not carried by an author-uniqueness theorem. The hand-tuned coefficient 0.5 for n=27 is an optimization parameter, not a fitted prediction of the triangle count. The heuristic straightening's acceptance of near-zero target values (Section 4.4) is a verification/rigor gap: without exact coordinates or stretchability certificates the existence claims are computational conjectures. That concern belongs to correctness risk, not to circularity, since the claim does not reduce to its inputs by construction.

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

The paper introduces no new physical or mathematical entities. Its results rest on external upper bounds, an unverified encoding, and a heuristic optimizer with hand-tuned coefficients.

free parameters (3)
  • main coefficient = 0.5 (for n=27; 1.0 default otherwise)
    Hand-chosen optimizer weight in the target function (Table 1 footnote) needed to make the 27-line straightening succeed; the result depends on this choice.
  • optimizer bounds AMIN, AMAX, CMIN, CMAX, INEQMAX, INEQepsilon = not specified numerically
    Bounds and slack parameters in Sections 4.1 and 4.2 control which tables can be straightened; they are chosen without derivation from the geometry.
  • epsilon values in Appendix A = 1/(2n) for n=5,7,9,13,17
    Small offsets used to position near-vertical lines in the special small-n arrangements; they are not part of the 23/27 central claim.
assumptions (5)
  • domain assumption Upper bound N(n) <= n(n-2)/3 for n mod 6 in {3,5}
    Taken from Bartholdi-Blanc-Loisel [3] and Clement-Bader [5]; the search targets this bound.
  • domain assumption Optimal arrangements meeting the upper bound have every finite non-overlapping segment as a triangle side
    Invoked in Section 3 to justify the CNF optimality clauses; referenced to [5].
  • ad hoc to paper The table notation of Section 2 faithfully encodes all relevant pseudoline arrangements, including parallel and multiple-intersection cases
    Stated constructively but not formally proved; the SAT encoding assumes this completeness.
  • ad hoc to paper The CNF clauses in Section 3.2, especially rule 12, are sound and complete for optimal Kobon arrangement tables
    Asserted with example clauses but no proof; the n=11 no-solution result depends on this.
  • domain assumption Kissat's unsat answers are correct and the generated CNF is satisfiability-equivalent to the table conditions
    The paper trusts a SAT solver return as proof of unsatisfiability; no certificate or independent check is provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Constructing Optimal Kobon Triangle Arrangements via Table Encoding, SAT Solving, and Heuristic Straightening." pith.science (2026). https://pith.science/paper/5LXCV2Z7

@misc{pith2026250707951,
  author       = {Pith},
  title        = {Pith review of: Constructing Optimal Kobon Triangle Arrangements via Table Encoding, SAT Solving, and Heuristic Straightening},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5LXCV2Z7}},
  note         = {Machine review of arXiv:2507.07951}
}
read the original abstract

We present new methods and results for constructing optimal Kobon triangle arrangements. First, we introduce a compact table notation for describing arrangements of pseudolines, enabling the representation and analysis of complex cases, including symmetrical arrangements, arrangements with parallel lines, and arrangements with multiple-line intersection points. Building on this, we provide a simple heuristic method and tools for recovering straight-line arrangements from a given table, with the ability to enforce additional properties such as symmetries. The tool successfully recovers arrangements for many previously known optimal solutions. Additionally, we develop a tool that transforms the search for optimal Kobon arrangement tables into a SAT problem, allowing us to leverage modern SAT solvers (specifically Kissat) to efficiently find new solutions or to show that no other solutions exist (for example, confirming that no optimal solution exists in the 11-line case). Using these techniques, we find new optimal Kobon arrangements for 23 and 27 lines, along with several other new results.

Figures

Figures reproduced from arXiv: 2507.07951 by the authors.

Figure 1
Figure 1. Some simpler arrangements and their tables. In this paper, we always use the topmost [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. For three different lines r, i, and j, there are only twelve possible ways they can form a triangle (grouped into six classes by the ordering: rij, rji, . . . , jir). 2.2 Properties Because tables are restricted by the logic of how (pseudo)lines can behave, they have many useful properties. Only some of these properties are listed here; an exhaustive and formalized set of properties for optimal Kobon arrangements wi… view at source ↗
Figure 3
Figure 3. Optimal arrangements found by kobon-cnf for n ∈ {3, 5, 7, 9, 13, 15, 17, 19}. For n ∈ {13, 19}, other arrangements could exist (for example, with different lines having missing triangles). 9 [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Every unique optimal arrangement for n = 13 where line #6 and line #9 lack a triangle, as found by kobon-cnf [15], shown with their respective tables. For a given line i, two consecutive entries j and k in the i-th table row specify that line j must intersect line i be…
Figure 5
Figure 5. Figure 5: These images show how the described techniques can be used to improve visual presentation. [PITH_FULL_IMAGE:figures/full_fig_p015_5.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Enumeration and Classification of Triangle-Maximal Pseudoline Arrangements

    math.CO 2026-07 conditional novelty 7.0 of 10

    Exhaustive enumeration and classification of triangle-maximal pseudoline arrangements for all odd n ≤ 27, with symmetry groups per projective class and existence settled for all odd n ≤ 89 except n = 11.

Reference graph

Works this paper leans on

18 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [1]

    chapter 5, page 126

    Handbook of discrete and computational geometry. chapter 5, page 126. Chapman and Hall/CRC, 3rd edition, 2017

    work page 2017

  2. [2]

    Kobon triangles

    Johannes Bader. Kobon triangles. https://www.sop.tik.ee.ethz.ch/people/baderj/other.html. Accessed: 2025-07-04

    work page 2025

  3. [3]

    On simple arrangements of lines and pseudo-lines in P2 and R2 with the maximum number of triangles

    Nicolas Bartholdi, J´ er´ emy Blanc, and S´ ebastien Loisel. On simple arrangements of lines and pseudo-lines in P2 and R2 with the maximum number of triangles. 07 2007

    work page 2007

  4. [4]

    arminbiere/kissat

    Armin Biere. arminbiere/kissat. https://github.com/arminbiere/kissat, jun 28 2025. 20

    work page 2025

  5. [5]

    Cl´ ement and J

    G. Cl´ ement and J. Bader. Tighter Upper Bound for the Number of Kobon Triangles. Draft Version, 2007

    work page 2007

  6. [6]

    Complete enumeration of small realizable oriented matroids

    Komei Fukuda, Hiroyuki Miyata, and Sonoko Moriyama. Complete enumeration of small realizable oriented matroids. Discrete & Computational Geometry , 49(2):359–381, Mar 2013

    work page 2013

  7. [7]

    Harris, K

    Charles R. Harris, K. Jarrod Millman, St´ efan J. van der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J. Smith, Robert Kern, Matti Picus, Stephan Hoyer, Marten H. van Kerkwijk, Matthew Brett, Allan Haldane, Jaime Fern´ andez del R ´ ıo, Mark Wiebe, Pearu Peterson, Pierre G´ erard-Marchant, Ke...

    work page 2020

  8. [8]

    J. D. Hunter. Matplotlib: A 2d graphics environment. Computing in Science & Engineering , 9(3):90–95, 2007

    2007

Show all 18 references
  1. [9]

    SAT-Based Generation of Planar Graphs

    Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. SAT-Based Generation of Planar Graphs. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) , volume 271 of Leibniz Internation...

    2023

  2. [10]

    The On-Line Encyclopedia of Integer Sequences, 2025

    OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences, 2025. Published electronically at http://oeis.org

    2025

  3. [11]

    The most general position

    G¨ unter Rote. The most general position. https://page.mi.fu-berlin.de/rote/Papers/slides/ Most+general+position-TUM-May-2015.pdf , 2015. Presentation at TU Munich, May 2015

    2015

  4. [12]

    NumPSLA: An experimental research tool for pseudoline arrangements and order types

    G¨ unter Rote. NumPSLA: An experimental research tool for pseudoline arrangements and order types. https://github.com/guenterrote/NumPSLA, 2024

    2024

  5. [13]

    Numpsla – an experimental research tool for pseudoline arrangements and order types

    G¨ unter Rote. Numpsla – an experimental research tool for pseudoline arrangements and order types. https://arxiv.org/abs/2503.02336, 2025

    2025 arXiv

  6. [14]

    Lineorder - a tool for finding straight line arrangements from pseudolines and generating svg visuals

    Pavlo Savchuk. Lineorder - a tool for finding straight line arrangements from pseudolines and generating svg visuals. https://github.com/zegalur/line-order, 2025. Accessed: 2025-06-26

    2025

  7. [15]

    Sat-based solver for the kobon triangle problem using kissat and lineorder

    Pavlo Savchuk. Sat-based solver for the kobon triangle problem using kissat and lineorder. https: //github.com/zegalur/kobon-cnf, 2025. Accessed: 2025-06-26

    2025

  8. [16]

    Oliphant, Matt Haberland, Tyler Reddy, David Cournapeau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, St´ efan J

    Pauli Virtanen, Ralf Gommers, Travis E. Oliphant, Matt Haberland, Tyler Reddy, David Cournapeau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, St´ efan J. van der Walt, Matthew Brett, Joshua Wilson, K. Jarrod Millman, Nikolay Mayorov, Andrew R. J. Nelson,...

    2020

  9. [17]

    Weisstein

    Eric W. Weisstein. Kobon triangle. From MathWorld—A Wolfram Web Resource. Accessed: 2025-06-26

    2025

  10. [18]

    Kobon triangle problem — Wikipedia, the free encyclopedia

    Wikipedia. Kobon triangle problem — Wikipedia, the free encyclopedia. http://en.wikipedia. org/w/index.php?title=Kobon%20triangle%20problem&oldid=1296397787, 2025. [Online; accessed 27-June-2025]. 21

    2025

Pith tools

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