Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SAT, Gadgets, Max2XOR, and Quantum Annealers

Carlos Ansótegui, Jordi Levy

TL;DR

This work reframes quantum annealers as Max2XOR solvers and formalizes a gadget-based pipeline to reduce SAT to Max2XOR (and hence to QUBO/Ising) for initialization on annealing devices. It introduces and analyzes several gadget families—Regular-like, Tree-like, and Clique-like—and measures trade-offs between energy gap $\Delta E$, auxiliary variable count, and connectivity, showing how denser constructions can reduce qubit overhead at the expense of gap. A direct (2,3)-gadget from 3SAT to Max2XOR achieves a favorable balance with $\Delta E=4$ and minimal auxiliary variables, while the clique-like gadget minimizes qubits at the cost of a smaller gap $\Delta E=O(1/k^2)$. The authors also present a MIP-based approach to automatically search for gadgets, confirming known patterns and enabling scalable discovery for small $k$. Overall, the paper advances SAT-to-annealer mappings by quantifying energy-gap–qubit-count trade-offs and providing practical methods to tailor encodings to hardware architectures.

Abstract

Quantum Annealers are basically quantum computers that with high probability can optimize certain quadratic functions on Boolean variables in constant time. These functions are basically the Hamiltonian of Ising models that reach the ground energy state, with a high probability, after an annealing process. They have been proposed as a way to solve SAT. These Hamiltonians can be seen as Max2XOR problems, i.e. as the problem of finding an assignment that maximizes the number of XOR clauses of at most 2 variables that are satisfied. In this paper, we present several gadgets to reduce SAT to Max2XOR. We show how they can be used to translate SAT instances to initial configurations of a quantum annealer.

SAT, Gadgets, Max2XOR, and Quantum Annealers

TL;DR

This work reframes quantum annealers as Max2XOR solvers and formalizes a gadget-based pipeline to reduce SAT to Max2XOR (and hence to QUBO/Ising) for initialization on annealing devices. It introduces and analyzes several gadget families—Regular-like, Tree-like, and Clique-like—and measures trade-offs between energy gap , auxiliary variable count, and connectivity, showing how denser constructions can reduce qubit overhead at the expense of gap. A direct (2,3)-gadget from 3SAT to Max2XOR achieves a favorable balance with and minimal auxiliary variables, while the clique-like gadget minimizes qubits at the cost of a smaller gap . The authors also present a MIP-based approach to automatically search for gadgets, confirming known patterns and enabling scalable discovery for small . Overall, the paper advances SAT-to-annealer mappings by quantifying energy-gap–qubit-count trade-offs and providing practical methods to tailor encodings to hardware architectures.

Abstract

Quantum Annealers are basically quantum computers that with high probability can optimize certain quadratic functions on Boolean variables in constant time. These functions are basically the Hamiltonian of Ising models that reach the ground energy state, with a high probability, after an annealing process. They have been proposed as a way to solve SAT. These Hamiltonians can be seen as Max2XOR problems, i.e. as the problem of finding an assignment that maximizes the number of XOR clauses of at most 2 variables that are satisfied. In this paper, we present several gadgets to reduce SAT to Max2XOR. We show how they can be used to translate SAT instances to initial configurations of a quantum annealer.
Paper Structure (10 sections, 6 theorems, 23 equations, 7 figures)

This paper contains 10 sections, 6 theorems, 23 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Quantum Annealers as Max2XOR Solvers
  4. New Gadgets From SAT to Max2XOR
  5. A Gadget from 3SAT to Max2XOR
  6. A Regular-Like Gadget
  7. A Tree-Like Gadget
  8. A Clique-Like Gadget
  9. Computing Gadgets Automatically
  10. Conclusions

Key Result

Lemma 2

The composition of a $(\alpha_1,\beta_1)$-gadget from $\mathcal{F}_1$ to $\mathcal{F}_2$ and a $(\alpha_2,\beta_2)$-gadget from $\mathcal{F}_2$ to $\mathcal{F}_3$ results into a $(\beta_1\,(\alpha_2-1)+\alpha_1,\ \beta_1\beta_2)$-gadget from $\mathcal{F}_1$ to $\mathcal{F}_3$.

Figures (7)

  • Figure 1: Graphic representation of the $(5/2,9/2)$-gadget with $\Delta E=2$ from 3SAT to Max2XOR proposed by Nüß lein et al. Nusslein. Blue edges represent equal-one constraints, and red dashed edges are equal-zero constraints.
  • Figure 2: Graphic representation of the $(3,5)$-gadget with $\Delta E=4$ from 3SAT to Max2XOR obtained with the method proposed by Chancellor et al. Chancellor.
  • Figure 3: Graphic representation of the $(4,6)$-gadget with $\Delta E=4/3$ obtained by Tseitin encoding of a 3SAT clause, as proposed by Bian et al. quantumSebastianiConferencequantumSebastianiJournal.
  • Figure 4: Graphical representation of the $(2,3)$-gadget with $\Delta E=4$ reducing Max3SAT to Max2XOR and based on Trevisan's gadgets gadget from Max3SAT to Max2SAT.
  • Figure 5: Graphical representation of $T^0(x_1\vee\cdots\vee x_k, \hat{1})$, defining a $(k-1,3/2(k-1)$-gadget with $\Delta E=4$ form kSAT to Max2XOR that introduces $k-2$ variables. For $k=3$, this gadget corresponds to the one in Figure \ref{['fig:Max3SAT->Max2XOR']}.
  • ...and 2 more figures

Theorems & Definitions (17)

  • Definition 1
  • Lemma 2
  • proof
  • Definition 3
  • Definition 4
  • Lemma 5
  • proof
  • Theorem 6
  • proof
  • Definition 7
  • ...and 7 more