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

TL;DR

This paper introduces AmplifySAT, a classical algorithm inspired by quantum amplitude amplification, designed to improve solving Boolean k-SAT problems by amplifying optimal solutions within a non-convex optimization framework.

Contribution

The paper presents a novel quantum-inspired classical algorithm, AmplifySAT, for k-SAT that applies a conditioning operation to amplify optimal solutions, bridging quantum concepts with classical optimization.

Findings

AmplifySAT effectively amplifies solutions in non-convex optimization.

The method offers potential advantages over traditional algorithms like simulated annealing.

Limitations include challenges in scaling and generalization to larger problem instances.

Abstract

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 "amplifying" the function value at points corresponding to optimal solutions. We describe the algorithm for achieving this amplification, 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.