Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Proceedings of the AAAI Conference on Artificial Intelligence

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)

Zhengyu Li, Curtis Bright, Vijay Ganesh

Published Mar 24, 2024• 1 citation
Publisher

Abstract

The problem of finding the minimum three-dimensional Kochen–Specker (KS) vector system, an important problem in quantum foundations, has remained open for over 55 years. We present a new method to address this problem based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS). Our approach improved the lower bound on the size of a KS system from 22 to 24. More importantly, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a proof size of 41.6 TiB for order 23. The efficiency is due to the powerful combination of SAT solvers and CAS-based orderly generation.

DOI
10.1609/aaai.v38i21.30472

Related papers

A SAT Solver + Computer Algebra Attack on the Minimum Kochen–Specker Problem

Zhengyu Li, Curtis Bright, Vijay Ganesh

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.

arXiv:2306.13319•International Joint Conference on Artificial Intelligence•Jul 26, 2024•2 citations

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

Zhengyu Li, Curtis Bright, Vijay Ganesh

Abstract One of the foundational results in quantum mechanics 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 to exist, the problem of finding the minimum KS vector system has remained stubbornly open for over 55 years, despite significant attempts by leading scientists and mathematicians. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. Our approach improves the lower bound on the minimum number of vectors in a KS system from 22 to 24, and is about 35,000 times more efficient compared to the previous best computational methods. The increase in efficiency derives from the fact we are able to exploit the powerful combinatorial search-with-learning capabilities of a SAT solver together with the isomorph-free exhaustive generation methods of a CAS. The quest for the minimum KS vector system is motivated by myriad applications such as simplifying experimental tests of contextuality, zero-error classical communication, dimension witnessing, and the security of certain quantum cryptographic protocols. To the best of our knowledge, this is the first application of a novel SAT+CAS system to a problem in the realm of quantum foundations.

•Jun 23, 2023•3 citations

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

Zhengyu Li, Curtis Bright, Vijay Ganesh

