Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

ACM/IEEE Symposium on Logic in Computer Science (LICS)

Computational Complexity of Quantum Satisfiability

Christian Herrmann, Martin Ziegler

Published Jun 1, 2011• 2 citations
Publisher

Abstract

Quantum logic generalizes, and in dimension one coincides with, Boolean propositional logic. We introduce the weak and strong satisfiability problem for quantum logic formulas, and show both NP-complete in dimension two as well. For higher-dimensional spaces Rdand Cdwith d≥3 fixed, on the other hand, we show the problem to be complete for the nondeterministic Blum-Shub-Smale model of real computation. This provides a unified view on both Turing and real BSS complexity theory, and adds (a perhaps more natural and combinatorially flavoured) one to the still sparse list of NPR-complete problems, mostly pertaining to real algebraic geometry. Our proofs rely on (a careful examination of) works by John von Neumannas well as contributions by Hagge et. al (2005,2007,2009). We finally investigate the problem over Indefinite finite dimensions and relate it to NON-commutative semi algebraic geometry.

DOI
10.1109/lics.2011.8

Related papers

Computational Complexity of Quantum Satisfiability

Christian Herrmann, Martin Ziegler

We connect both discrete and algebraic complexity theory with the satisfiability problem in certain non-Boolean lattices. Specifically, quantum logic was introduced in 1936 by Garrett Birkhoff and John von Neumann as a framework for capturing the logical peculiarities of quantum observables: in the 1D case it coincides with Boolean propositional logic but, starting with dimension two, violates the distributive law. We introduce the weak and strong satisfiability problem for quantum logic propositional formulae. It turns out that in dimension two, both are also NP --complete. For higher-dimensional spaces ℝ d and ℂ d with d ≥ 3 fixed, on the other hand, we show both problems to be complete for the nondeterministic Blum-Shub-Smale (BSS) model of real computation. This provides a unified view on both Turing and real BSS complexity theory, and extends the (still relatively scarce) list of problems established NP ℝ --complete with one, perhaps, closest in spirit to the classical Cook-Levin Theorem. More precisely, strong satisfiability of ∧ ∨ ∧ --terms is complete, while that of ∧ ∨--terms (i.e., those in conjunctive form) can be decided in polynomial time in dimensions d ≥ 2. The decidability of the infinite-dimensional case being still open, we proceed to investigate the case of indefinite finite dimensions. Here, weak satisfiability still belongs to NP R and strong satisfiability is still hard; the latter, in fact, turns out as polynomial-time equivalent to the feasibility of noncommutative integer polynomial equations over matrix rings.

Journal of the ACM•May 4, 2016•14 citations

Computational Complexity of Quantum Satisfiability

Christian Herrmann, Martin Ziegler

Quantum logic was introduced in 1936 by Garrett Birkhoff and John von Neumann as a framework for capturing the logical peculiarities of quantum observables. It generalizes, and on 1-dimensional Hilbert space coincides with, Boolean propositional logic. We introduce the weak and strong satisfiability problem for quantum logic terms. It turns out that in dimension two both are also NP-complete. For higher-dimensional spaces R^d and C^d with d>2 fixed, on the other hand, we show both problems to be complete for the nondeterministic Blum-Shub-Smale model of real computation. This provides a unified view on both Turing and real BSS complexity theory; and extends the still relatively scarce family of NP_R-complete problems with one perhaps closest in spirit to the classical Cook-Levin Theorem. Our investigations on the dimensions a term is weakly/strongly satisfiable in lead to satisfiability problems in indefinite finite and finally in infinite dimension. Here, strong satisfiability turns out as polynomial-time equivalent to the feasibility of noncommutative integer polynomial equations

arXiv:1004.1696•Apr 10, 2010•0 citations

Complexity of Quantum Logic Satisfiability in Fixed Dimension: Realification and Rank-One Encodings

Higuchi, Joaquim Reizi

Quantum propositional logic, introduced by Birkhoff and von Neumann, formalizes reasoning about experimental propositions in quantum mechanics through closed subspaces of Hilbert spaces. We provide a comprehensive complexity analysis of the satisfiability problem for quantum logic formulas over the connectives conjunction, disjunction, and negation. Distinguishing between weak satisfiability (evaluation to a nonzero subspace) and strong satisfiability (evaluation to the full space), we establish that both notions coincide with Boolean satisfiability for dimension one, are classically NP complete for dimension two, and become complete for the Blum Shub Smale class NP_R when dimension d >= 3 is fixed. Our principal contribution is twofold. First, we present two alternative constructive reductions from quantum logic satisfiability to the Existential Theory of the Reals (ETR): a realification based encoding that explicitly handles the complex to real translation through commutant characterizations, and a rank one column encoding with orthogonal splitting gadgets. Both reductions yield polynomial size systems of quadratic equations for fixed dimension, proving membership in the complexity class existsR and hence in PSPACE via Cannys algorithm. Second, we provide detailed size bounds distinguishing weak and strong satisfiability: weak satisfiability encodes with O(n D^2 + N_v D) scalar variables where n is the number of atoms, D the real dimension, and N_v the number of disjunctions, while strong satisfiability requires O(n D^2 + N_v D^2) variables due to basis vector witnesses. When dimension is part of the input, strong satisfiability becomes polynomial time equivalent to feasibility of noncommutative integer polynomial equations. These results position quantum logic satisfiability precisely between classical NP and existsR, highlighting dimension as a fundamental complexity parameter.

•Nov 17, 2025•0 citations

Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras

Anuj Dawar, Nihil Shah

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 satisfiablity 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 satisfiablity 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.

quant-pharXiv:2602.24164•Mar 2, 2026•0 citations

Classical and Quantum Algorithms for the Boolean Satisfiability Problem

Carlos Barrón-Romero

