Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover's algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexity O(m) -- linear to the number of clauses m -- per Grover iteration. In this work, we develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We have proved the correctness of our approaches and demonstrated them in simulations.

翻译：布尔可满足性（SAT）求解是计算机科学中的基本问题。寻求高效的SAT求解算法对计算机科学及其他诸多领域具有广泛意义。现有文献基于Grover算法提出了量子SAT求解器。尽管现有量子SAT求解器能同时考虑所有可能的输入，但每次Grover迭代中，它们需逐一顺序评估公式中的每个子句，导致时间复杂度为O(m)——即与子句数量m呈线性关系。本研究开发了一种并行量子SAT求解器，通过利用额外的纠缠量子比特，将每次迭代的时间复杂度从线性时间O(m)降低至常数时间O(1)。为进一步提升应对超大规模问题的可扩展性，我们基于量子隐形传态提出了并行SAT求解器的分布式版本，使得所需的总量子比特在一组量子计算机（节点）间共享与分布，并由所有节点协作完成量子SAT求解。我们已证明所提方法的正确性，并通过仿真实验进行了验证。