@article{Sahai_Mishra_Pasini_Jha_2020, title={Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms}, volume={34}, url={https://ojs.aaai.org/index.php/AAAI/article/view/5524}, DOI={10.1609/aaai.v34i02.5524}, abstractNote={<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>}, number={02}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Sahai, Tuhin and Mishra, Anurag and Pasini, Jose Miguel and Jha, Susmit}, year={2020}, month={Apr.}, pages={1627-1635} }