This paper presents a complete algorithmic study of the decision Boolean Satisfiability Problem under the classical computation and quantum computation theories. The paper depicts deterministic and probabilistic algorithms, propositions of their properties and the main result is that the problem has not an efficient algorithm (NP is not P). Novel quantum algorithms and propositions depict that the complexity by quantum computation approach for solving the Boolean Satisfiability Problem or any NP problem is lineal time.

arXiv:1510.02682•Oct 6, 2015•3 citations

Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras

Anuj Dawar, Nihil Shah

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.

Leibniz international proceedings in informatics•Jan 1, 2026•0 citations
Quantum logic generalizes, and in dimension one coincides with, Boolean propositional logic. We introduce the weak and strong satisfiability problem for quantum logic formulas, and show both NP-complete in dimension two as well. For higher-dimensional spaces Rdand Cdwith d≥3 fixed, on the other hand, we show the problem to be complete for the nondeterministic Blum-Shub-Smale model of real computation. This provides a unified view on both Turing and real BSS complexity theory, and adds (a perhaps more natural and combinatorially flavoured) one to the still sparse list of NPR-complete problems, mostly pertaining to real algebraic geometry. Our proofs rely on (a careful examination of) works by John von Neumannas well as contributions by Hagge et. al (2005,2007,2009). We finally investigate the problem over Indefinite finite dimensions and relate it to NON-commutative semi algebraic geometry.
We connect both discrete and algebraic complexity theory with the satisfiability problem in certain non-Boolean lattices. Specifically, quantum logic was introduced in 1936 by Garrett Birkhoff and John von Neumann as a framework for capturing the logical peculiarities of quantum observables: in the 1D case it coincides with Boolean propositional logic but, starting with dimension two, violates the distributive law. We introduce the weak and strong satisfiability problem for quantum logic propositional formulae. It turns out that in dimension two, both are also NP --complete. For higher-dimensional spaces ℝ d and ℂ d with d ≥ 3 fixed, on the other hand, we show both problems to be complete for the nondeterministic Blum-Shub-Smale (BSS) model of real computation. This provides a unified view on both Turing and real BSS complexity theory, and extends the (still relatively scarce) list of problems established NP ℝ --complete with one, perhaps, closest in spirit to the classical Cook-Levin Theorem. More precisely, strong satisfiability of ∧ ∨ ∧ --terms is complete, while that of ∧ ∨--terms (i.e., those in conjunctive form) can be decided in polynomial time in dimensions d ≥ 2. The decidability of the infinite-dimensional case being still open, we proceed to investigate the case of indefinite finite dimensions. Here, weak satisfiability still belongs to NP R and strong satisfiability is still hard; the latter, in fact, turns out as polynomial-time equivalent to the feasibility of noncommutative integer polynomial equations over matrix rings.
Quantum logic was introduced in 1936 by Garrett Birkhoff and John von Neumann as a framework for capturing the logical peculiarities of quantum observables. It generalizes, and on 1-dimensional Hilbert space coincides with, Boolean propositional logic. We introduce the weak and strong satisfiability problem for quantum logic terms. It turns out that in dimension two both are also NP-complete. For higher-dimensional spaces R^d and C^d with d>2 fixed, on the other hand, we show both problems to be complete for the nondeterministic Blum-Shub-Smale model of real computation. This provides a unified view on both Turing and real BSS complexity theory; and extends the still relatively scarce family of NP_R-complete problems with one perhaps closest in spirit to the classical Cook-Levin Theorem. Our investigations on the dimensions a term is weakly/strongly satisfiable in lead to satisfiability problems in indefinite finite and finally in infinite dimension. Here, strong satisfiability turns out as polynomial-time equivalent to the feasibility of noncommutative integer polynomial equations
Quantum propositional logic, introduced by Birkhoff and von Neumann, formalizes reasoning about experimental propositions in quantum mechanics through closed subspaces of Hilbert spaces. We provide a comprehensive complexity analysis of the satisfiability problem for quantum logic formulas over the connectives conjunction, disjunction, and negation. Distinguishing between weak satisfiability (evaluation to a nonzero subspace) and strong satisfiability (evaluation to the full space), we establish that both notions coincide with Boolean satisfiability for dimension one, are classically NP complete for dimension two, and become complete for the Blum Shub Smale class NP_R when dimension d >= 3 is fixed. Our principal contribution is twofold. First, we present two alternative constructive reductions from quantum logic satisfiability to the Existential Theory of the Reals (ETR): a realification based encoding that explicitly handles the complex to real translation through commutant characterizations, and a rank one column encoding with orthogonal splitting gadgets. Both reductions yield polynomial size systems of quadratic equations for fixed dimension, proving membership in the complexity class existsR and hence in PSPACE via Cannys algorithm. Second, we provide detailed size bounds distinguishing weak and strong satisfiability: weak satisfiability encodes with O(n D^2 + N_v D) scalar variables where n is the number of atoms, D the real dimension, and N_v the number of disjunctions, while strong satisfiability requires O(n D^2 + N_v D^2) variables due to basis vector witnesses. When dimension is part of the input, strong satisfiability becomes polynomial time equivalent to feasibility of noncommutative integer polynomial equations. These results position quantum logic satisfiability precisely between classical NP and existsR, highlighting dimension as a fundamental complexity parameter.
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 satisfiablity 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 satisfiablity 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.
This paper presents a complete algorithmic study of the decision Boolean Satisfiability Problem under the classical computation and quantum computation theories. The paper depicts deterministic and probabilistic algorithms, propositions of their properties and the main result is that the problem has not an efficient algorithm (NP is not P). Novel quantum algorithms and propositions depict that the complexity by quantum computation approach for solving the Boolean Satisfiability Problem or any NP problem is lineal time.
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.