Pith. sign in

REVIEW 5 minor 1 cited by

Toward Satisfiability Modulo Realizability

T0 review · 0 major / 5 minor · reviewed 2026-07-12 · grok-4.5

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

Pith's one-line read The largest set of points with no empty convex hexagon and no convex heptagon has size exactly 23.

desk verdict They settle h(6,7)=24 with an explicit 23-point integer witness and a reusable SAT+Localizer pipeline whose flippability heuristic is the real novelty. read the letter →

arxiv 2607.02958 v1 pith:YAMJB4QG submitted 2026-07-03 cs.CG math.CO

Andrew Krapivin , Benjamin Przybocki , Marijn J. H. Heule This is my paper · ORCID
classification cs.CGmath.CO MSC 52C1068Q17
keywords discretegeometrySATsolvingordertypesrealizabilityhappyendingproblemexistentialtheoryoftherealsPointflippability
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

Many problems in discrete geometry are complete for the existential theory of the reals, so exact encodings are hard for SAT. This paper introduces satisfiability modulo realizability: encode an under-approximation of the geometry as a SAT problem over abstract order types, then guide a search toward the rare realizable ones. Diversity sampling, feedback from partial realizations, and a flippability heuristic (omitting orientation variables that can flip while remaining abstractly feasible) make the search succeed where naive enumeration fails. The method settles an open case of the happy-ending problem by constructing thousands of 23-point sets with neither a 6-hole nor a 7-gon, matching a prior upper bound of 24. A reader cares because the same pipeline recovers known constructions for related problems without any problem-specific geometric code, showing a practical route for computer-assisted discovery beyond pure SAT.

What carries the argument

Satisfiability modulo realizability (PointSAT): SAT encoding of geometric constraints over abstract order types, diversity-driven generation of abstract solutions, omission of flippable orientation constraints, and Localizer search for (partial) realizations that are then re-checked for combinatorial validity.

What would settle it

Independent verification that the published 23-point integer configuration actually contains a 6-hole or a 7-gon, or discovery of any 24-point set that avoids both.

Watch

Extended reading notes

Core claim

The largest point set in the plane in general position that contains neither an empty convex hexagon nor a convex heptagon has size 23 (hence h(6,7)=24). The claim is witnessed by an explicit integer-coordinate configuration of 23 points and by more than a thousand additional realizations produced by the PointSAT solver; the matching upper bound of 24 was already known.

Load-bearing premise

Dropping the flippable orientations and accepting imperfect partial realizations still produces combinatorially valid geometric solutions often enough for the search to succeed.

Editorial extensions

If this is right

  • h(6,7) is settled at 24 with an explicit construction of size 23.
  • The same pipeline recovers known constructions for 26 points without 5-caps or 7-gons and for 29 points without 6-holes, without specialized geometric primitives.
  • Many orientation constraints in these geometric solutions are non-critical and can be safely omitted during realization search.
  • Generating many diverse realizations becomes practical, enabling selection of visually clean integer embeddings.

Reading between the lines

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

  • The flippability observation may transfer to other combinatorial configuration spaces that admit SAT under-approximations.
  • Hybrid SAT-plus-local-search pipelines of this form could be tried on further open existential-theory-of-the-reals problems whose combinatorial skeletons encode cleanly.
  • The scarcity of flippable orientations on larger instances (e.g., 32 points) already signals a scaling barrier that future heuristics will need to address.
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

0 major / 5 minor

Summary. The paper introduces PointSAT, a SAT-based framework (satisfiability modulo realizability) for finding realizable point configurations in the plane that satisfy combinatorial constraints expressible via abstract order types. It encodes an underapproximation of the geometric problem as a SAT instance over orientation variables, then uses diversity-driven sampling of abstract solutions (via clause scrambling), partial-realization feedback from the Localizer local-search tool, and a novel flippability heuristic that drops orientation constraints corresponding to flippable variables before calling Localizer. The method is applied to variants of the Erdős–Szekeres happy-ending problem; the central result is Theorem 1, which states that the largest set of points in general position with no 6-hole and no 7-gon has size 23 (hence h(6,7)=24), witnessed by an explicit integer-coordinate configuration of 23 points (Figure 1) together with more than a thousand additional realizations. Supporting experiments recover known constructions (26 points with no 5-cap or 7-gon; 29 points with no 6-hole) and include ablations (Table 1) and statistics on flippable orientations and violation counts.

Significance. If the explicit 23-point witness is correct (which can be verified independently by computing orientations), the paper settles the last nontrivial case of h(k,ℓ) for k≤6, closing an open question left by Heule & Scheucher. Beyond the concrete theorem, the work supplies a reusable, publicly available pipeline that systematically searches for realizable order types on problems whose naïve SAT encodings produce overwhelmingly unrealizable abstract solutions. The three heuristics—especially the empirically motivated flippability omission—are shown by ablation to be essential for obtaining any solutions, and the same pipeline recovers previously known constructions without problem-specific algorithms. This constitutes a genuine advance in computer-assisted discrete geometry for ∃ℝ-complete problems and demonstrates that SMT-style interfacing can resolve open existence questions in pure mathematics.

minor comments (5)
  1. Section 4.2 heading contains a typographical space (“T esting”); similar minor OCR/spacing artifacts appear elsewhere and should be cleaned.
  2. Figure 3 and Figures 4–7 would benefit from explicit axis labels and a short caption note clarifying that the top-percentile outliers have already been removed (as stated in the footnote).
  3. The description of how flippable variables are identified (Section 4.3) is clear, but a one-sentence remark on the computational cost of the flip checks (relative to the subsequent Localizer calls) would help readers gauge practicality for larger n.
  4. Table 2 lists many hull-layer signatures; a brief remark on whether any of the rare signatures that appear only among abstract solutions (never among realized ones) can be ruled out a priori would strengthen the discussion of Theorem 2.
  5. The integer-grid post-processing pipeline that produced Figure 1 is described only at a high level; a short pseudocode or reference to the annealing scripts would improve reproducibility of the “pretty” drawing.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 1 is an existence claim witnessed by an explicit, independently checkable 23-point configuration; the matching upper bound and the SAT/Localizer tools are external inputs, not self-definitions of the result.

full rationale

The paper's central claim (Theorem 1 / h(6,7)=24) is settled by two independent pieces: (i) the already-published upper bound h(6,7)≤24 of Heule & Scheucher, and (ii) an explicit integer-coordinate 23-point set (Figure 1) whose orientations can be verified by direct computation to contain neither a 6-hole nor a 7-gon. The SAT encoding of abstract order types, the order-type axioms, and the combinatorial definitions of holes/gons/caps are standard and do not encode the target size. Diversity sampling, partial-realization checking, and the flippability heuristic are search heuristics that improve the frequency with which Localizer returns a usable witness; they are not parameters fitted to force size 23, nor do they redefine realizability. Self-citations to Localizer and to the prior upper-bound paper supply a theory solver and a matching bound; neither is a uniqueness theorem that forbids alternatives, nor an ansatz that smuggles the construction into the premises. Ablations (Table 1) and recovery of known constructions further corroborate the pipeline but are not required once a concrete, checkable witness exists. Consequently the derivation chain does not reduce by construction to its own inputs.

Assumptions & free parameters 2 free parameters · 4 assumptions · 2 invented entities

The existence claim rests on standard combinatorial axioms of order types, the correctness of the SAT encoding of holes and gons (imported from prior work), and the empirical reliability of Localizer plus the three new heuristics. No free parameters are fitted to produce the size-23 witness; timeouts and sampling budgets affect only the rate at which solutions are found, not the validity of any found solution.

free parameters (2)
  • Localizer timeout = 15 seconds
    Fixed at 15 s per abstract solution; chosen for throughput, not fitted to force existence.
  • number of abstract solutions sampled = ~174k–200k
    Hundreds of thousands generated on a supercomputer; larger budgets simply increase the chance of finding a realization, they do not alter the combinatorial claim.
