Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms

被引:0
|
作者
Sahai, Tuhin [1 ]
Mishra, Anurag [1 ]
Pasini, Jose Miguel [2 ]
Jha, Susmit [3 ]
机构
[1] United Technol Res Ctr, Berkeley, CA 94705 USA
[2] United Technol Res Ctr, Hartford, CT USA
[3] SRI Int, Comp Sci Lab, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA
来源
THIRTY-FOURTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THE THIRTY-SECOND INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE AND THE TENTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE | 2020年 / 34卷
基金
美国国家科学基金会;
关键词
COMPLEXITY;
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Given a Boolean formula phi(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 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.
引用
收藏
页码:1627 / 1635
页数:9
相关论文
共 25 条