AF: Small: Exact algorithms for the quantum satisfiability problem

理论计算机科学中最基本的问题之一是k-满足性问题（k-SAT），它大致上是这样问的：给定一组特殊形式的布尔约束，每个约束作用于n位中的k位，是否存在对所有n位同时满足每个约束的赋值？这个问题在从人工智能到电子设计自动化再到定理证明等领域都有着深远的应用，因此强调了它的重要性。最近，k-SAT的量子推广出现了，称为k-QSAT，它在量子纠错码等领域中找到了应用。此外，k-QSAT在物理上是有动机的，因为它可以被认为是模拟自然界中的量子系统如何受到局部量子约束的控制。然而，与k-SAT不同，对k-QSAT的了解要少得多。该项目的目的正是为了弥合这一基本知识差距。特别是，这个项目广泛地问：在什么情况下可以开发非平凡的算法来解决k-QSAT？这个问题的解决将产生深刻的见解，量子系统的性质可以有效地计算一个经典的计算机。此外，所取得的成果将通过各种途径传播，包括会议、新课程材料和旨在使年轻计算机科学家接触研究前沿的高中讲习班。

Among the most fundamental problems in theoretical computer science is the k-SATISFIABILITY problem (k-SAT), which roughly asks: Given a set of Boolean constraints of a special form, each acting on k out of n bits, does there exist an assignment to all n bits which simultaneously satisfies every constraint? This problem has far-reaching applications in areas ranging from artificial intelligence to electronic design automation to theorem proving, thus underscoring its significance. More recently, a quantum generalization of k-SAT has arisen, known as k-QSAT, which finds applications in areas such as quantum error-correcting codes. Moreover, k-QSAT is physically well-motivated, as it can be thought of as modeling how quantum systems in nature are governed by local quantum constraints. Unlike k-SAT, however, much less is known about k-QSAT. The aim of this project is precisely to close this fundamental knowledge gap. In particular, this project broadly asks: In what cases can non-trivial algorithms be developed for solving k-QSAT? The resolution of this question will yield deep insights into which properties of quantum systems can be computed efficiently by a classical computer. Moreover, the results obtained will be disseminated through a variety of avenues, including conferences, new course materials, and high school workshops aimed at exposing young computer scientists to the frontiers of research.