Paper Info
Title
Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report.
Abstract
Quantum annealers (QA) are specialized quantum computers that minimize objective functions over discrete variables by physically exploiting quantum effects. Current QA platforms allow for the optimization of quadratic objectives defined over binary variables, that is, they solve quadratic unconstrained binary optimization (QUBO) problems. In the last decade, QA systems as implemented by D-Wave have scaled with Moore-like growth. Current architectures provide 2048 sparsely-connected qubits, and continued exponential growth is anticipated. We explore the feasibility of such architectures for solving SAT and MaxSAT problems as QA systems scale. We develop techniques for effectively encoding SAT and MaxSAT into QUBO problems compatible with sparse QA architectures. We provide the theoretical foundations for this mapping, and present encoding techniques that combine offline Satisfiability and Optimization Modulo Theories with on-the-fly placement and routing. Preliminary empirical tests on a current generation 2048-qubit D-Wave system support the feasibility of the approach. We provide details on our SMT model of the SAT-encoding problem in the hopes that further research may improve upon the scalability of this application of SMT technology. Further, these models generate hard SMT problems which may be useful as benchmarks for solvers.
Year
DOI
Venue
2017
10.1007/978-3-319-66167-4_9
Lecture Notes in Artificial Intelligence
Field
DocType
Volume
Maximum satisfiability problem,Quantum,Mathematical optimization,Quadratic unconstrained binary optimization,Computer science,Algorithm,Quadratic equation,Quantum computer,Qubit,Exponential growth,Binary number
Conference
10483
ISSN
Citations 
PageRank 
0302-9743
4
0.43
References 
Authors
21
6
Name
Order
Citations
PageRank
Zhengbing Bian1202.20
Fabian A. Chudak2101.50
William G. Macready316139.07
Aidan Roy4724.26
Roberto Sebastiani52455237.86
Stefano Varotti650.78