Computational Complexity of Quantum Satisfiability

Abstract

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 R-d and C-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 NPR-complete with one, perhaps, closest in spirit to the classical Cook-Levin Theorem. More precisely, strong satisfiability of boolean AND boolean OR boolean AND-terms is complete, while that of boolean AND boolean OR-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 NPR 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