DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.37

Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras

Authors: Anuj Dawar and Nihil Shah

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.LICS.2026.37,
  author =	{Dawar, Anuj and Shah, Nihil},
  title =	{{Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{37:1--37:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.37},
  URN =		{urn:nbn:de:0030-drops-268247},
  doi =		{10.4230/LIPIcs.LICS.2026.37},
  annote =	{Keywords: partial Boolean algebra, quantum logic, existential theory of the reals}
}

Document

DOI: 10.4230/LIPIcs.CSL.2018.2

Relating Structure and Power: Comonadic Semantics for Computational Resources

Authors: Samson Abramsky and Nihil Shah

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract

Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraïssé games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraïssé comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.

Cite as

Samson Abramsky and Nihil Shah. Relating Structure and Power: Comonadic Semantics for Computational Resources. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.CSL.2018.2,
  author =	{Abramsky, Samson and Shah, Nihil},
  title =	{{Relating Structure and Power: Comonadic Semantics for Computational Resources}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.2},
  URN =		{urn:nbn:de:0030-drops-96698},
  doi =		{10.4230/LIPIcs.CSL.2018.2},
  annote =	{Keywords: Finite model theory, combinatorial games, Ehrenfeucht-Fra\"{i}ss\'{e} games, pebble games, bisimulation, comonads, coKleisli category, coalgebras of a comonad}
}

Search Results

Documents authored by Shah, Nihil

Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras

Abstract

Cite as

Relating Structure and Power: Comonadic Semantics for Computational Resources

Abstract

Cite as

Thanks for your feedback!

Could not send message