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

TL;DR

This paper introduces a novel SAT solver and computer algebra system approach to determine the minimum size of Kochen-Specker vector systems in 3D, establishing a lower bound of 24 vectors with verifiable proof certificates.

Contribution

It presents a new combined SAT and CAS method that significantly improves efficiency in solving the minimum KS problem and provides the first verifiable proof certificate for the lower bound.

Findings

Minimum KS vector system in 3D has at least 24 vectors.

The proposed SAT+CAS method outperforms previous approaches in speed.

A 40.3 TiB proof certificate verifies the lower bound.

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.