Research map / Learning theory and algorithms / Combinatorial and search optimization
A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Combines a SAT solver (MapleSAT) with a computer algebra system doing canonicity checking (orderly generation) to search for minimum three-dimensional Kochen-Specker systems, raising the lower bound from 22 to 24 with DRAT-based proof certificates.
Problem
Finding the minimum-size three-dimensional Kochen-Specker vector system, an open problem for over 55 years in quantum foundations.
Approach
Integrates a SAT solver with a CAS-based canonicity checker in an orderly isomorph-free generation loop, adding CAS-derived blocking clauses for noncanonical partial matrices, and certifies the nonexistence results with extended DRAT proofs.
Key results
- Improved the lower bound on the minimum three-dimensional Kochen-Specker system size from 22 to 24 (order 23 solved via cube-and-conquer on up to 5000 CPUs, ~52,619 CPU hours).
- Order 21 search estimated about 35,000 times faster than Uijlen and Westerbaan (2016).
- Produced computer-verifiable DRAT proof certificates of 1.9 and 41.6 TiB for orders 22 and 23.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Combine SAT solving with CAS orderly generation | Minimum KS problem · Order 17 | Speedup over SAT-only: 8.4× | Helped |
| Combine SAT solving with CAS orderly generation | Minimum KS problem · Order 18 | Speedup over SAT-only: 123.8× | Helped |
| Combine SAT solving with CAS orderly generation | Minimum KS problem · Order 19 | Speedup over SAT-only: 883.5× | Helped |
| Combine SAT solving with CAS orderly generation | Minimum KS problem · Order 17 | Speedup over CAS-only: 24.2× | Helped |
| Combine SAT solving with CAS orderly generation | Minimum KS problem · Order 18 | Speedup over CAS-only: 211.5× | Helped |
| Combine SAT solving with CAS orderly generation | Minimum KS problem · Order 19 | Speedup over CAS-only: 717.6× | Helped |
| Use SAT+CAS search rather than prior lower-bound methods | Minimum three-dimensional KS system · Minimum KS system size | Lower bound: 22 to 24 | Helped |
Limitations
- Order 23 required a cluster of up to 5000 CPUs and proofs are very large (41.6 TiB).
- Upper bound on minimum KS system size remains open (only lower bound improved).
Experimental setup
Benchmarks: Kochen-Specker minimum system orders 17-23
Metrics: CPU time (hours) speedup over SAT-only and CAS-only proof size (TiB)
Baselines: SAT-only solving CAS-only (nauty) generation Uijlen and Westerbaan (2016) Kirchweger, Peitl, Szeider (2023) SAT modulo symmetries
Builds on: orderly generation DRAT proof format MapleSAT nauty
Closest papers by meaning
- A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract) (AAAI 2024 · similarity 0.85)
- Rethinking Parity Check Enhanced Symmetry-Preserving Ansatz (NeurIPS 2024 · similarity 0.83)
- A Sub-Problem Quantum Alternating Operator Ansatz for Correlation Clustering (ICML 2025 · similarity 0.81)
- SAT-Based Techniques for Lexicographically Smallest Finite Models (AAAI 2024 · similarity 0.81)
- Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization (AAAI 2025 · similarity 0.81)
- Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.80)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.