Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms
This addresses a computationally intensive problem in AI and optimization with potential applications in real-world scenarios, though it appears incremental as it builds on existing QUBO and quantum annealing methods.
The paper tackles the problem of estimating the density of states for Boolean satisfiability problems, which is computationally infeasible with state-of-the-art methods, by proposing a novel approach based on concentration of measure inequalities that yields a QUBO formulation suitable for quantum annealing, and compares results from a D-Wave quantum annealer against classical algorithms like HFS and SMT solvers, showing competitive performance.
Given a Boolean formula $φ(x)$ in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly $e$ clauses, for all values of $e$. Thus, the density of states is a histogram of the number of unsatisfied clauses over all possible assignments. This computation generalizes both maximum-satisfiability (MAX-SAT) and model counting problems and not only provides insight into the entire solution space, but also yields a measure for the \emph{hardness} of the problem instance. Consequently, in real-world scenarios, this problem is typically infeasible even when using state-of-the-art algorithms. While finding an exact answer to this problem is a computationally intensive task, we propose a novel approach for estimating density of states based on the concentration of measure inequalities. The methodology results in a quadratic unconstrained binary optimization (QUBO), which is particularly amenable to quantum annealing-based solutions. We present the overall approach and compare results from the D-Wave quantum annealer against the best-known classical algorithms such as the Hamze-de Freitas-Selby (HFS) algorithm and satisfiability modulo theory (SMT) solvers.