A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)
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.
Cite
Text
Li et al. "A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)." AAAI Conference on Artificial Intelligence, 2024. doi:10.1609/AAAI.V38I21.30472Markdown
[Li et al. "A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)." AAAI Conference on Artificial Intelligence, 2024.](https://mlanthology.org/aaai/2024/li2024aaai-sat/) doi:10.1609/AAAI.V38I21.30472BibTeX
@inproceedings{li2024aaai-sat,
title = {{A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)}},
author = {Li, Zhengyu and Bright, Curtis and Ganesh, Vijay},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2024},
pages = {23559-23560},
doi = {10.1609/AAAI.V38I21.30472},
url = {https://mlanthology.org/aaai/2024/li2024aaai-sat/}
}