Document Open Access Logo

Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras

Authors Anuj Dawar , Nihil Shah

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.37.pdf
  • Filesize: 0.9 MB
  • 25 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantum information theory
  • Theory of computation → Logic
Keywords
  • partial Boolean algebra
  • quantum logic
  • existential theory of the reals

Metrics

Abstract

The Kochen-Specker no-go theorem established that hidden-variable theories in quantum mechanics necessarily admit contextuality. This theorem is formally stated in terms of the partial Boolean algebra structure of projectors on a Hilbert space. Each partial Boolean algebra provides a semantics for interpreting propositional logic. In this paper, we examine the complexity of propositional satisfiability for various classes of partial Boolean algebras. We first show that the satisfiability problem for the class of non-trivial partial Boolean algebras is NP-complete. Next, we consider the satisfiability problem for the class of partial Boolean algebras arising from projectors on finite dimensional Hilbert spaces. For real Hilbert spaces of dimension greater 2 and any complex Hilbert spaces of dimension greater than 3, we demonstrate that the satisfiability problem is complete for the existential theory of the reals. Interestingly, the proofs of these results make use of Kochen-Specker sets as gadgets. As a corollary, we conclude that deciding quantum homomorphism in these fixed dimensions are also complete for the existential theory of the reals. Finally, we show that the satisfiability problems for the class of all Hilbert spaces and all finite-dimensional Hilbert spaces is undecidable.

Cite As Get BibTex

Anuj Dawar and Nihil Shah. Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 37:1-37:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.37

Author Details

Anuj Dawar
  • Department of Computer Science and Technology, University of Cambridge, UK
Nihil Shah
  • Department of Computer Science and Technology, University of Cambridge, UK

Funding

Research supported by UK Research and Innovation (UKRI) under the UK government’s Horizon Europe funding guarantee: grant number EP/X028259/1.