assumptions (4)
  • standard math Order-type axioms (signotope axioms) correctly under-approximate realizable orientations of point sets in general position.
    Standard since Goodman–Pollack / Knuth; used throughout Sections 3–4.
  • domain assumption The SAT encoding of k-holes, ℓ-gons and k-caps given by Heule–Scheucher is sound and complete for abstract order types.
    Imported from the cited TACAS 2024 paper; correctness of the encoding is assumed rather than re-proved.
  • domain assumption Localizer returns a realization (or a useful partial realization) with non-negligible frequency whenever the input abstract order type is realizable.
    Empirical claim about the prior local-search tool; the whole pipeline’s success rate depends on it.
  • ad hoc to paper Omitting flippable orientation variables does not systematically destroy all realizable solutions of the geometric problem.
    The novel heuristic of Section 4.3; justified only by the experimental observation that ~90 % of the resulting partial realizations remain solutions.
invented entities (2)
  • satisfiability modulo realizability (PointSAT architecture)
    purpose: Interface a SAT solver with a realizability oracle while exchanging only limited information (diversity samples, partial realizations, flippable literals).
    New algorithmic paradigm introduced in the paper; no independent prior definition.
  • flippability heuristic
    purpose: Identify orientation variables that can be flipped while preserving SAT satisfaction and drop the corresponding constraints before calling Localizer.
    Core novel technique of Section 4.3; its utility is demonstrated only inside the experiments of this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Toward Satisfiability Modulo Realizability." pith.science (2026). https://pith.science/paper/YAMJB4QG

@misc{pith2026260702958,
  author       = {Pith},
  title        = {Pith review of: Toward Satisfiability Modulo Realizability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YAMJB4QG}},
  note         = {Machine review of arXiv:2607.02958}
}
abstract

Problems complete for the existential theory of the reals ($\exists \mathbb{R}$) arise throughout discrete geometry. We introduce satisfiability modulo realizability, a SAT-based approach for solving satisfiable instances of $\exists \mathbb{R}$ whose solutions correspond to realizable geometric configurations. Our method encodes an underapproximation of a geometric problem as a SAT instance over abstract order types. Since almost all abstract order types are unrealizable, naive search is infeasible. We guide the search toward realizable order types using diversity-driven sampling, partial realizability feedback, and a novel flippability heuristic that passes only limited information between components. We apply our method to discrete geometry problems and resolve an open problem by showing that the largest set of points avoiding empty convex hexagons and convex heptagons is of size 23.

Figures

Figures reproduced from arXiv: 2607.02958 by the authors.