Abstract One of the most fundamental results in the foundations of quantum mechanics is the Kochen--Specker (KS) theorem, a `no-go' theorem which states that contextuality is an essential feature of any hidden-variable theory. The theorem hinges on the existence of a mathematical object called a KS vector system. Although the existence of a KS vector system was first established by Kochen and Specker, the problem of the minimum size of such a system has stubbornly remained open for over 50 years. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. We improve the lower bound on the minimum number of vectors in a KS system from 22 to 23 and improve the efficiency of the search by a factor of over 1000 when compared to the most recent computational methods. Finding a minimum KS system would simplify experimental tests of the KS theorem and have direct applications in quantum information processing, specifically in the security of quantum cryptographic protocols based on complementarity, zero-error classical communication, and dimension witnessing.

•Jun 21, 2023•2 citations

On Searching for Small Kochen-Specker Vector Systems (extended version)

Felix Arends, Joël Ouaknine, Charles W. Wampler

Kochen-Specker (KS) vector systems are sets of vectors in R^3 with the property that it is impossible to assign 0s and 1s to the vectors in such a way that no two orthogonal vectors are assigned 0 and no three mutually orthogonal vectors are assigned 1. The existence of such sets forms the basis of the Kochen-Specker and Free Will theorems. Currently, the smallest known KS vector system contains 31 vectors. In this paper, we establish a lower bound of 18 on the size of any KS vector system. This requires us to consider a mix of graph-theoretic and topological embedding problems, which we investigate both from theoretical and practical angles. We propose several algorithms to tackle these problems and report on extensive experiments. At the time of writing, a large gap remains between the best lower and upper bounds for the minimum size of KS vector systems.

arXiv:1111.3301•Nov 14, 2011•1 citation

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

Zhengyu Li, Curtis Bright, Stefan Trandafir +2 more

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ütte 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.

cs.LOCross-listedarXiv:2604.19947•Apr 23, 2026•0 citations

Maximal non-Kochen-Specker sets and a lower bound on the size of Kochen-Specker sets

Tom L Williams, Andrei Constantin

The challenge of determining bounds for the minimal number of vectors in a three-dimensional Kochen-Specker (KS) set has captivated the quantum foundations community for decades. This paper establishes a weak lower bound of 10 vectors, which does not surpass the current best-known bound of 24 vectors. By exploring the complementary concept of large non-KS sets and employing a probability argument independent of the graph structure of KS sets, we introduce a technique that could be applied in the future to derive tighter bounds. Additionally, we highlight an intriguing connection to a generalization of the moving sofa problem in navigating a right-angled hallway on the surface of a two-dimensional sphere.

arXiv:2403.05230•Physical Review A•Jan 29, 2025•1 citation
The problem of finding the minimum three-dimensional Kochen–Specker (KS) vector system, an important problem in quantum foundations, has remained open for over 55 years. We present a new method to address this problem based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS). Our approach improved the lower bound on the size of a KS system from 22 to 24. More importantly, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a proof size of 41.6 TiB for order 23. The efficiency is due to the powerful combination of SAT solvers and CAS-based orderly generation.
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.
Abstract One of the foundational results in quantum mechanics 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 to exist, the problem of finding the minimum KS vector system has remained stubbornly open for over 55 years, despite significant attempts by leading scientists and mathematicians. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. Our approach improves the lower bound on the minimum number of vectors in a KS system from 22 to 24, and is about 35,000 times more efficient compared to the previous best computational methods. The increase in efficiency derives from the fact we are able to exploit the powerful combinatorial search-with-learning capabilities of a SAT solver together with the isomorph-free exhaustive generation methods of a CAS. The quest for the minimum KS vector system is motivated by myriad applications such as simplifying experimental tests of contextuality, zero-error classical communication, dimension witnessing, and the security of certain quantum cryptographic protocols. To the best of our knowledge, this is the first application of a novel SAT+CAS system to a problem in the realm of quantum foundations.
Abstract One of the most fundamental results in the foundations of quantum mechanics is the Kochen--Specker (KS) theorem, a `no-go' theorem which states that contextuality is an essential feature of any hidden-variable theory. The theorem hinges on the existence of a mathematical object called a KS vector system. Although the existence of a KS vector system was first established by Kochen and Specker, the problem of the minimum size of such a system has stubbornly remained open for over 50 years. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. We improve the lower bound on the minimum number of vectors in a KS system from 22 to 23 and improve the efficiency of the search by a factor of over 1000 when compared to the most recent computational methods. Finding a minimum KS system would simplify experimental tests of the KS theorem and have direct applications in quantum information processing, specifically in the security of quantum cryptographic protocols based on complementarity, zero-error classical communication, and dimension witnessing.
Kochen-Specker (KS) vector systems are sets of vectors in R^3 with the property that it is impossible to assign 0s and 1s to the vectors in such a way that no two orthogonal vectors are assigned 0 and no three mutually orthogonal vectors are assigned 1. The existence of such sets forms the basis of the Kochen-Specker and Free Will theorems. Currently, the smallest known KS vector system contains 31 vectors. In this paper, we establish a lower bound of 18 on the size of any KS vector system. This requires us to consider a mix of graph-theoretic and topological embedding problems, which we investigate both from theoretical and practical angles. We propose several algorithms to tackle these problems and report on extensive experiments. At the time of writing, a large gap remains between the best lower and upper bounds for the minimum size of KS vector systems.
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ütte 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.
The challenge of determining bounds for the minimal number of vectors in a three-dimensional Kochen-Specker (KS) set has captivated the quantum foundations community for decades. This paper establishes a weak lower bound of 10 vectors, which does not surpass the current best-known bound of 24 vectors. By exploring the complementary concept of large non-KS sets and employing a probability argument independent of the graph structure of KS sets, we introduce a technique that could be applied in the future to derive tighter bounds. Additionally, we highlight an intriguing connection to a generalization of the moving sofa problem in navigating a right-angled hallway on the surface of a two-dimensional sphere.