TY - JOUR
AU - Sahai, Tuhin
AU - Mishra, Anurag
AU - Pasini, Jose Miguel
AU - Jha, Susmit
PY - 2020/04/03
Y2 - 2021/04/13
TI - Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms
JF - Proceedings of the AAAI Conference on Artificial Intelligence
JA - AAAI
VL - 34
IS - 02
SE - AAAI Technical Track: Constraint Satisfaction and Optimization
DO - 10.1609/aaai.v34i02.5524
UR - https://ojs.aaai.org/index.php/AAAI/article/view/5524
SP - 1627-1635
AB - <p>Given a Boolean formula <em>ϕ</em>(<em>x</em>) in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly <em>e</em> clauses, for all values of <em>e</em>. 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 <em>hardness</em> 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.</p>
ER -