Figure 1
Figure 1. A set of 23 points with no 6-hole or 7-gon [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A 5-cap Let a k-cap be a sequence of points p1, . . . , pk with increasing x-coordinates such that pi+2 lies below the line from pi to pi+1 for all i ∈ [k − 2]. PointSAT can find a set of 26 points with no 5-cap or 7-gon. The existence of such a set follows from a theorem of Erdős, Tuza, and Valtr [12], al￾though PointSAT works without relying on any problem-specific knowledge. PointSAT can also find a set of 29 poi… view at source ↗
Figure 3
Figure 3. Distribution of number of violations in the best partial realizations [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Number of flippable orientations [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]
Figure 5
Figure 5. Figure 5: Number of violations applied to study small cases of the Williamson conjecture [5], a problem from design theory, and to improve the bounds on the minimum Kochen–Specker prob￾lem [28], a problem from quantum mechanics. Another SMT-style paradigm is satisfiability modul…
Figure 6
Figure 6. Figure 6: Probability of being a solution versus number of violations [PITH_FULL_IMAGE:figures/full_fig_p015_6.png]
Figure 7
Figure 7. Figure 7: Proportion of solutions with a given number of violations [PITH_FULL_IMAGE:figures/full_fig_p015_7.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. Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

    cs.LO 2026-07 accept novelty 8.0 of 10 full

    Exact rational case-tree certificates, replayed by a sound Lean checker, prove non-embeddability in R³ for all 180 distinct graphs in the published blocking database.

Reference graph

Works this paper leans on

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

  1. [1]

    In: Yokoyama, K., Linton, S., Robertz, D

    Ábrahám, E.: Building bridges between symbolic computation and satisfiability checking. In: Yokoyama, K., Linton, S., Robertz, D. (eds.) Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, IS- SAC 2015, Bath, United Kingdom, July 06 - 09, 2015. pp. 1–6. ACM (2015), https://doi.org/10.1145/2755996.2756636

    work page doi:10.1145/2755996.2756636 2015

  2. [2]

    Barba, L., Duque, F., Fabila-Monroy, R., Hidalgo-Toscano, C.: Drawing the Horton set in an integer grid of minimum size. Comput. Geom.63, 10–19 (2017), https: //doi.org/10.1016/j.comgeo.2017.02.002

    work page doi:10.1016/j.comgeo.2017.02.002 2017

  3. [3]

    In: Berre, D.L., Järvisalo, M

    Biere, A., Heule, M.: The effect of scrambling CNFs. In: Berre, D.L., Järvisalo, M. (eds.) Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018. EPiC Series in Computing, vol. 59, pp. 111–126. EasyChair (2018), https://doi.org/10.29007/9dj5

    work page doi:10.29007/9dj5 2015

  4. [4]

    Brakensiek, J., Heule, M., Mackey, J., Narváez, D.E.: The resolution of Keller’s conjecture. J. Autom. Reason.66(3), 277–300 (2022), https://doi.org/10.1007/ s10817-022-09623-5

    2022

  5. [5]

    Bright, C., Kotsireas, I.S., Ganesh, V.: Applying computer algebra systems with SAT solvers to the Williamson conjecture. J. Symb. Comput.100, 187–209 (2020), https://doi.org/10.1016/j.jsc.2019.07.024

    work page doi:10.1016/j.jsc.2019.07.024 2020

  6. [6]

    In: Prac- tice and Experience in Advanced Research Computing 2021: Evolution Across All Dimensions

    Brown, S.T., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.A.: Bridges-2: A platform for rapidly-evolving and data intensive research. In: Prac- tice and Experience in Advanced Research Computing 2021: Evolution Across All Dimensions. PEARC ’21, Association for Computing Machinery, New York, NY, USA (2021). https://doi.org/10.1145/34373...

    doi:10.1145/3437359.3465593 2021

  7. [7]

    Algorithmica5(4), 561–571 (1990), https://doi.org/10.1007/BF01840404

    Dobkin, D.P., Edelsbrunner, H., Overmars, M.H.: Searching for empty convex poly- gons. Algorithmica5(4), 561–571 (1990), https://doi.org/10.1007/BF01840404

    work page doi:10.1007/bf01840404 1990

  8. [8]

    Discrete Comput

    Duque, F., Fabila-Monroy, R., Hidalgo-Toscano, C.: Point sets with small integer coordinates and no large convex polygons. Discrete Comput. Geom.59(2), 461–476 (2018), https://doi.org/10.1007/s00454-017-9931-6

    work page doi:10.1007/s00454-017-9931-6 2018

Show all 39 references
  1. [9]

    Compositio Math

    Erdős, P., Szekeres, G.: A combinatorial problem in geometry. Compositio Math. 2, 463–470 (1935), http://www.numdam.org/item?id=CM_1935__2__463_0

    1935

  2. [10]

    Erdős, P., Szekeres, G.: On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math.3/4, 53–62 (1960/61)

    1960

  3. [11]

    In: Relations betweencombinatoricsandotherpartsofmathematics(Proc.Sympos.PureMath., Ohio State Univ., Columbus, Ohio, 1978), Proc

    Erdős, P.: Combinatorial problems in geometry and number theory. In: Relations betweencombinatoricsandotherpartsofmathematics(Proc.Sympos.PureMath., Ohio State Univ., Columbus, Ohio, 1978), Proc. Sympos. Pure Math., vol. XXXIV, pp. 149–162. Amer. Math. Soc., Providence, RI (19...

    1978

  4. [12]

    European J

    Erdős, P., Tuza, Z., Valtr, P.: Ramsey-remainder. European J. Combin.17(6), 519–532 (1996), https://doi.org/10.1006/eujc.1996.0045

    1996 doi

  5. [13]

    Felsner, S., Weil, H.: Sweeps, arrangements and signotopes. vol. 109, pp. 67– 94 (2001), https://doi.org/10.1016/S0166-218X(00)00232-8, 14th European Work- shop on Computational Geometry CG’98 (Barcelona)

    2001 doi

  6. [14]

    Gardam, G.: A counterexample to the unit conjecture for group rings. Ann. of Math. (2)194(3), 967–979 (2021), https://doi.org/10.4007/annals.2021.194.3.9

    2021 doi

  7. [15]

    In: Schölkopf, B., Platt, J.C., Hof- mann, T

    Gomes, C.P., Sabharwal, A., Selman, B.: Near-uniform sampling of combi- natorial spaces using XOR constraints. In: Schölkopf, B., Platt, J.C., Hof- mann, T. (eds.) Advances in Neural Information Processing Systems 19, Pro- ceedings of the Twentieth Annual Conference on Neural ...

    2006

  8. [16]

    Goodman, J.E., Pollack, R.: Proof of Grünbaum’s conjecture on the stretchability of certain arrangements of pseudolines. J. Combin. Theory Ser. A29(3), 385–390 (1980), https://doi.org/10.1016/0097-3165(80)90038-2

    1980 doi

  9. [17]

    Discrete Comput

    Goodman, J.E., Pollack, R.: Upper bounds for configurations and polytopes inR d. Discrete Comput. Geom.1(3), 219–227 (1986), https://doi.org/10.1007/ BF02187696

    1986

  10. [18]

    Goodman, J.E., Pollack, R., Sturmfels, B.: The intrinsic spread of a configuration inR d. J. Amer. Math. Soc.3(3), 639–651 (1990), https://doi.org/10.2307/1990931

    1990 doi

  11. [19]

    Harborth, H.: Konvexe Fünfecke in ebenen Punktmengen. Elem. Math.33(5), 116–118 (1978)

    1978

  12. [20]

    In: McIlraith, S.A., Weinberger, K.Q

    Heule, M.J.H.: Schur number five. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Pro- ceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI- 18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educat...

    2018 doi

  13. [21]

    In: Creignou, N., Berre, D.L

    Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016 - 19th Interna- tional Conference, Bordeaux, France, ...

    2016

  14. [22]

    In: Finkbeiner, B., Kovács, L

    Heule, M.J.H., Scheucher, M.: Happy ending: An empty hexagon in every set of 30 points. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Con- struction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Con...

    2024 doi

  15. [23]

    Horton, J.D.: Sets with no empty convex7-gons. Canad. Math. Bull.26(4), 482– 484 (1983), https://doi.org/10.4153/CMB-1983-077-8

    1983 doi

  16. [24]

    In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China

    Kirchweger, M., Peitl, T., Szeider, S.: Co-certificate learning with SAT modulo symmetries. In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China. pp. 1944–1953. ijcai.org (2023), ht...

    2023 doi

  17. [25]

    ACM Trans

    Kirchweger, M., Szeider, S.: SAT modulo symmetries for graph generation and enumeration. ACM Trans. Comput. Log.25(3), 1–30 (2024), https://doi.org/10. 1145/3670405

    2024

  18. [26]

    Knuth, D.E.: Axioms and hulls, Lecture Notes in Computer Science, vol. 606. Springer-Verlag, Berlin (1992), https://doi.org/10.1007/3-540-55611-7

    1992 doi

  19. [27]

    In: Sinz, C., Egly, U

    Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-...

    2014

  20. [28]

    In: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, Au- gust 3-9, 2024

    Li, Z., Bright, C., Ganesh, V.: A SAT solver + computer algebra attack on the min- imum Kochen-Specker problem. In: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, Au- gust 3-9, 2024. pp. 1898–1906. ijca...

    2024

  21. [29]

    In: Topology and geometry—Rohlin Seminar, Lecture Notes in Math., vol

    Mnëv, N.E.: The universality theorems on the classification problem of configura- tion varieties and convex polytopes varieties. In: Topology and geometry—Rohlin Seminar, Lecture Notes in Math., vol. 1346, pp. 527–543. Springer, Berlin (1988), https://doi.org/10.1007/BFb0082792

    1988 doi

  22. [30]

    In: Sakallah, K.A., Simon, L

    Nadel, A.: Generating diverse solutions in SAT. In: Sakallah, K.A., Simon, L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2011 - 14th Inter- national Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceed- ings. Lecture Notes in Computer Science...

    2011 doi

  23. [31]

    Discrete Com- put

    Overmars, M.: Finding sets of points without empty convex 6-gons. Discrete Com- put. Geom.29(1), 153–158 (2003), https://doi.org/10.1007/s00454-002-2829-x

    2003 doi

  24. [32]

    https://github.com/jreeves3/allsat-cadical (2022)

    Reeves, J.: allsat-cadical. https://github.com/jreeves3/allsat-cadical (2022)

    2022

  25. [33]

    Schaefer, M., Cardinal, J., Miltzow, T.: The existential theory of the reals as a complexity class: A compendium (2024), https://arxiv.org/abs/2407.18006

    2024 arXiv

  26. [34]

    In: Applied geometry and discrete mathematics, DIMACS Ser

    Shor, P.W.: Stretchability of pseudolines is NP-hard. In: Applied geometry and discrete mathematics, DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 4, pp. 531–554. Amer. Math. Soc., Providence, RI (1991), https://doi.org/10.1090/ dimacs/004/41

    1991

  27. [35]

    In: Sankaranarayanan, S., Sharygina, N

    Subercaseaux, B., Heule, M.J.H.: The packing chromatic number of the infinite square grid is 15. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algo- rithms for the Construction and Analysis of Systems - 29th International Confer- ence, TACAS 2023, Held as Part of th...

    2023 doi

  28. [36]

    In: de Paiva, V., Koepke, P

    Subercaseaux,B.,Mackey,E.,Qian,L.,Heule,M.:Automatedsymmetricconstruc- tions in discrete geometry. In: de Paiva, V., Koepke, P. (eds.) Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, Octo- ber 6-10, 2025, Proceedings. Lecture Note...

    2025 doi

  29. [37]

    ANZIAM J.48(2), 151–164 (2006), https://doi.org/10.1017/ S144618110000300X Toward Satisfiability Modulo Realizability 19

    Szekeres, G., Peters, L.: Computer solution to the 17-point Erdős–Szekeres problem. ANZIAM J.48(2), 151–164 (2006), https://doi.org/10.1017/ S144618110000300X Toward Satisfiability Modulo Realizability 19

    2006

  30. [38]

    Lecture Notes in Computer Science, vol

    Zheng, Z., Cherif, S., Shibasaki, R.S., Li, C.M., Zhang, J.: Exact approaches for the diversesatisfiabilityproblem.In:Casini,G.,Dundua,B.,Kutsia,T.(eds.)Logicsin Artificial Intelligence - 19th European Conference, JELIA 2025, Kutaisi, Georgia, September 1-4, 2025, Proceedings,...

    2025 doi

  31. [39]

    In: Kambhampati, S

    Zulkoski, E., Ganesh, V., Czarnecki, K.: MATHCHECK: A math assistant via a combination of computer algebra systems and SAT solvers. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, US...

    2016

Pith tools

Reviewed July 12, 2026 · model on record in the stance chip above.