Solving SAT and MaxSAT with a Quantum Annealer: Foundations, Encodings and a Preliminary Report

Supervisor
Roberto Sebastiani - Università di Trento
Date and time
Monday, February 25, 2019 at 2:00 PM - Aula Verde
Programme Director
External reference
Publication date
January 24, 2019
Department
Computer Science  

Summary

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.

In this talk we first present a brief introduction to D-Wave's QAs, given from a computer science perspective, and to our collaboration with D-Wave. Then we present recently-published work in collaboration with D-Wave, in which 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 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 will complete the presentation by discussing some features of the novel D-Wave Pegasus architecture, under development.

Contact Person: Lorenzo Bottarelli





© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234