A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student 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.

Authors

• Zhengyu Li Georgia Institute of Technology
• Curtis Bright University of Windsor
• Vijay Ganesh Georgia Institute of Technology

Keywords

• Automated Reasoning
• Constraint Satisfaction
• Logic
• Scientific Discovery
• Search