Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem

Zhengyu Li, Curtis Bright, Vijay Ganesh

TL;DR

This work tackles the minimum KS problem in three dimensions by developing a verifiable proof-producing pipeline that combines SAT solving with computer algebra (SAT+CAS) and orderly generation (OG). The authors introduce Math-Check, a system that encodes KS graph properties, prunes using isomorph-free generation, and checks embeddability with Z3, while producing fully verifiable proof certificates (DRAT). They establish a rigorous lower bound of $24$ vectors for 3D KS systems, including complex vectors, and demonstrate substantial speedups over prior SAT-only, CAS-only, and some SMS-based approaches, even achieving competitive parallel performance for the hardest cases. All results are verified, and the codebase is open-source, illustrating the viability of the SAT+CAS paradigm for deep quantum-foundation questions and related combinatorial problems.

Abstract

One of the fundamental results in quantum foundations is the Kochen-Specker (KS) theorem, which states that any theory whose predictions agree with quantum mechanics must be contextual, i.e., a quantum observation cannot be understood as revealing a pre-existing value. The theorem hinges on the existence of a mathematical object called a KS vector system. While many KS vector systems are known, the problem of finding the minimum KS vector system in three dimensions (3D) has remained stubbornly open for over 55 years. To address the minimum KS problem, we present a new verifiable proof-producing method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) that uses an isomorph-free orderly generation technique that is very effective in pruning away large parts of the search space. Our method shows that a KS system in 3D must contain at least 24 vectors. We show that our sequential and parallel Cube-and-Conquer (CnC) SAT+CAS methods are significantly faster than SAT-only, CAS-only, and a prior CAS-based method of Uijlen and Westerbaan. Further, while our parallel pipeline is somewhat slower than the parallel CnC version of the recently introduced Satisfiability Modulo Theories (SMS) method, this is in part due to the overhead of proof generation. Finally, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 40.3 TiB in order 23.

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem

TL;DR

This work tackles the minimum KS problem in three dimensions by developing a verifiable proof-producing pipeline that combines SAT solving with computer algebra (SAT+CAS) and orderly generation (OG). The authors introduce Math-Check, a system that encodes KS graph properties, prunes using isomorph-free generation, and checks embeddability with Z3, while producing fully verifiable proof certificates (DRAT). They establish a rigorous lower bound of vectors for 3D KS systems, including complex vectors, and demonstrate substantial speedups over prior SAT-only, CAS-only, and some SMS-based approaches, even achieving competitive parallel performance for the hardest cases. All results are verified, and the codebase is open-source, illustrating the viability of the SAT+CAS paradigm for deep quantum-foundation questions and related combinatorial problems.

Abstract

One of the fundamental results in quantum foundations is the Kochen-Specker (KS) theorem, which states that any theory whose predictions agree with quantum mechanics must be contextual, i.e., a quantum observation cannot be understood as revealing a pre-existing value. The theorem hinges on the existence of a mathematical object called a KS vector system. While many KS vector systems are known, the problem of finding the minimum KS vector system in three dimensions (3D) has remained stubbornly open for over 55 years. To address the minimum KS problem, we present a new verifiable proof-producing method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) that uses an isomorph-free orderly generation technique that is very effective in pruning away large parts of the search space. Our method shows that a KS system in 3D must contain at least 24 vectors. We show that our sequential and parallel Cube-and-Conquer (CnC) SAT+CAS methods are significantly faster than SAT-only, CAS-only, and a prior CAS-based method of Uijlen and Westerbaan. Further, while our parallel pipeline is somewhat slower than the parallel CnC version of the recently introduced Satisfiability Modulo Theories (SMS) method, this is in part due to the overhead of proof generation. Finally, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 40.3 TiB in order 23.
Paper Structure (24 sections, 1 equation, 5 figures, 5 tables)

This paper contains 24 sections, 1 equation, 5 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Two definitions of the Kochen-Specker System
  3. The SAT+CAS Paradigm for Hard Combinatorial Problems
  4. Automated Verification of Results
  5. Our Contributions
  6. Background
  7. The KS Theorem
  8. The Minimum KS Problem
  9. Cube-and-conquer
  10. Previous Work
  11. SAT Encoding of the Minimum KS Problem
  12. Encoding the Squarefree Constraint
  13. Encoding the Minimum Degree Constraint
  14. Encoding the Triangle Constraint
  15. Encoding the Noncolorability Constraint
  16. ...and 9 more sections

Figures (5)

  • Figure 1: A flowchart of our SAT+CAS based tool Math-Check for solving the KS problem in the sequential setting. The CNF instance encoding the KS problem (see Section \ref{['sec:encoding']}) is simplified using CaDiCaL+CAS. The simplified instance is passed to the MapleSAT+CAS tool (see Section \ref{['orderly']}) either sequentially or in parallel using Cube-and-Conquer (CnC). Finally, an embeddability checker applies the SMT solver Z3 to determine whether the candidates are embeddable (see Section \ref{['sec:embeddability']}).
  • Figure 2: The 31 vectors of the smallest known KS system in three dimensions (discovered by John Conway and Simon Kochen circa 1990). For simplicity, the vectors have been scaled to lie on the cube with vertices $(\pm2,\pm2,\pm2)$ instead of the unit sphere.
  • Figure 3: The only two minimal nonembeddable graphs of order 10. These are the smallest squarefree graphs that are not embeddable.
  • Figure 4: The only two KS candidates up to order 23 that do not contain minimal nonembeddable graphs up to and including order 14. These two graphs are determined to be unembeddable by Z3.
  • Figure 5: One of the four graphs with 20 vertices that were not present in Uijlen and Westerbaan's enumeration. The four graphs satisfy all constraints mentioned in Section \ref{['sec:encoding']}, but are not embeddable, and therefore do not constitute a KS system.

Theorems & Definitions (10)

  • Definition 1: Vector System
  • Definition 2: 010-Colorability of Vector Systems
  • Definition 3: KS Vector System
  • Definition 4: Orthogonality Graph
  • Definition 5: 010-colorability of Graphs
  • Definition 6: Embeddable Graph
  • Definition 7: KS Graph
  • Definition 8: KS Candidates
  • Definition 9: Canonical Graph
  • Definition 10: Minimal Unembeddable Graph