A Quantum-Inspired Classical Solver for Boolean k-Satisfiability Problems

In this paper we detail a classical algorithmic approach to the k-satisfiability (k-SAT) problem that is inspired by the quantum amplitude amplification algorithm. This work falls under the emerging field of quantum-inspired classical algorithms. To propose our modification, we adopt an existing problem model for k-SAT known as Universal SAT (UniSAT), which casts the Boolean satisfiability problem as a non-convex global optimization over a real-valued space. The quantum-inspired modification to UniSAT is to apply a conditioning operation to the objective function that has the effect of "am-plifying" the function value at points corresponding to optimal solutions. We describe the algorithm for achieving this ampli-fication, termed "AmplifySAT," which follows a familiar two-step process of applying an oracle-like operation followed by a reflection about the average. We then discuss opportunities for meaningfully leveraging this processing in a classical digital or analog computing setting, attempting to identify the strengths and limitations of AmplifySAT in the context of existing non-convex optimization strategies like simulated annealing and gradient descent.