References

  1. Samson Abramsky and Rui Soares Barbosa. The Logic of Contextuality. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.5.
  2. Samson Abramsky, Rui Soares Barbosa, Nadish de Silva, and Octavio Zapata. The Quantum Monad on Relational Structures. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), volume 83 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.35.
  3. Albert Atserias, Phokion G. Kolaitis, and Simone Severini. Generalized satisfiability problems via operator assignments. Journal of Computer and System Sciences, 105:171-198, 2019. URL: https://doi.org/10.1016/j.jcss.2019.05.003.
  4. Albert Atserias, Laura Mančinska, David E. Roberson, Robert Šámal, Simone Severini, and Antonios Varvitsiotis. Quantum and non-signalling graph isomorphisms. Journal of Combinatorial Theory, Series B, 136:289-328, 2019. URL: https://doi.org/10.1016/j.jctb.2018.11.002.
  5. Lenore Blum, Mike Shub, and Steve Smale. On a theory of computation and complexity over the real numbers: Np-completeness, recursive functions and universal machines. Bulletin of the American Mathematical Society, 21(1):1-46, 1989. Google Scholar
  6. John Canny. Some algebraic and geometric computations in pspace. In Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, STOC '88, pages 460-467, New York, NY, USA, 1988. Association for Computing Machinery. URL: https://doi.org/10.1145/62212.62257.
  7. John Conway and Simon Kochen. The Geometry of the Quantum Paradoxes, pages 257-269. Springer Berlin Heidelberg, Berlin, Heidelberg, 2002. URL: https://doi.org/10.1007/978-3-662-05032-3_18.
  8. Anuj Dawar and Nihil Shah. Complexity of satisfiability in kochen-specker partial boolean algebras. arXiv preprint arXiv:2602.24164, 2026. URL: https://doi.org/10.48550/arXiv.2602.24164.
  9. Tobias Fritz. Quantum logic is undecidable. Archive for Mathematical Logic, 60(3):329-341, May 2021. URL: https://doi.org/10.1007/S00153-020-00749-0.
  10. John Harding and Chris Heunen. Topos quantum theory with short posets. Order, 38(1):111-125, 2020. URL: https://doi.org/10.1007/s11083-020-09531-6.
  11. Christian Herrmann, Johanna Sokoli, and Martin Ziegler. Satisfiability of cross product terms is complete for real nondeterministic polytime blum-shub-smale machines. In Turlough Neary and Matthew Cook, editors, Proceedings Machines, Computations and Universality 2013, MCU 2013, Zürich, Switzerland, September 9-11, 2013, volume 128 of EPTCS, pages 85-92, 2013. URL: https://doi.org/10.4204/EPTCS.128.16.
  12. Christian Herrmann and Martin Ziegler. Computational complexity of quantum satisfiability. J. ACM, 63(2), May 2016. URL: https://doi.org/10.1145/2869073.
  13. Chris Heunen. Piecewise boolean algebras and their domains. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming, pages 208-219, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-43951-7_18.
  14. Amin Karamlou. Quantum Relaxations of CSP and Structure Isomorphism. In Paweł Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak, editors, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025), volume 345 of Leibniz International Proceedings in Informatics (LIPIcs), pages 61:1-61:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2025.61.
  15. Simon Kochen. A reconstruction of quantum mechanics. Foundations of Physics, 45(5):557-590, May 2015. URL: https://doi.org/10.1007/s10701-015-9886-5.
  16. Simon Kochen and Ernst Specker. Logical structures arising in quantum theory. the theory of models. In 1963 Symposium at Berkeley, pages 177-189, 1963. Google Scholar
  17. Simon Kochen and Ernst Specker. The problem of hidden variables in quantum mechanics. Journal of Mathematics and Mechanics, 17(1):59-87, 1967. Google Scholar
  18. Laura Mančinska and David E. Roberson. Quantum homomorphisms. Journal of Combinatorial Theory, Series B, 118:228-267, 2016. URL: https://doi.org/10.1016/j.jctb.2015.12.009.
  19. A Peres. Two simple proofs of the kochen-specker theorem. Journal of Physics A: Mathematical and General, 24(4):L175, February 1991. Google Scholar
  20. R. Piziak, P.L. Odell, and R. Hahn. Constructing projections on sums and intersections. Computers and Mathematics with Applications, 37(1):67-74, 1999. URL: https://doi.org/10.1016/S0898-1221(98)00242-9.
  21. Ravishankar Ramanathan, Monika Rosicka, Karol Horodecki, Stefano Pironio, Michał Horodecki, and Paweł Horodecki. Gadget structures in proofs of the kochen-specker theorem. Quantum, 4:308, 2020. URL: https://doi.org/10.22331/Q-2020-08-14-308.
  22. Marcus Schaefer, Jean Cardinal, and Tillmann Miltzow. The existential theory of the reals as a complexity class: A compendium, 2024. URL: https://doi.org/10.48550/arXiv.2407.18006.
  23. Grigori S Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967-1970, pages 466-483, 1983. Google Scholar
  24. C.J. van Alten. Partial algebras and complexity of satisfiability and universal theory for distributive lattices, boolean algebras and heyting algebras. Theoretical Computer Science, 501:82-92, 2013. URL: https://doi.org/10.1016/j.tcs.2013.05.012.
  25. Benno van den Berg and Chris Heunen. Noncommutativity as a colimit. Applied Categorical Structures, 20(4):393-414, August 2012. URL: https://doi.org/10.1007/s10485-011-9246-3.
  26. Xingyao Wu, Jean-Daniel Bancal, Matthew McKague, and Valerio Scarani. Device-independent parallel self-testing of two singlets. Phys. Rev. A, 93:062121, June 2016. URL: https://doi.org/10.1103/PhysRevA.93.062121.
  27. Zhen-Peng Xu, Debashis Saha, Kishor Bharti, and Adán Cabello. Certifying sets of quantum observables with any full-rank state. Phys. Rev. Lett., 132:140201, April 2024. URL: https://doi.org/10.1103/PhysRevLett.132.140201.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact