AAAI 2024technical25 citations
A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)
Zhengyu Li, Curtis Bright, Vijay Ganesh
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.
BibTeX
@article{Li_Bright_Ganesh_2024, title={A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)}, volume={38}, url={https://ojs.aaai.org/index.php/AAAI/article/view/30472}, DOI={10.1609/aaai.v38i21.30472}, abstractNote={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.}, number={21}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Li, Zhengyu and Bright, Curtis and Ganesh, Vijay}, year={2024}, month={Mar.}, pages={23559-23560} }