pith. sign in

arxiv: 2604.19947 · v1 · submitted 2026-04-21 · 💻 cs.LO · math.CO· quant-ph

SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set

Zhengyu Li , Curtis Bright , Stefan Trandafir , Ad\'an Cabello , Vijay Ganesh This is my paper

Pith reviewed 2026-05-10 01:02 UTC · model grok-4.3

classification 💻 cs.LO math.COquant-ph
keywords Kochen-Specker setsstate-independent contextualitySAT solvingorderly generationcanonical labelinggraph isomorphismYu-Oh setSchütte set
0
0 comments X

The pith

The 33-ray Schütte set is the smallest three-dimensional Kochen-Specker set containing the full 25-ray state-independent contextuality set.

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

The paper develops a SAT-based framework that incorporates recursive canonical labeling with NAUTY to generate and verify small Kochen-Specker sets in three dimensions in an orderly way. It targets extensions of the Yu-Oh 13-ray set to locate the smallest KS set that includes the entire 25-ray state-independent contextuality core obtained through rigid extensions. The exhaustive enumeration up to 33 rays, completed in 1,641 CPU hours, establishes that Schütte's set is the minimal example with this property, and every non-existence result carries an independently checkable proof certificate. A sympathetic reader would care because the work settles a concrete minimality question for these quantum contextuality structures using certified computation rather than heuristic search.

Core claim

After introducing a SAT-based orderly generation method that pairs recursive canonical labeling with NAUTY to avoid the exponential scaling of prior lexicographic checks, the authors exhaustively enumerate all Kochen-Specker sets of up to 33 rays that contain the complete 25-ray state-independent contextuality set derived from the Yu-Oh configuration. The enumeration shows that the 33-ray set previously found by Schütte is the smallest such KS set in three dimensions, with all negative results for smaller cardinalities supported by formal proof certificates in an extended DRAT format.

What carries the argument

The SAT-based orderly generation framework that integrates recursive canonical labeling (RCL) with the NAUTY graph isomorphism tool to maintain consistent performance on 25-to-33-vertex instances while correctly pruning the search space.

If this is right

  • No three-dimensional KS set smaller than 33 rays contains the complete 25-ray state-independent contextuality set.
  • The enumeration of all KS sets up to 33 rays that contain this 25-ray core is complete.
  • The recursive canonical labeling approach eliminates the exponential bottleneck that made prior SAT methods intractable on these graph sizes.
  • All non-existence claims are accompanied by independently verifiable formal proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same SAT-plus-recursive-labeling method could be applied to exhaustive searches for minimal KS sets that do not fix the 25-ray core in advance.
  • The availability of DRAT certificates makes the minimality result open to direct community verification without re-running the full search.
  • The framework suggests a route to certified enumeration of contextuality witnesses in higher dimensions where manual or heuristic methods have previously been insufficient.

Load-bearing premise

The SAT encoding of Kochen-Specker set properties is both sound and complete, and the recursive canonical labeling with NAUTY accurately identifies canonical forms without omitting valid sets or producing false negatives on the 25-to-33 vertex instances.

What would settle it

Discovery of one valid three-dimensional KS set with 32 rays or fewer that contains the entire 25-ray state-independent contextuality set, or detection of an error in any of the DRAT proof certificates for non-existence.

Figures

Figures reproduced from arXiv: 2604.19947 by Ad\'an Cabello, Curtis Bright, Stefan Trandafir, Vijay Ganesh, Zhengyu Li.

