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. © 2020 Elsevier Inc. All rights reserved

Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results / Bian, Z.; Chudak, F.; Macready, W.; Roy, A.; Sebastiani, R.; Varotti, S.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 275:(2020), pp. 104609.1-104609.34. [10.1016/j.ic.2020.104609]

Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results

Sebastiani R.;Varotti S.
2020-01-01

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. © 2020 Elsevier Inc. All rights reserved
2020
Bian, Z.; Chudak, F.; Macready, W.; Roy, A.; Sebastiani, R.; Varotti, S.
Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results / Bian, Z.; Chudak, F.; Macready, W.; Roy, A.; Sebastiani, R.; Varotti, S.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 275:(2020), pp. 104609.1-104609.34. [10.1016/j.ic.2020.104609]
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0890540120300973-main.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 2.67 MB
Formato Adobe PDF
2.67 MB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/287765
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 15
  • OpenAlex ND
social impact