Solving SAT and MaxSAT with a Quantum Annealer: Foundations, Encodings, and Preliminary Results
arXiv:1811.02524
Abstract
Quantum annealers (QAs) 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 (qubits), also known as Ising 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, together with increased connectivity. 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, with some limitations, MaxSAT- into Ising 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 for certain SAT and MaxSAT problems.
arXiv commentunder submission to Information and Computation
References in corpus (17)
- Ising formulations of many NP problems
- Quantum Annealing in the Transverse Ising Model
- A practical heuristic for finding graph minors
- A case study in programming a quantum annealer for hard operational planning problems
- Solving the Optimal Trading Trajectory Problem Using a Quantum Annealer
- Searching for quantum speedup in quasistatic quantum annealers
- Quantum Annealing Implementation of Job-Shop Scheduling
- Experimental determination of Ramsey numbers
- Exponential Complexity of the Quantum Adiabatic Algorithm for certain Satisfiability Problems
- A Quantum Annealing Approach for Fault Detection and Diagnosis of Graph-Based Systems
- Prime factorization using quantum annealing and computational algebraic geometry
- MAX 2-SAT with up to 108 qubits
- Experimental quantum annealing: case study involving the graph isomorphism problem
- Different Adiabatic Quantum Optimization Algorithms for the NP-Complete Exact Cover and 3SAT Problems
- Performance of a quantum annealer on range-limited constraint satisfaction problems
- Quantum Annealing and the Satisfiability Problem
- Quantum Annealing for Prime Factorization