Figure 1
Figure 1. Figure 1: If we connect the center of the figure with all the dots, we [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Average canonicity-check runtime on the benchmark [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
read the original abstract

We present a search for small Kochen-Specker (KS) sets in dimension 3, specifically targeting extensions of the 13-ray Yu-Oh set, which has been proven to be the minimal witness to state-independent contextuality. To enable this search, we introduce a novel SAT-based orderly generation framework integrating recursive canonical labeling (RCL) with the graph isomorphism tool NAUTY. We demonstrate that previous SAT approaches relying on lexicographical canonicity suffer from exponential scaling on canonical graphs. This limitation renders them intractable on the large instances (25 to 33 vertices) encountered in our search, whereas our RCL check maintains consistent millisecond-level performance, effectively eliminating the bottleneck. Overcoming this bottleneck allows us to perform the first exhaustive enumeration of all KS sets with up to 33 rays containing the complete 25-ray state-independent contextuality (SI-C) set obtained by rigid extensions of the Yu-Oh set in 1,641 CPU hours. We found and verified that the 33-ray set discovered by Sch\"utte is the smallest three-dimensional KS set containing the complete 25-ray SI-C set. All non-existence results are backed by independently verifiable proof certificates via an extension of the DRAT proof format.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper introduces a SAT-based orderly generation framework that integrates recursive canonical labeling (RCL) with the NAUTY graph isomorphism tool to search for small three-dimensional Kochen-Specker (KS) sets. It targets exhaustive enumeration of KS sets with 26–33 rays that contain the complete 25-ray state-independent contextuality (SI-C) set obtained via rigid extensions of the 13-ray Yu-Oh set. The authors demonstrate that prior lexicographic canonicity approaches scale exponentially on these instances while RCL remains efficient, enabling a 1,641 CPU-hour search. They conclude that the 33-ray Schütte set is the smallest such KS set and supply DRAT proof certificates for all non-existence results between 26 and 32 rays.

Significance. If the results hold, the work supplies the first exhaustive, machine-verifiable demonstration that no KS set smaller than 33 rays contains the full 25-ray SI-C set, tightening the known bounds on minimal state-independent contextuality witnesses in dimension 3. The provision of independently checkable DRAT certificates and the performance improvement of RCL over lexicographic ordering are concrete strengths that support reproducibility and allow external validation of the non-existence claims.

major comments (1)
  1. The soundness of the central non-existence claims (26–32 rays) rests on the SAT encoding of the KS coloring constraints (no 0-1 assignment summing to 1 on every context) together with the RCL+NAUTY pruning being both complete and sound. While DRAT certificates are supplied, the manuscript should include an explicit clause-level description or pseudocode of the encoding (likely in the section introducing the SAT formulation) so that the certificates can be interpreted without reverse-engineering the generator.
minor comments (1)
  1. The performance advantage of RCL is stated qualitatively (“millisecond-level”); a small table or plot comparing wall-clock times of RCL versus lexicographic canonicity on the 25–33 vertex instances would make the scaling claim easier to assess.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation and the helpful suggestion to improve the clarity of our SAT encoding. We address the single major comment below.

read point-by-point responses

  1. Referee: The soundness of the central non-existence claims (26–32 rays) rests on the SAT encoding of the KS coloring constraints (no 0-1 assignment summing to 1 on every context) together with the RCL+NAUTY pruning being both complete and sound. While DRAT certificates are supplied, the manuscript should include an explicit clause-level description or pseudocode of the encoding (likely in the section introducing the SAT formulation) so that the certificates can be interpreted without reverse-engineering the generator.

    Authors: We agree that an explicit clause-level description of the encoding will make the DRAT certificates more accessible. In the revised version we will insert a new subsection (immediately following the description of the KS coloring problem) that provides (i) the precise mapping from KS contexts to CNF clauses enforcing that no context receives a 0-1 assignment summing to 1, (ii) the auxiliary variables introduced for the orderly-generation constraints, and (iii) pseudocode for the clause-generation routine. This addition will allow readers to interpret the certificates directly from the manuscript without inspecting the generator source. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper derives its central claim (that the 33-ray Schütte set is the smallest 3D KS set containing the fixed 25-ray SI-C set) via exhaustive computational enumeration of extensions, using a SAT encoding of KS coloring constraints together with RCL+NAUTY orderly generation and DRAT proof certificates for all non-existence results up to 32 rays. No step reduces by construction to a fitted input, self-definition, or load-bearing self-citation; the Yu-Oh minimality and Schütte set are treated as external inputs, and the search method is justified by independent machine-checkable artifacts rather than internal renaming or ansatz smuggling. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the completeness of the KS set encoding in SAT and the correctness of the RCL+NAUTY canonicity procedure; no new free parameters or invented entities are introduced beyond standard SAT and graph-isomorphism primitives.

axioms (2)
  • domain assumption The 13-ray Yu-Oh set is the minimal witness to state-independent contextuality in dimension 3
    Abstract states it has been proven; used as the base for rigid extensions to the 25-ray SI-C set
  • standard math SAT solvers combined with canonical labeling can exhaustively enumerate KS sets without omissions when the encoding is complete
    Core assumption underlying the orderly generation framework

pith-pipeline@v0.9.0 · 5543 in / 1611 out tokens · 71073 ms · 2026-05-10T01:02:57.680843+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages · 1 internal anchor

  1. [1]

    PhD thesis, Aus- tralian National University,

    [Afzaly, 2016] Seyedeh Narjess Afzaly.Generation of graph classes with efficient isomorph rejection. PhD thesis, Aus- tralian National University,

    work page 2016

  2. [2]

    Fully nonlocal quantum correlations

    [Aolitaet al., 2012 ] Leandro Aolita, Rodrigo Gallego, Anto- nio Ac´ın, Andrea Chiuri, Giuseppe Vallone, Paolo Mataloni, and Ad´an Cabello. Fully nonlocal quantum correlations. Phys. Rev. A, 85:032107,

    work page 2012

  3. [3]

    Tri- acontagonal proofs of the Bell-Kochen-Specker theorem

    [Aravindet al., 2025 ] Padmanabhan K Aravind, Justin YJ Burton, David Richter, and Guillermo Nu˜nez Ponasso. Tri- acontagonal proofs of the Bell-Kochen-Specker theorem. Journal of Physics A: Mathematical and Theoretical,

    work page 2025

  4. [4]

    Bengtsson, K

    [Bengtssonet al., 2012 ] I. Bengtsson, K. Blanchfield, and A. Cabello. A Kochen–Specker inequality from a SIC. Phys. Lett. A, 376:374–376,

    work page 2012

  5. [5]

    Cadical 2.0

    [Biereet al., 2024 ] Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pol- litt. Cadical 2.0. InInternational Conference on Computer Aided Verification, pages 133–152. Springer,

    work page 2024

  6. [6]

    [Brightet al., 2021 ] Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, and Vijay Ganesh. A SAT-based resolution of Lam’s problem.Proceedings of the AAAI Con- ference on Artificial Intelligence, 35(5):3669–3676, May

    work page 2021

  7. [7]

    When satisfiability solving meets symbolic com- putation.Communications of the ACM, 65(7):64–72,

    [Brightet al., 2022 ] Curtis Bright, Ilias Kotsireas, and Vijay Ganesh. When satisfiability solving meets symbolic com- putation.Communications of the ACM, 65(7):64–72,

    work page 2022

  8. [8]

    Sch¨utte’s tautology and the Kochen- Specker theorem.Found

    [Bub, 1996] Jeffrey Bub. Sch¨utte’s tautology and the Kochen- Specker theorem.Found. Phys., 26:787–806,

    work page 1996

  9. [9]

    Cabello, M

    [Cabelloet al., 2016 ] A. Cabello, M. Kleinmann, and J. R. Portillo. Quantum state-independent contextuality requires 13 rays.J. Phys. A: Math. Theor., 49:38LT01,

    work page 2016

  10. [10]

    PhD thesis, Universidad Complutense de Madrid,

    [Cabello, 1996] Ad´an Cabello.Pruebas algebraicas de im- posibilidad de variables ocultas en mec ´anica cu ´antica. PhD thesis, Universidad Complutense de Madrid,

    work page 1996

  11. [11]

    Cinelli, M

    [Cinelliet al., 2005 ] C. Cinelli, M. Barbieri, R. Perris, P. Mat- aloni, and F. De Martini. All-Versus-Nothing Nonlocality Test of Quantum Mechanics by Two-Photon Hyperentan- glement.Phys. Rev. Lett., 95:240405,

    work page 2005

  12. [12]

    Crawford, Matthew L

    [Crawfordet al., 1996 ] James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry- breaking predicates for search problems. InProceedings of the Fifth International Conference on Principles of Knowl- edge Representation and Reasoning, KR’96, page 148–159, San Francisco, CA, USA,

    work page 1996

  13. [13]

    [Faradˇzev, 1978] I A Farad ˇzev

    Morgan Kaufmann Pub- lishers Inc. [Faradˇzev, 1978] I A Farad ˇzev. Constructive enumeration of combinatorial objects. InProbl `emes combinatoires et th´eorie des graphes, pages 131–135,

    work page 1978

  14. [14]

    IPASIR-UP: User propagators for CDCL

    [Fazekaset al., 2023 ] Katalin Fazekas, Aina Niemetz, Math- ias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User propagators for CDCL. In Meena Mahajan and Friedrich Slivovsky, editors,26th Interna- tional Conference on Theory and Applications of Satisfia- bility Testing (SAT 2023), volume 271 ofLeibniz Interna- tional Proceedi...

    work page 2023

  15. [15]

    [Heule, 2019] Marijn J. H. Heule. Optimal symmetry break- ing for graph problems.Mathematics in Computer Science, 13(4):533–548, May

    work page 2019

  16. [16]

    AlphaMapleSAT: An MCTS-based cube-and-conquer SAT solver for hard com- binatorial problems,

    [Jhaet al., 2024 ] Piyush Jha, Zhengyu Li, Zhengyang Lu, Curtis Bright, and Vijay Ganesh. AlphaMapleSAT: An MCTS-based cube-and-conquer SAT solver for hard com- binatorial problems,

    work page 2024

  17. [17]

    The Algebraic Landscape of Kochen-Specker Sets in Dimension Three

    [Kernaghan, 2026] Michael Kernaghan. The algebraic land- scape of Kochen-Specker sets in dimension three.arXiv preprint arXiv:2603.16988,

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  18. [18]

    SAT Modulo Symmetries for graph generation and enumeration.ACM Trans

    [Kirchweger and Szeider, 2024] Markus Kirchweger and Ste- fan Szeider. SAT Modulo Symmetries for graph generation and enumeration.ACM Trans. Comput. Log., 25(3),

    work page 2024

  19. [19]

    Co-certificate learning with SAT mod- ulo symmetries

    [Kirchwegeret al., 2023 ] Markus Kirchweger, Tom´aˇs Peitl, and Stefan Szeider. Co-certificate learning with SAT mod- ulo symmetries. In Edith Elkind, editor,Proceedings of the Thirty-Second International Joint Conference on Artifi- cial Intelligence, IJCAI-23, pages 1944–1953. International Joint Conferences on Artificial Intelligence Organization,

    work page 2023

  20. [20]

    Kochen and E

    [Kochen and Specker, 1965] S. Kochen and E. P. Specker. Logical structures arising in quantum theory. In J. W. Ad- dison, L. Henkin, and A. Tarski, editors,Symposium on the Theory of Models: Proceedings of the 1963 International Symposium at Berkeley, pages 177–189. North-Holland, Amsterdam,

    work page 1965

  21. [21]

    [Kochen and Specker, 1967] Simon Kochen and Ernst P. Specker. The Problem of Hidden Variables in Quantum Mechanics.J. Math. Mech., 17:59–87,

    work page 1967

  22. [22]

    Quantum-classical separation in bounded-resource tasks arising from measurement contextuality,

    [Kumaret al., 2025 ] Shashwat Kumar, Eliott Rosenberg, et al. Quantum-classical separation in bounded-resource tasks arising from measurement contextuality,

    work page 2025

  23. [23]

    [Liet al., 2024 ] Zhengyu Li, Curtis Bright, and Vijay Ganesh

    arXiv:2512.02284. [Liet al., 2024 ] Zhengyu Li, Curtis Bright, and Vijay Ganesh. A SAT solver + computer algebra attack on the minimum Kochen–Specker problem. In Kate Larson, editor,Pro- ceedings of the Thirty-Third International Joint Confer- ence on Artificial Intelligence, IJCAI-24, pages 1898–1906. International Joint Conferences on Artificial Intelli...

    work page arXiv 2024

  24. [24]

    Learning rate based branching heuristic for SAT solvers

    [Lianget al., 2016 ] Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. InInternational Con- ference on Theory and Applications of Satisfiability Testing, pages 123–140. Springer,

    work page 2016

  25. [25]

    McKay and Adolfo Piperno

    [McKay and Piperno, 2014] Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II.Journal of Sym- bolic Computation, 60:94–112,

    work page 2014

  26. [26]

    Nauty user’s guide (ver- sion 2.4).Computer Science Dept., Australian National University, pages 225–239,

    [McKay, 2007] Brendan D McKay. Nauty user’s guide (ver- sion 2.4).Computer Science Dept., Australian National University, pages 225–239,

    work page 2007

  27. [27]

    Fast generation of reg- ular graphs and construction of cages.Journal of Graph Theory, 30(2):137–146,

    [Meringer, 1999] Markus Meringer. Fast generation of reg- ular graphs and construction of cages.Journal of Graph Theory, 30(2):137–146,

    work page 1999

  28. [28]

    CDCLSym: Introducing effective symmetry breaking in SAT solving

    [Metinet al., 2018 ] Hakan Metin, Souheib Baarir, Maximi- lien Colange, and Fabrice Kordon. CDCLSym: Introducing effective symmetry breaking in SAT solving. InTools and Algorithms for the Construction and Analysis of Systems, pages 99–114, New York,

    work page 2018

  29. [29]

    [Peres, 1993] Asher Peres.Quantum Theory: Concepts and Methods

    Springer International Pub- lishing. [Peres, 1993] Asher Peres.Quantum Theory: Concepts and Methods. Kluwer, Dordrecht,

    work page 1993

  30. [30]

    Every one a winner or how to avoid isomorphism search when cataloguing combinatorial configurations.Annals of Discrete Mathematics, 2:107– 120,

    [Read, 1978] Ronald C Read. Every one a winner or how to avoid isomorphism search when cataloguing combinatorial configurations.Annals of Discrete Mathematics, 2:107– 120,

    work page 1978

  31. [31]

    Structural symmetry breaking

    [Sellmann and Hentenryck, 2005] Meinolf Sellmann and Pascal Van Hentenryck. Structural symmetry breaking. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, IJCAI-05, pages 298–303, California,

    work page 2005

  32. [32]

    Two fundamental solutions to the rigid Kochen- Specker set problem and the solution to the minimal Kochen-Specker set problem under one assumption.Phys

    [Trandafir and Cabello, 2025] Stefan Trandafir and Ad´an Ca- bello. Two fundamental solutions to the rigid Kochen- Specker set problem and the solution to the minimal Kochen-Specker set problem under one assumption.Phys. Rev. A, 111:052204, May

    work page 2025

  33. [33]

    Experimental Demonstration of Quantum Pseudotelepathy.Phys

    [Xuet al., 2022 ] Jia-Min Xu, Yi-Zheng Zhen, Yu-Xiang Yang, Zi-Mo Cheng, Zhi-Cheng Ren, Kai Chen, Xi-Lin Wang, and Hui-Tian Wang. Experimental Demonstration of Quantum Pseudotelepathy.Phys. Rev. Lett., 129:050402, Jul

    work page 2022

  34. [34]

    Certifying sets of quantum observables with any full-rank state.Phys

    [Xuet al., 2024 ] Zhen-Peng Xu, Debashis Saha, Kishor Bharti, and Ad ´an Cabello. Certifying sets of quantum observables with any full-rank state.Phys. Rev. Lett., 132:140201, Apr

    work page 2024

  35. [35]

    All-Versus-Nothing Violation of Local Realism by Two-Photon, Four-Dimensional Entanglement.Phys

    [Yanget al., 2005 ] Tao Yang, Qiang Zhang, Jun Zhang, Juan Yin, Zhi Zhao, Marek ˙Zukowski, Zeng-Bing Chen, and Jian- Wei Pan. All-Versus-Nothing Violation of Local Realism by Two-Photon, Four-Dimensional Entanglement.Phys. Rev. Lett., 95:240406,

    work page 2005

  36. [36]

    [Yu and Oh, 2012] Sixia Yu and C. H. Oh. State-independent proof of Kochen-Specker theorem with 13 rays.Phys. Rev. Lett., 108:030402, 2012

    work page 2012