# SAT, Gadgets, Max2XOR
and Quantum Annealers

Carlos Ansótegui
Logic & Optimization Group,
Universitat de Lleida, Spain  Jordi Levy
IIIA, CSIC, Spain

###### Abstract

Quantum Annealers are presented as 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 in some
preliminary works.

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 focus on introducing 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.

Keywords: Maximum Satisfiability; Quantum Annealers; Satisfiability

##  1 Introduction

### Quantum Annealers

Quantum Computation exploits some particularities of quantum mechanics, such
as superposition, interference, and entanglement to solve some hard problems
such as the ones we face in Artificial Intelligence. Current quantum computers
are still too small to compete with classical computers, but the rapid
increase in their number of qubits could replace them in some of these hard
problems. Most research in quantum computing is focused on the model of
quantum circuits, where gates are quantum operators that act on a qubit or a
superposition of them.

An alternative model is _Quantum Annealing_. D-Wave Systems
Inc.111https://www.dwavesys.com/. has constructed some computers based on this
model of computation with more than 5000 qubits, surpassing (in the number of
qubits) the rest of the manufacturers of quantum computers. However, in these
machines, we can only decide the _coupling factor_ $J_{ij}$ between certain
pairs of qubits $i$ and $j$, and the _biases_ $h_{i}$ of each qubit $i$. From
an initial state of minimal energy and absence of magnetic fields, the system
evolves into a system described by an Ising Hamiltonian $\mathcal{H}_{Ising}$.
The energy eigenvalues of $\mathcal{H}_{Ising}$ are

$E(\vec{s})=\sum_{i\in V_{G}}h_{i}s_{i}+\sum_{(i,j)\in
E_{G}}J_{ij}\,s_{i}\,s_{j}$

where $s_{i}\in\\{+1,-1\\}$ are the spins of the qubits and $G=(V_{G},E_{G})$
is a graph. With a high probability, that depends on the difference of energy
between the ground energy state and the next energy level, when observing the
state after some time, we get the ground-energy state that minimizes this
energy function. The Landau-Zener describes the probability of success
(finishing in the minimal energy state) for a two-states system with one
$1/2$-spin particle with energy gap $\Delta$ under the action of a varying
external magnetic field at rate $c$ as

$p=1-e^{\frac{-\pi\,\Delta^{2}}{4c}}$

Mehta et al. (2022) argue that, although the quantum annealers are more
complicated systems, the probability can be approximated by this two-level
system.

In order to increase the probability of finding this minimum, the experiment
is repeated many times. Biases and couplings depend on the particular model of
the quantum annealer.222For old Chimera-base D-Wave 2000 series, they were
$h_{i}\in[-2,2]$ and $J_{ij}\in[-1,1]$. In more modern models they are
$h_{i}\in[-4,4]$ and $J_{ij}\in[-2,1]$. In this paper, for simplicity, we
assume that they are in the range $h_{i}\in[-1,1]$ and in $J_{ij}\in[-1,1]$,
being our conclusions easily adapted for other ranges. The structure of the
machine also depends on the model. For our purposes, we simply assume that $G$
is an undirected sparse graph. In other words, we will idealize quantum
annealers as devices that are able to solve –in constant time and with high
probability 333Here we use high probability in the mathematical sense, as a
non-zero probability. that depends exponentially on the difference between the
minimal solution and the next state– a quadratic function where only some
quadratic terms are allowed.

In this paper, we will show that (obviating some technical details) a quantum
annealer can be seen as a Max2XOR solver with constraint weights in the reals
$[0,1]$. Therefore, we focus on the problem of finding gadgets to reduce the
satisfiability of a CNF formula (SAT) to the satisfiability of the _maximum_
number of 2XOR constraints (Max2XOR) and analyze which (theoretical) features
of the gadgets are desirable for quantum annealers. In some sense, a
subproduct of our contribution could be seen as one more step to assess the
maturity and potential of quantum annealers to solve the SAT problem.

### Max2XOR

Exclusive OR (XOR), here written $\oplus$, may be an alternative to the use of
traditional OR to represent propositional formulas. In practice, many
approaches combining SAT and XOR reasoning have been presented Li (2000a, b);
Baumgartner and Massacci (2000); Li (2003); Heule and van Maaren (2004); Heule
et al. (2004); Chen (2009); Soos et al. (2009); Laitinen et al. (2012); Soos
(2010); Laitinen et al. (2011, 2012); Soos and Meel (2019). By writing clauses
$x_{1}\oplus\cdots\oplus x_{k}$ as constraints $x_{1}\oplus\cdots\oplus
x_{k}=1$ or $x_{1}\oplus\cdots\oplus x_{k}=0$, where $1$ means true and $0$
false, we can avoid the use of negation, because $\neg x\oplus C=k$ is
equivalent to $x\oplus C=1-k$. The equivalent to the resolution rule for XOR
constraints, called XOR resolution rule, is

$\begin{array}[]{c}x\oplus A=k_{1}\\\ x\oplus B=k_{2}\\\ \hline\cr A\oplus
B=k_{1}\oplus k_{2}\end{array}$

where $A$ and $B$ are clauses. In the particular case of $A=B=\emptyset$ and
$k_{1}\neq k_{2}$, this rule concludes the contradiction $0=1$, that we
represent as  . The proof system containing only this rule allows us to
produce polynomial refutations for any unsatisfiable set of XOR constraints,
using Gaussian elimination. Therefore, unless $P=NP$, we cannot polynomially
translate any propositional formula into an equivalent conjunction of XOR
constraints.444We can translate any OR clause $x_{1}\vee\dots\vee x_{k}$ into
the set of weighted XOR constraints:
$\bigcup_{S\subseteq\\{1,\dots,k\\}}\\{_{(1/2^{k-1})}\,\bigoplus_{i\in
S}x_{i}=1\\}$ This translation allows us to reduce SAT to MaxXOR. However, the
reduction is not polynomial, because it translates every clause of size $k$
into $2^{k}-1$ constraints. In Section 4, we describe a polynomial reduction
that avoids this exponential explosion on expenses of introducing new
variables. However, the SAT problem can be reduced to the Max2XOR problem,
i.e., the problem of maximizing the number of 2XOR constraints that can be
satisfied simultaneously. Formally, a Max2XOR problem is a set of pairs
$\\{_{(w_{1})}\,C_{1}=k_{1},\dots,_{(w_{n})}\,C_{n}=k_{n}\\}$, where $w_{i}$
are positive rational numbers (we can also consider the special case of
natural weights or the generalization to positive real weights), $C_{i}$ are
clauses form by one variable or the XOR disjuntion (or sum modulo two) of two
variables, and $k_{i}$ are either $0$ or $1$, representing $false$ and $true$,
respectively. A solution is an optimal assignment that maximizes the sum of
the weights of satisfied constraints.

For example, $\\{_{(1/2)}\,x=1,\ _{(1/2)}\,y=1,\ _{(1/2)}\,x+y=1\\}$ is a
Max2XOR problem where the set of solutions (optimal assignments) are exactly
the set of solutions of the SAT formula $\\{x\vee y\\}$, i.e. the assignments
that assign $x$, or $y$, or both, to one. All these three optimal assignments
satisfy two constraints with a total weight equal to one. In this paper, to
formalize the reduction from SAT to Max2XOR we will use gadgets.

### Gadgets

Traditionally, the word ”gadget” is used to denote a finite combinatorial
structure that allows translating constraints of one problem to constraints of
another. In Trevisan et al. (2000), the notion is formalized, defining a
$(\alpha,\beta)$-_gadget_ as a function from a family of constraints
$\mathcal{F}_{1}$ to another family $\mathcal{F}_{2}$ that translate every
constraint $f(\vec{x})$ in $\mathcal{F}_{1}$ to a set of $\beta$ constraints
$\\{g_{i}(\vec{x},\vec{b})\\}_{i=1,\dots,\beta}$ in $\mathcal{F}_{2}$, where
the $b$’s are (fresh) _auxiliary variables_ such that, when $f(\vec{x})$ is
satisfied for some assignment of the $x$’s, we can find an assignment to the
$b$’s that satisfy $\alpha$ constraints $g(\vec{x},\vec{b})$. Conversely, when
$f(\vec{x})$ is falsified, no assignment for the $b$’s satisfy strictly more
than $\alpha-1$ constraints $g(\vec{x},\vec{b})$. If, additionally, when
$f(\vec{x})$ is falsified, some assignment for the $b$’s satisfy exactly
$\alpha-1$ constraints $g(\vec{x},\vec{b})$, we say that the gadget is
_strict_. This definition can be generalized to _weighted_ constraints, where
the weights are real numbers.555Although a more detailed analysis would show
that we can restrict them to be rational numbers. Then, instead of the number
of satisfied constraints, we talk about the sum of the weights of satisfied
constraints.

There is a long tradition of the use of gadgets. For instance, the
$(k-2,k-2)$-gadget:

$x_{1}\vee\cdots\vee x_{k}\to\left\\{\begin{array}[]{l}x_{1}\vee x_{2}\vee
b_{1},\\\ \neg b_{1}\vee x_{3}\vee b_{2},\\\ \cdots,\\\ \neg b_{k-4}\vee
x_{k-2}\vee b_{k-3},\\\ \neg b_{k-3}\vee x_{k-1}\vee x_{k}\end{array}\right.$
(1)

reduces $k$SAT to 3SAT. The following (weighted) $(3.5,4)$-gadget Trevisan et
al. (2000) reduces 3SAT to Max2SAT:

$x_{1}\vee x_{2}\vee x_{3}\to\left\\{\begin{array}[]{ll}{}_{(1/2)}\,x_{1}\vee
x_{3},\ _{(1/2)}\,\neg x_{1}\vee\neg x_{3},\\\ {}_{(1/2)}\,x_{1}\vee\neg b,\
_{(1/2)}\,\neg x_{1}\vee b,\\\ {}_{(1/2)}\,x_{3}\vee\neg b,\ _{(1/2)}\,\neg
x_{3}\vee b,\\\ {}_{(1)}\,x_{2}\vee b\end{array}\right.$ (2)

In Ansótegui and Levy (2021) new gadgets reducing SAT to Max2SAT are
introduced. The authors show, formally and empirically, that the new reduction
allows solving efficiently the Pigeon Hole Principle, i.e. they prove that
there exists a polynomial MaxSAT resolution proof Bonet et al. (2007) and that
a general purpose MaxSAT solvers can solve the resulting Max2SAT formula.

Defining $Opt(P)$ as the maximal number of satisfied constraints of a problem
$P$, $Cost(P)$ as the minimal number of falsified constraints, and $Weight(P)$
the number of constraints in $P$, we have that, if $P$ is translated into
$P^{\prime}$ using a $(\alpha,\beta)$-gadget, then

$\begin{array}[]{l}Opt(P^{\prime})\leq(\alpha-1)Weight(P)+Opt(P)\\\
Cost(P^{\prime})\geq(\beta-\alpha)Weight(P)+Cost(P)\end{array}$

with equalities if the gadget is strict. This allows us to obtain an algorithm
to maximize $P$, using an algorithm to maximize $P^{\prime}$.

When $\alpha=\beta$ we preserve the cost, hence the satisfiability. Then,
given a decision algorithm for $P^{\prime}$, we get a decision algorithm for
$P$.

Moreover, when we have a $p$-approximation algorithm for $P^{\prime}$ we can
get an $(1-\alpha(1-p))$-approximation algorithm for $P$. Therefore,
traditionally, we were interested in gadgets with minimal $\alpha$ in order to
minimize the error in the approximation.

If the algorithm is based on deriving empty clauses, i.e. that prove lower
bounds for the cost, we will be interested in gadgets that minimize
$\beta-\alpha$. Notice that in the case that $P$ is a decision problem, then
we can say that $P$ is unsatisfiable if, and only if,
$Cost(P^{\prime})\geq(\beta-\alpha)Weight(P)+1$.

In this paper, we are interested on maximizing another feature of gadgets,
that we will call _energy gap_ , and will be introduced later. We will also
discuss on the number of auxiliary variables the gadget introduces and how
_flexible_ is the structure itself of the gadget.

### Related Work

Santra et al. Santra et al. (2014) experimentally study the performance of one
of the first quantum annealers, with 108 qubits, on random Max2SAT problems.
Despite the small size of tested instances, they observe that the probability
of obtaining a correct answer decreases with the clause density (when we
increase the number of clauses while keeping the number of variables fixed).
This is explained by the decrease in the energy gap between the ground state
and the first excited state. They find that success probability decreases
around the critical clause density. However, it is not correlated with the
time required by classical MaxSAT solvers (they compare _akmaxsat_) to find a
solution. In order to avoid the problem with not connectivity between all
pairs of qubits, they only consider Max2SAT formulas
$\Gamma=\bigwedge_{i=1}^{m}C_{i}$ where clauses $C_{i}=x_{j_{i}}\vee
x_{j_{i}^{\prime}}$ only contain pairs of variables whose corresponding qubits
can be coupled $(j_{i},j_{i}^{\prime})\in E$. Moreover, to ensure that the
bounds in the coupling factors are not exceeded, they do not allow repeated
clauses. The Hamiltonian is then $H=\sum_{(x_{i}\vee
x_{j})\in\Gamma}\frac{1-\sigma_{i}}{2}\frac{1-\sigma_{j}}{2}$ where
$\sigma_{i}$ is the qubit associated to variable $x_{i}$.

Douglass et al. Douglass et al. (2015) explores the use of a quantum annealer
for the construction of SAT filters. In this case, the encoding involves the
translation of MaxCUT, Not-all-equal 3-SAT, 2-in-4-SAT into a Hamiltonian.
This translation is almost direct. The authors already remarked that the
translation of SAT would involve the use of auxiliary variables, which are
called _ancillary variables_.

Bian et al. Bian et al. (2017, 2020) already using a 2048 qubits quantum
annealer, explore the feasibility of solving SAT, without limitation on the
size of clauses. The basic idea is to decompose any clause (or other
subformulas) into constraints of at most 3 variables using the traditional
Tseitin encoding. Like in the case of gadgets, this requires the introduction
of auxiliary variables. For instance, we can decompose $x_{1}\vee x_{2}\vee
x_{3}\vee x_{4}$ as $\\{b_{1}\leftrightarrow x_{1}\vee
x_{2},b_{2}\leftrightarrow x_{3}\vee x_{4},b_{1}\vee b_{2}\\}$. Then, each one
of these constraints or subformulas contributes to the Hamiltonian. For
instance, $b_{1}\leftrightarrow x_{1}\vee x_{2}$ contributes by adding
$5/2+1/2x_{1}+1/2x_{2}-b_{1}+1/2x_{1}x_{2}-x_{1}b_{1}-x_{2}b_{1}$666Abusing
from the notation, we identify the variable (that takes Boolean values $0$ or
$1$) with the qubit representing it (that takes values +1 or -1 when
measured). to the Hamiltonian. Below, we will see that this decomposition can
in fact be interpreted as a gadget, although the authors do not mention the
notion of a gadget in their paper. To ensure that the coupling factors are in
the range $[-1,1]$, in some cases they have to re-normalize the entire
Hamiltonian, dividing all factors by a constant. Moreover, they have to use
several qubits to represent the same variable, when there are several
occurrences of a variable in a formula. Then, they have to ensure that there
is a path of coupled qubits that connect all these occurrences. They present
some heuristics to find these paths.

Choi Choi (2010) analyzes the problem of allocating variables into qubits and
models it as a variant of graph embedding where in the process some
transformations are allowed, basically the contractions of paths into edges.
Bian et al. Bian et al. (2014) also analyze some methods with the same
purpose.

##  2 Preliminaries

A k-ary _constraint function_ is a Boolean function
$f:\\{0,1\\}^{k}\to\\{0,1\\}$. A _constraint family_ is a set $\mathcal{F}$ of
constraint functions (with possibly distinct arities). A _constraint_ , over
variables $V=\\{x_{1},\dots,x_{n}\\}$ and constraint family $\mathcal{F}$, is
a pair formed by a k-ary constraint function $f\in\mathcal{F}$ and a subset of
$k$ variables, noted $f(x_{i_{1}},\dots,x_{i_{k}})$, or $f(\vec{x})$ for
simplicity. A _(weighted) constraint problem_ or _(weighted) formula_ $P$,
over variables $V$ and constraint family $\mathcal{F}$, is a set of pairs
(weight, constraint) over $V$ and $\mathcal{F}$, where the weight is a
positive rational number, denoted
$P=\\{_{(w_{1})}\,f_{1}(x^{1}_{i_{1}},\dots,x^{1}_{i_{k_{1}}}),\dots,_{(w_{m})}\,f_{m}(x^{m}_{i_{1}},\dots,x^{m}_{i_{k_{m}}})\\}$.
The _weight_ of a problem is $Weight(P)=w_{1}+\cdots+w_{m}$.

An _assignment_ is a function $I:\\{x_{1},\dots,x_{n}\\}\to\\{0,1\\}$. We say
that an assignment $I$ _satisfies_ a constraint
$f(x_{i_{1}},\dots,x_{i_{k}})$, if
$I(f(\vec{x}))=_{\mbox{def}}f(I(x_{i_{1}}),\dots,I(x_{i_{k}}))=1$. The value
of an assignment $I$ for a constraint problem
$P=\\{_{(w_{i})}\,f_{i}(\vec{x})\\}_{i=1,\dots,m}$, is the sum of the weights
of the constraints that this assignment satisfies, i.e.
$I(P)=\sum_{i=1}^{m}w_{i}\,I(f_{i}(\vec{x}))$. We also define the sum of
weights of unsatisfied clauses as
$\overline{I}(P)=\sum_{i=1}^{m}w_{i}\,(1-I(f_{i}(\vec{x})))$. An assignment
$I$ is said to be _optimal_ for a constraint problem $P$, if it maximizes
$I(P)$. We define this optimum as $Opt(P)=\max_{I}I(P)$. We also define
$Cost(P)=\min_{I}\overline{I}(P)$, i.e. the minimum sum of weights of
falsified constraints, that fulfills $Opt(P)+Cost(P)=Weight(P)$.

Many optimization problems may be formalized as the problem of finding an
optimal assignment for a constraint problem. In the following we define some
of them:

  1. 1.

MaxkSAT is the constraint family defined by the constraint functions of the
form $f(x_{1},\dots,x_{r})=l_{1}\vee\cdots\vee l_{r}$, where every $l_{i}$ may
be either $x_{i}$ or $\neg x_{i}$ and $r\leq k$.

  2. 2.

MaxkXOR is the constraint family defined by the constraint functions
$f(x_{1},\dots,x_{r})=x_{1}\oplus\cdots\oplus x_{r}$ and
$f(x_{1},\dots,x_{r})=x_{1}\oplus\cdots\oplus x_{r}\oplus 1$, where $r\leq k$.

In this paper, we are interested in the problem Max2XOR, which has got very
little attention in the literature, probably because it is quite similar to
MaxCUT.

Next, we define gadgets as a transformation from constraints into sets of
weighted constraints (or problems). These transformations can be extended to
define transformations of problems into problems.

######  Definition 1.

Let $\mathcal{F}_{1}$ and $\mathcal{F}_{2}$ be two constraint families. A
_$(\alpha,\beta)$ -gadget_ from $\mathcal{F}_{1}$ to $\mathcal{F}_{2}$ is a
function that, for any constraint $f(\vec{x})$ over $\mathcal{F}_{1}$ returns
a weighted constraint problem
$P=\\{_{(w_{i})}\,g_{i}(\vec{x},\vec{b})\\}_{i=1,\dots,m}$ over
$\mathcal{F}_{2}$ and variables $\\{\vec{x}\\}\cup\\{\vec{b}\\}$, where
$\vec{b}$ are auxiliary variables distinct from $\vec{x}$, such that
$\beta=\sum_{i=1}^{m}w_{i}$ and, for any assignment
$I:\\{\vec{x}\\}\to\\{0,1\\}$:

  1. 1.

If $I(f(\vec{x}))=1$, for any extension of $I$ to
$I^{\prime}:\\{\vec{x}\\}\cup\\{\vec{b}\\}\to\\{0,1\\}$,
$I^{\prime}(P)\leq\alpha$ and there exist one of such extension with
$I^{\prime}(P)=\alpha$.

  2. 2.

If $I(f(\vec{x}))=0$, for any extension of $I$ to
$I^{\prime}:\\{\vec{x}\\}\cup\\{\vec{b}\\}\to\\{0,1\\}$,
$I^{\prime}(P)\leq\alpha-1$ and if, additionally, there exist one of such
extension with $I^{\prime}(P)=\alpha-1$ we say the gadget is strict.

######  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}$.

###### Proof.

The first gadget multiplies the total weight of constraints by $\beta_{1}$,
and the second by $\beta_{2}$. Therefore, the composition multiplies it by
$\beta=\beta_{1}\beta_{2}$.

For any assignment, if the original constraint is falsified, the optimal
extension after the first gadget satisfies constraints with a weight of
$\alpha_{1}-1$, and falsifies the rest $\beta_{1}-(\alpha_{1}-1)$. The second
gadget satisfies constraints for a weight of $\alpha_{2}-1$ of the falsified
plus $\alpha_{2}$ of the satisfied. Therefore, the composition satisfies
constraints with a total weight
$(\alpha_{2}-1)(\beta_{1}-(\alpha_{1}-1))+\alpha_{2}(\alpha_{1}-1)=\beta_{1}(\alpha_{2}-1)+\alpha_{1}-1$.

If the original constraint is satisfied, the optimal extension after the first
gadget satisfies $\alpha_{1}$ and falsifies the rest $\beta_{1}-\alpha_{1}$.
After the second gadget the weight of satisfied constraints is
$(\alpha_{2}-1)(\beta_{1}-\alpha_{1})+\alpha_{2}\alpha_{1}=\beta_{1}(\alpha_{2}-1)+\alpha_{1}$.

The difference between both situations is one, hence the composition is a
gadget, and $\alpha=\beta_{1}(\alpha_{2}-1)+\alpha_{1}$. ∎

##  3 Quantum Annealers as Max2XOR Solvers

As we mention in the introduction, a quantum annealer can be seen as a Max2XOR
solver. Roughly speaking, it is able to find (in constant time and with high
probability) the state $\sigma$ that minimizes the Ising Hamiltonian
$\mathcal{H}(\sigma)=\sum_{i}h_{i}\sigma_{i}+\sum_{(i,j)\in
E}J_{ij}\sigma_{i}\sigma_{j}$, where $\sigma_{i}$’s can get the values +1 or
-1. For every linear term $h_{i}\sigma_{i}$ of this Hamiltonian, we can get a
2XOR constraint ${}_{(h_{i})}\,x_{i}=0$, when $h_{i}>0$, or
${}_{(-h_{i})}\,x_{i}=1$, when $h_{i}<0$. Similarly, for each quadratic term
$J_{ij}\sigma_{i}\sigma_{j}$, we get a constraint ${}_{(J_{ij})}\,x_{i}\oplus
x_{j}=1$, when $J_{ij}>0$, or ${}_{(-J_{ij})}\,x_{i}\oplus x_{j}=0$, when
$J_{ij}<0$. Conversely, any Max2XOR problem may be trivially mapped into an
Ising Hamiltonian, probably normalizing i.e. multiplying all constraint
weights by the same constant, to ensure that the resulting couplings are in
$[-1,1]$ and biases in $[-2,2]$.

In the following, we review with further detail the related work on
constructing Hamiltonians for SAT and MaxSAT from the perspective of gadgets.

When in Santra et al. (2014) they say that every 2SAT clause $x_{i}\vee x_{j}$
contributes to the Hamiltonian as
$\frac{1-\sigma_{i}}{2}\frac{1-\sigma_{j}}{2}=1/4-1/4\sigma_{i}-1/4\sigma_{j}+1/4\sigma_{i}\sigma_{j}$,
they are implicitly defining a $(1,3/2)$-gadget from 2SAT to 2XOR:

$x_{i}\vee x_{j}\to\left\\{\begin{array}[]{l}{}_{(1/2)}\,x_{i}=1,\\\
{}_{(1/2)}\,x_{j}=1,\\\ {}_{(1/2)}\,x_{i}\oplus x_{j}=1\end{array}\right.$ (3)

In the following, we only describe the translation of clauses
$x_{1}\vee\cdots\vee x_{k}$ where all variables are positive. We can easily
generalize the transformation when any of the variables $x$ is negated, simply
by recalling that $\neg x\oplus y=k$ is equivalent to $x\oplus y=1-k$, and
$\neg x\oplus\neg y=k$ is equivalent to $x\oplus y=k$.

Notice also that we normalize the weights to ensure that the gap between the
sum of weights when the original constraint is falsified ($\alpha-1$) and the
sum when is satisfied ($\alpha$) is just one. Later, when from the Max2XOR
problem we construct the Hamiltonian, we can multiply the weights for the
maximal value that still allows biases and couplings to be inside their
corresponding ranges, while we try to maximize this gap. In the case of the
previous gadget, we could multiply all weights by $2$. We call this quantity
the _energy gap_ of the gadget, noted $\Delta E=2$. Formally,

######  Definition 3.

Given a gadget $P$ to Max2XOR, we define _energy gap_ as

$\Delta E=\min\\{\min_{{}_{(w)}\,x=0\in P\atop{}_{(w)}\,x=1\in
P}\\{2/w\\},\min_{{}_{(w)}\,x\oplus y=0\in P\atop{}_{(w)}\,x\oplus y=1\in
P}\\{1/w\\}\\}$

In the case of Bian et al. (2017, 2020), the polynomial
$5/2+1/2x_{1}+1/2x_{2}-x_{3}+1/2x_{1}x_{2}-x_{1}x_{3}-x_{2}x_{3}$, that they
give, implicitly defines the non-strict $(3,9/2)$-gadget with $\Delta E=1$:

$(x_{1}\vee x_{2}\leftrightarrow
x_{3})\to\left\\{\begin{array}[]{l}{}_{(1/2)}\,x_{1}=0\\\
{}_{(1/2)}\,x_{2}=0\\\ {}_{(1)}\,x_{3}=1\\\ {}_{(1/2)}\,x_{1}\oplus x_{2}=1\\\
{}_{(1)}\,x_{1}\oplus x_{3}=0\\\ {}_{(1)}\,x_{2}\oplus x_{3}=0\\\
\end{array}\right.$ (4)

Notice that the values of the polynomial coefficients correspond to the
weights of the constraints in the gadget. The independent term $5/2$ is only
introduced in order to ensure that the ground-state energy is zero. Recall
that this is just a convention, and the values of this term are not restricted
to any range.

The application of the Tseitin encoding also can be seen as a gadget. For
instance, the $(2,2)$-gadget to reduce 3SAT

$x_{1}\vee x_{2}\vee x_{3}\to\left\\{\begin{array}[]{l}x_{1}\vee
x_{2}\leftrightarrow b\\\ b\vee x_{3}\end{array}\right.$ (5)

The composition of this gadget (5) with both (3) and (4), results in the
$(4,6)$-gadget with $\Delta E=1$ from 3SAT to Max2XOR used in Bian et al.
(2020) to translate 3SAT clauses into Hamiltonian components, and represented
here in Figure 1. In the rest of the paper, we will use this graphical
representation where solid blue lines between $x$ and $y$ represent $x\oplus
y=1$ and red dashed lines represent $x\oplus y=0$. Constraints $x=0$ and $x=1$
are graphically represented by means of lines to a special node $\hat{1}$ or
$\hat{0}$.

$\hat{1}$$x_{1}$$x_{2}$$x_{3}$$b$$1/2$$1/2$$1/2$$1/2$$1$$1$$3/2$$1/2$

$\begin{array}[b]{l}{}_{(1/2)}\,x_{1}=0\\\ {}_{(1/2)}\,x_{2}=0\\\
{}_{(1/2)}\,x_{3}=1\\\ {}_{(3/2)}\,b=1\\\ {}_{(1/2)}\,x_{1}\oplus x_{2}=1\\\
{}_{(1)}\,x_{1}\oplus b=0\\\ {}_{(1)}\,x_{2}\oplus b=0\\\
{}_{(1/2)}\,x_{3}\oplus b=1\end{array}$

Figure 1: Graphic representation of the $(4,6)$-gadget obtained by Tseitin
encoding of a 3SAT clause, with $\Delta E=1$. Blue edges represent equal-one
constraints, and red dashed edges are equal-zero constraints.

##  4 New Gadgets From SAT to Max2XOR

As we have seen in the previous section, the construction of Hamiltonians to
solve a problem $P$ with a quantum annealer is basically the search for a
gadget from the constraints in $P$ to Max2XOR. In general, there are three
aspects that we will like to optimize in this gadget. First, we want to reduce
the number of auxiliary variables (or ancillary variables in quantum
terminology) because they imply the use of more qubits. Second, we want to
relax the structure of the gadget, and in general avoid the use of gadgets
with a dense structure (such as cliques), because there are limitations in the
architecture of the quantum annealer, i.e., the graph of allowed couplings.
Third, we want to maximize the energy gap, because this reduces the
probability of errors.

$\hat{1}$$x_{1}$$x_{3}$$x_{2}$$b$

$\begin{array}[b]{l}{}_{(1/2)}\,x_{1}\oplus x_{3}=1\\\ {}_{(1/2)}\,x_{1}\oplus
b=0\\\ {}_{(1/2)}\,x_{3}\oplus b=0\\\ {}_{(1/2)}\,x_{2}\oplus b=1\\\
{}_{(1/2)}\,b=1\\\ {}_{(1/2)}\,x_{2}=1\\\ \end{array}$

Figure 2: Graphical representation of the $(2,3)$-gadget reducing Max3SAT to
Max2XOR and based on Trevisan’s gadget from Max3SAT to Max2SAT. All
constraints have weight $1/2$.

###  4.1 A Gadget from 3SAT to Max2XOR

An easy way to reduce SAT to Max2XOR is to reduce SAT to 3SAT, using the
gadget (1), this to Max2SAT, using the gadget (2) Trevisan et al. (2000);
Ansótegui and Levy (2021), and this to Max2XOR, using the gadget (3).

The concatenation of the gadget (2) and the gadget (3) results into the
$(2,3)$-gadget described in Figure 2 with $\Delta E=2$. This gadget is similar
to the gadget used in Bian et al. (2020) for 3SAT (and represented in Figure
1), but it has a better energy gap. In fact, this gadget is optimal in terms
of minimizing $\alpha$, $\beta$, and the number of auxiliary variables.

However, when we concatenate gadget (1) with the gadget in Figure 2 to obtain
a reduction from kSAT to Max2XOR, for $k\geq 4$, we get a
$(2(k-2),\,3(k-2))$-gadget with $2k-5$ auxiliary variables and $\Delta E=2$.
This one is not optimal, in the sense that, as we will see below, there exist
other gadgets that introduce fewer variables with the same $\Delta E$, and
smaller $\alpha$ and $\beta$ parameters.

In our experience, in general, if we concatenate two gadgets, even if both are
optimal (in some parameter), the resulting gadget can be suboptimal (in that
parameter). Therefore, it is usually better to compute _direct_ gadgets. In
the following, we describe direct and better reductions (for some of the
parameters) from SAT to Max2XOR.

###  4.2 A Regular-Like Gadget

Here, we present a new gadget inspired by the Refined-Regular gadget from SAT
to Max2SAT introduced in Ansótegui and Levy (2021). The reduction is based on
a function $T^{0}$ that takes as parameters a SAT clause and a variable. The
use of this variable is for technical reasons, to make simpler the recursive
definition and proof of Lemma 5. Later (see Theorem 6), it will be replaced by
the constant one.

######  Definition 4.

Given a SAT clause $x_{1}\vee\cdots\vee x_{k}$ and an auxiliary variable $b$,
define the Max2XOR problem $T^{0}(x_{1}\vee\cdots\vee x_{k},b)$ recursively as
follows:

$T^{0}(x_{1}\vee x_{2},b)=\left\\{\begin{array}[]{l}{}_{(1/2)}\,x_{1}\oplus
x_{2}=1\\\ {}_{(1/2)}\,x_{1}\oplus b=0\\\ {}_{(1/2)}\,b\oplus
x_{2}=0\end{array}\right.$

for binary clauses, and

$T^{0}(x_{1}\vee\cdots\vee x_{k},b)=T^{0}(x_{1}\vee\cdots\vee
x_{k-1},b^{\prime})\cup\left\\{\begin{array}[]{l}{}_{(1/2)}\,b^{\prime}\oplus
x_{k}=1\\\ {}_{(1/2)}\,b^{\prime}\oplus b=0\\\ {}_{(1/2)}\,b\oplus
x_{k}=0\end{array}\right.$

for $k\geq 3$.

$x_{1}$$b_{1}$$x_{2}$$b_{2}$$x_{3}$$b_{k-2}$$b_{k-1}$$x_{k}$$\cdots$ Figure 3:
Graphical representation of $T^{0}(x_{1}\vee\cdots\vee x_{k},b_{k-1})$.

######  Lemma 5.

Consider the Max2XOR problem $T^{0}(x_{1}\vee\cdots\vee x_{k},b_{k-1})$. We
have:

  1. 1.

For any assignment $I:\\{x_{1},\dots,x_{k}\\}\to\\{0,1\\}$, the extension of
the assignment as $I^{\prime}(b_{i})=I(x_{i+1})$, for $i=1,\dots,k-1$,
maximizes the number of satisfied 2XOR constraints, that is $2\,(k-1)$.

  2. 2.

For any assignment $I:\\{x_{1},\dots,x_{k},b_{k-1}\\}\to\\{0,1\\}$ satisfying
$I(b_{k-1})=1$, the extension of the assignment as

$I^{\prime}(b_{i})=\left\\{\begin{array}[]{ll}1&\mbox{if
$I(x_{i+2})=\cdots=I(x_{k})=0$}\\\\[5.69054pt]
I(x_{i+1})&\mbox{otherwise}\end{array}\right.$

for $i=1,\dots,k-2$, maximizes the number of satisfied 2XOR constraints, that
is $2\,(k-2)$, if $I(x_{1})=\cdots=I(x_{k})=0$, or $2\,(k-1)$ otherwise.

###### Proof.

See Lemma 8, where a more general result is proved. ∎

######  Theorem 6.

The translation of every clause $x_{1}\vee\cdots\vee x_{k}$ into
$T^{0}(x_{1}\vee\cdots\vee x_{k},\hat{1})$ defines a $(k-1,3/2(k-1))$-gadget
from kSAT to Max2XOR that introduces $k-2$ auxiliary variables and has $\Delta
E=2$.

###### Proof.

The soundness of the reduction is based on the second statement of Lemma 5.
Assume that we force the variable $\hat{1}$ to be interpreted as one, i.e.
$I(\hat{1})=1$, or that, alternatively, we simply replace it by the constant
$1$. Any assignment satisfying the clause can extend to satisfy at least
$2(k-1)$ 2XOR constraints from $T^{0}(x_{1}\vee\cdots\vee x_{k},\hat{1})$,
with a total weight equal to $k-1$. Any assignment falsifying it can only be
extended to satisfy at most $2(k-2)$ 2XOR constraints, with a total weight
$k-2$. Hence, $\alpha=k-1$. The number of 2XOR constraints is $3(k-1)$, all of
them with weight $1/2$. Therefore, $\beta=3/2(k-1)$. ∎

###  4.3 A Tree-Like Gadget

In this section, we describe the Tree-like gadget, which is a generalization
of the Regular-like gadget. Before describing the new gadget, we introduce an
example for the clause $x_{1}\vee\cdots\vee x_{7}$, in Figure 4.

$x_{1}$$x_{2}$$x_{3}$$x_{4}$$x_{5}$$x_{6}$$x_{7}$$b_{1}$$b_{2}$$b_{3}$$b_{4}$$b_{5}$$\hat{1}$
Figure 4: A graphical representation of a Tree-like gadget for 7SAT. All
constraints have weight $1/2$.

######  Definition 7.

Given a clause $x_{1}\vee\cdots\vee x_{k}$ and an auxiliary variable $b$,
define the Max2XOR problem $T^{t}(x_{1}\vee\cdots\vee x_{k},b)$ recursively
and non-deterministically as follows:

$T^{t}(x_{1}\vee\cdots\vee x_{k},\ b)=\left\\{\begin{tabular}[]{l@{\
}r}$\\{x_{1}\oplus x_{2}=1,x_{1}\oplus b=0,x_{2}\oplus b=0\\}$&if
$k=2$\\\\[8.53581pt] $\begin{array}[t]{l}T^{t}(x_{1}\vee\cdots\vee x_{k-1},\
b^{\prime})\ \cup\\\ \\{b^{\prime}\oplus x_{k}=1,b^{\prime}\oplus
b=0,x_{k}\oplus b=0\\}\par\end{array}$&if $k\geq 3$\\\\[19.91692pt]
$\begin{array}[t]{l}T^{t}(x_{2}\vee\cdots\vee x_{k},\ b^{\prime})\ \cup\\\
\\{b^{\prime}\oplus x_{1}=1,b^{\prime}\oplus b=0,x_{1}\oplus
b=0\\}\end{array}$&if $k\geq 3$\\\\[19.91692pt] $\begin{array}[t]{l}\
T^{t}(x_{1}\vee\cdots\vee x_{r},\ b^{\prime})\ \cup\\\ \
T^{t}(x_{r+1}\vee\cdots\vee x_{k},\ b^{\prime\prime})\ \cup\\\
\\{b^{\prime}\oplus b^{\prime\prime}=1,b^{\prime}\oplus
b=0,b^{\prime\prime}\oplus b=0\\}\end{array}$&\begin{tabular}[t]{l}if $k\geq
4$, where\\\ $2\leq r\leq k-2$\end{tabular}\end{tabular}\right.$

where all XOR constraints have weight $1/2$.

Notice that the definition of $T^{t}$ is not deterministic. When $k=3$ we have
two possible translations (applying the second or third case), and when $k\geq
4$ we can apply the second, third, and fourth cases, with distinct values of
$r$, getting as many possible translations as possible binary trees with $k$
leaves.

Notice also that the definition of $T^{0}$ corresponds to the definition of
$T^{t}$ where we only apply the first and second cases. Therefore, $T^{t}$ is
a generalization of $T^{0}$.

######  Lemma 8.

Consider the set of 2XOR constraints of $T^{t}(x_{1}\vee\cdots\vee x_{k},b)$
without weights. We have:

  1. 1.

There are $3(k-1)$ constraints.

  2. 2.

Any assignment satisfies at most $2(k-1)$ of them.

  3. 3.

Any assignment $I:\\{x_{1},\dots,x_{k}\\}\to\\{0,1\\}$ can be extended to an
optimal assignment satisfying $I(b)=I(x_{1}\vee\cdots\vee x_{k})$ and $2(k-1)$
constraints.

  4. 4.

Any assignment $I$ satisfying $I(x_{1}\vee\cdots\vee x_{k})=0$ and $I(b)=1$
can be extended to an optimal assignment satisfying $2(k-2)$ constraints.

###### Proof.

The first statement is trivial.

For the second, notice that for, each one of the $k-1$ _triangles_ of the form
$\\{a\oplus b=1,a\oplus c=0,b\oplus c=0\\}$, any assignment can satisfy at
most two of the constraints of each triangle.

The third statement is proved by induction. The base case, for binary clauses,
is trivial. For the induction case, if we apply the second or third options of
the definition of $T$, the proof is similar to Lemma 5. In the fourth case,
assume by induction that there is an assignment extending
$I:\\{x_{1},\dots,x_{r}\\}\to\\{0,1\\}$ that verifies
$I(b^{\prime})=I(x_{1}\vee\cdots\vee x_{r})$ and satisfies $2(r-2)$
constraints of $T^{t}(x_{1}\vee\cdots\vee x_{r},b^{\prime})$. Similarly, there
is an assignment extending $I:\\{x_{r+1},\dots,x_{k}\\}\to\\{0,1\\}$ that
verifies $I(b^{\prime\prime})=I(x_{r+1}\vee\cdots\vee x_{k})$ and satisfies
$2((k-r)-2)$ constraints of $T^{t}(x_{r+1}\vee\cdots\vee
x_{k},b^{\prime\prime})$. Both assignments do not share variables, therefore,
they can be combined into a single assignment. This assignment can be extended
with $I(b)=b^{\prime}\vee b^{\prime\prime}$. This ensures that it will satisfy
two of the constraints from $\\{b^{\prime}\oplus
b^{\prime\prime}=1,b^{\prime}\oplus b=0,b^{\prime\prime}\oplus b=0\\}$.
Therefore, it verifies $I(b)=I(x_{1}\vee\cdots\vee x_{k})$ and satisfies
$2(r-2)+2((k-r)-2)+2=2(k-1)$ constraints of $T^{t}(x_{1}\vee\cdots\vee
x_{k},b)$. Since this is the maximal number of constraints we can satisfy,
this assignment is optimal.

The fourth statement is also proved by induction. The base case, for binary
clauses, is trivial. For the induction case, consider only the application of
the fourth case of the definition of $T$ (the other cases are quite similar).
We have to consider 3 possibilities:

If we extend $I(b^{\prime})=I(b^{\prime\prime})=1$, by induction, we can
extend $I$ to satisfy $2(r-2)$ constraints of $T^{t}(x_{1}\vee\cdots\vee
x_{r},b^{\prime})$ and $2((k-r)-2)$ constraints of
$T^{t}(x_{r+1}\vee\cdots\vee x_{k},b^{\prime\prime})$. It satisfies $2$
constraints from $\\{b^{\prime}\oplus b^{\prime\prime}=1,b^{\prime}\oplus
b=0,b^{\prime\prime}\oplus b=0\\}$, hence a total of $2(k-3)$ constraints.

If we extend $I(b^{\prime})=I(b^{\prime\prime})=0$, by the third statement of
this lemma, we can extend $I$ to satisfy $2(r-1)$ constraints of
$T^{t}(x_{1}\vee\cdots\vee x_{r},b^{\prime})$ and $2((k-r)-1)$ constraints of
$T^{t}(x_{r+1}\vee\cdots\vee x_{k},b^{\prime\prime})$. It does not satisfy any
constraints from $\\{b^{\prime}\oplus b^{\prime\prime}=1,b^{\prime}\oplus
b=0,b^{\prime\prime}\oplus b=0\\}$, hence a total of $2(k-2)$ constraints.

Finally, If we extend $I(b^{\prime})=1$ and $I(b^{\prime\prime})=0$ (or vice
versa), by induction, we can extend $I$ to satisfy $2(r-2)$ constraints of
$T^{t}(x_{1}\vee\cdots\vee x_{r},b^{\prime})$ and by the third statement
$2((k-r)-2)$ constraints of $T^{t}(x_{r+1}\vee\cdots\vee
x_{k},b^{\prime\prime})$. It also satisfy $2$ constraints from
$\\{b^{\prime}\oplus b^{\prime\prime}=1,b^{\prime}\oplus
b=0,b^{\prime\prime}\oplus b=0\\}$, hence a total of $2(k-2)$ constraints. ∎

######  Theorem 9.

The translation of every clause $x_{1}\vee\cdots\vee x_{k}$ into
$T^{t}(x_{1}\vee\cdots\vee x_{k},\hat{1})$ defines a $(k-1,3/2(k-1))$-gadget
from kSAT to Max2XOR that introduces $k-2$ auxiliary variables, with $\Delta
E=2$.

###### Proof.

The theorem is a direct consequence of the two last statements of Lemma 8. ∎

If we compare Theorems 6 and 9, we observe that both establish the same values
for $\alpha=k-1$ and $\beta=3/2(k-1)$ in the $(\alpha,\beta)$-gadget, and both
introduce the same number $(k-2)$ of auxiliary variables. Therefore, a priory,
the parallel translation is a generalization of the sequential translation,
but it does not have a clear (theoretical) advantage.

However, in the context of quantum annealers, we recall that not all possible
couplings are allowed, only the ones in the graph defined by the architecture.
To circumvent this issue the typical approach is to make _copies_ (using extra
qubits) of the variables involved in the Max2XOR constraint whose coupling is
not allowed. In other words, if we have a constraint ${}_{(w)}\,x_{i}\oplus
x_{j}=1$ in the Max2XOR problem, but $(i,j)\not\in E$, we have to find a path
and replace the constraint by $\\{_{(1)}\,x_{i}\oplus
x_{k_{1}}=0,\dots,_{(1)}\,x_{k_{r-1}}\oplus x_{r}=0,_{(w)}\,x_{r}\oplus
x_{j}=1\\}$

In this sense, the more _flexible_ structure of the parallel translation can
help to fit more easily (i.e. with fewer extra qubits) the Max2XOR constraints
generated by the gadget into the architecture of the quantum annealer.

$\cdots$$\hat{1}$$x_{1}$$x_{5}$$b_{1}$$b_{2}$$1/2$$5/6$$5/6$$2/3$$2/3$$5/6$$1/2$$1/2$$2/3$$5/6$

$\begin{array}[b]{l}{}_{(1/2)}\,x_{i}=1\\\ {}_{(2/3)}\,b_{1}=1\\\
{}_{(5/6)}\,b_{2}=1\\\ {}_{(1/2)}\,x_{i}\oplus x_{j}=1\\\
{}_{(5/6)}\,x_{i}\oplus b_{1}=1\\\ {}_{(2/3)}\,x_{i}\oplus b_{2}=1\\\
{}_{(5/6)}\,b_{1}\oplus b_{2}=1\\\\[5.69054pt] \mbox{where $i,j=1,\dots,5$}\\\
\mbox{and $i\neq j$}\end{array}$

Figure 5: Graphic representation of the clique-like $(10,52/3)$-gadget from
5SAT to Max2XOR, with $\Delta E=6/5$, and optimal number of $2$ auxiliary
variables.

###  4.4 A Clique-Like Gadget

The previous gadgets have an energy gap $\Delta E=2$, but they are not optimal
with respect to the number of auxiliary variables. We can obtain gadgets that
only require $\mathcal{O}(\log k)$ auxiliary variables, on expenses of
decreasing the energy gap and increasing the density of constraints.
Therefore, there is a trade-off between optimizing the energy gap and the
number of auxiliary variables.

######  Definition 10.

Given a clause $x_{1}\vee\cdots\vee x_{k}$, where $k$ is a power of $2$,
define the Max2XOR problem $T^{c}(x_{1}\vee\cdots\vee x_{k})$ as follows:

$T^{c}(x_{1}\vee\cdots\vee
x_{k})=\left\\{\begin{array}[]{l@{\hspace{5mm}}l}{}_{(1/2)}\,x_{i}=1\hfil\hskip
14.22636pt&i=1,\dots,k\\\ {}_{(2^{j-1})}\,b_{j}=1\hfil\hskip
14.22636pt&j=1,\dots,\log k-1\\\ {}_{(1/2)}\,x_{i}\oplus x_{j}=1\hfil\hskip
14.22636pt&1\leq i<j\leq k\\\ {}_{(2^{i+j-1})}\,b_{i}\oplus b_{j}=1\hfil\hskip
14.22636pt&1\leq i<j\leq\log k-1\\\ {}_{(2^{j-1})}\,x_{i}\oplus
b_{j}=1\hfil\hskip 14.22636pt&i=1,\dots,k\\\ \hfil\hskip
14.22636pt&j=1,\dots,\log k-1\\\ \end{array}\right.$

######  Theorem 11.

The transformation of every clause $x_{1}\vee\cdots\vee x_{k}$ into
$T^{c}(x_{1}\vee\cdots\vee x_{k})$ defines a $(\alpha,\beta)$-gadget from kSAT
to Max2XOR that introduces $\log k-1$ auxiliary variables, with

$\begin{array}[]{l}\displaystyle\alpha=\frac{1}{2}\,k\,(k-1)\\\\[5.69054pt]
\displaystyle\beta=\frac{11\,k^{2}-15\,k+4}{12}\\\\[5.69054pt]
\displaystyle\Delta E=16\,k^{-2}\end{array}$

###### Proof.

The intuition for the construction of the gadget is: apart from the variables
$x_{i}$ (with weight $1$), we add auxiliary variables $b_{j}$ with weight
$2^{j}$ and a constant $\hat{0}$ with weight $1$. The sum of all weights is
$2k-1$. The weight of every constraint $x\oplus y=1$ is equal to one-half of
the weight of $x$ by the weight of $y$. No matter how $x$’s are assigned, if
at least one is assigned to one, we can assign the $b$’s such that the weight
of variables assigned to one is $k$ and the weight of the assigned to zero is
$k-1$, or vice versa. This maximizes the weight of satisfied assignments that
is $k(k-1)/2=\alpha$. Conversely, if all $x$’s are assigned to zero, the best
we can do is assign all $b$’s to one, which results in weight
$(k+1)(k-2)/2=\alpha-1$ for the satisfied constraints.

More formally, let $I$ be an assignment satisfying $x_{1}\vee\cdots\vee
x_{k}$. Let $r=\sum_{i=1}^{k}I(x_{i})\in[1,k]$. We extend $I$ such that
$I(b_{i})$ is the $i$th bit of the binary representation of the number $k-r$.
Therefore, $\sum_{i=1}^{\log k-1}I(b_{i})\,2^{i}$ is either $k-r$ or $k-r-1$.
And the sum of weights of variables assigned to one,
$w_{1}\stackrel{{\scriptstyle def}}{{=}}\sum_{i=1}^{\log
k-1}I(b_{i})\,2^{i}+\sum_{i=1}^{k}x_{i}$ is either $k$ or $k-1$. For the ones
assigned to zero (including $\hat{0}$) we have $w_{0}\stackrel{{\scriptstyle
def}}{{=}}\sum_{i=1}^{\log
k-1}(1-I(b_{i}))\,2^{i}+\sum_{i=1}^{k}(1-I(x_{i}))+1=2k-1-w_{1}$. Therefore,
the sum of satisfied constraints is $w_{1}\,w_{0}/2=k(k-1)/2$.

If $I$ falsifies the clause, we can set $I(b_{i})=1$ and get
$w_{1}=\sum_{i=1}^{\log k-1}2^{i}=k-2$ and $w_{0}=k+1$. In this case, we get
satisfied constraints for a total weight $(k+1)(k-2)/2=k(k-1)/2-1$. ∎

When $k$ is not a power of $2$, the gadget with a minimal number of auxiliary
variables is not straightforward to generalize. In Figure 5, we represent the
gadget for $k=5$ with $2$ auxiliary variables.

##  5 Computing Gadgets Automatically

As in Ansótegui and Levy (2021), we have created a Mixed Integer Programming
model to compute automatically gadgets from SAT to Max2XOR with the MIP solver
Gurobi.

Given a $k$SAT clause and a set of new auxiliary variables $b_{j}$ the MIP
program explores the subsets of weighted XOR clauses of length at most 2 that
can be constructed with the $k$ input variables and the $b_{j}$ variables. The
weights of the XOR clauses are represented with continuous variables in the
interval $[0,1]$.

The MIP model incorporates constraints to ensure that the selected subset of
XOR clauses fulfils the definition of a $(\alpha,\beta)$-gadget, and the
objective function maximizes the energy gap $\Delta E$. The MIP model is
solved to optimality.

In the following table, we report the $\alpha$, $\beta$ and $\Delta E$ values
found with the MIP program for some combinations of $k$ and number of
auxiliary variables:

| Number of aux. vars.
---|---
| 1 | 2 | 3
k=3 | $\begin{array}[]{l}\alpha=2\\\ \beta=3\\\ \Delta E=2\end{array}$ |  |
k=4 | $\begin{array}[]{l}\alpha=6\\\ \beta=10\\\ \Delta E=1\end{array}$ | $\begin{array}[]{l}\alpha=3\\\ \beta=9/2\\\ \Delta E=2\end{array}$ |
k=5 | - | $\begin{array}[]{l}\alpha=10\\\ \beta=52/3\\\ \Delta E=6/5\end{array}$ | $\begin{array}[]{l}\alpha=4\\\ \beta=6\\\ \Delta E=2\end{array}$

As we can see, the gadgets found by the MIP program presented in the diagonal
of the table have the same values as the Tree-like gadget, while the gadgets
under the diagonal have the same values as the Clique-like gadget, certifying
that, for small values of $k$, they are optimal respect to the energy gap and
the number of auxiliary variables, respectively.

##  6 Conclusions

Quantum annealers _may_ offer in the future an alternative to solve the SAT
problem more efficiently. To take maximum advantage of this new computation
architecture, we need to take into account several aspects, such as the number
of qubits that needs our reformulation of the SAT problem, the energy gap, and
how adaptable is our encoding to the graph describing the allowed couplings of
the qubits in the quantum annealer (what may incur into the use of additional
auxiliary variables).

Tree-like gadgets help us to maximize the energy gap using a linear number of
auxiliary variables and are rather _flexible_ to adapt them efficiently to
different graph architectures. On the other hand, Clique-like gadgets require
a logarithmic number of auxiliary variables, (i.e. fewer qubits), but with a
lower energy gap, and may use additional qubits to accommodate the dense
structure of the gadget to the architecture of the quantum annealer.

## Acknowledgements

This work was supported by MCIN/AEI/10.13039/501100011033 (Grant:
PID2019-109137GB-C21).

## References

  * Mehta et al. (2022) V. Mehta, F. Jin, H. De Raedt, K. Michielsen,  Quantum annealing for hard 2-satisfiability problems: Distribution and scaling of minimum energy gap and success probability,  Phys. Rev. A 105 (2022) 062406. URL: https://link.aps.org/doi/10.1103/PhysRevA.105.062406. doi:10.1103/PhysRevA.105.062406.
  * Li (2000a) C. M. Li,  Integrating equivalency reasoning into Davis-Putnam procedure,  in: H. A. Kautz, B. W. Porter (Eds.), Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30 - August 3, 2000, Austin, Texas, USA, AAAI Press / The MIT Press, 2000a, pp. 291–296.
  * Li (2000b) C. M. Li,  Equivalency reasoning to solve a class of hard SAT problems,  Inf. Process. Lett. 76 (2000b) 75–81. doi:10.1016/S0020-0190(00)00126-5.
  * Baumgartner and Massacci (2000) P. Baumgartner, F. Massacci,  The taming of the (X)OR,  in: J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, P. J. Stuckey (Eds.), Computational Logic - CL 2000, First International Conference, London, UK, 24-28 July, 2000, Proceedings, volume 1861 of Lecture Notes in Computer Science, Springer, 2000, pp. 508–522. doi:10.1007/3-540-44957-4\\_34.
  * Li (2003) C. M. Li,  Equivalent literal propagation in the DLL procedure,  Discret. Appl. Math. 130 (2003) 251–276. doi:10.1016/S0166-218X(02)00407-9.
  * Heule and van Maaren (2004) M. Heule, H. van Maaren,  Aligning CNF- and equivalence-reasoning,  in: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004.
  * Heule et al. (2004) M. Heule, M. Dufour, J. van Zwieten, H. van Maaren,  March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver,  in: H. H. Hoos, D. G. Mitchell (Eds.), Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers, volume 3542 of Lecture Notes in Computer Science, Springer, 2004, pp. 345–359. doi:10.1007/11527695\\_26.
  * Chen (2009) J. Chen,  Building a hybrid SAT solver via conflict-driven, look-ahead and XOR reasoning techniques,  in: O. Kullmann (Ed.), Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, Springer, 2009, pp. 298–311. doi:10.1007/978-3-642-02777-2\\_29.
  * Soos et al. (2009) M. Soos, K. Nohl, C. Castelluccia,  Extending SAT solvers to cryptographic problems,  in: O. Kullmann (Ed.), Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, Springer, 2009, pp. 244–257. doi:10.1007/978-3-642-02777-2\\_24.
  * Laitinen et al. (2012) T. Laitinen, T. A. Junttila, I. Niemelä,  Conflict-driven XOR-clause learning,  in: A. Cimatti, R. Sebastiani (Eds.), Theory and Applications of Satisfiability Testing \- SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012\. Proceedings, volume 7317 of Lecture Notes in Computer Science, Springer, 2012, pp. 383–396. doi:10.1007/978-3-642-31612-8\\_29.
  * Soos (2010) M. Soos,  Enhanced gaussian elimination in DPLL-based SAT solvers,  in: D. L. Berre (Ed.), POS-10. Pragmatics of SAT, Edinburgh, UK, July 10, 2010, volume 8 of EPiC Series in Computing, EasyChair, 2010, pp. 2–14.
  * Laitinen et al. (2011) T. Laitinen, T. A. Junttila, I. Niemelä,  Equivalence class based parity reasoning with DPLL(XOR),  in: IEEE 23rd International Conference on Tools with Artificial Intelligence, ICTAI 2011, Boca Raton, FL, USA, November 7-9, 2011, IEEE Computer Society, 2011, pp. 649–658. doi:10.1109/ICTAI.2011.103.
  * Laitinen et al. (2012) T. Laitinen, T. A. Junttila, I. Niemelä,  Extending clause learning SAT solvers with complete parity reasoning,  in: IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9, 2012, IEEE Computer Society, 2012, pp. 65–72. doi:10.1109/ICTAI.2012.18.
  * Soos and Meel (2019) M. Soos, K. S. Meel,  BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting,  in: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, AAAI Press, 2019, pp. 1592–1599. doi:10.1609/aaai.v33i01.33011592.
  * Trevisan et al. (2000) L. Trevisan, G. B. Sorkin, M. Sudan, D. P. Williamson,  Gadgets, approximation, and linear programming,  SIAM J. Comput. 29 (2000) 2074–2097.
  * Ansótegui and Levy (2021) C. Ansótegui, J. Levy,  Reducing SAT to Max2SAT,  in: Z. Zhou (Ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, ijcai.org, 2021, pp. 1367–1373.
  * Bonet et al. (2007) M. L. Bonet, J. Levy, F. Manyà,  Resolution for Max-SAT,  Artif. Intell. 171 (2007) 606–618. doi:10.1016/j.artint.2007.03.001.
  * Santra et al. (2014) S. Santra, G. Quiroz, G. V. Steeg, D. A. Lidar,  Max 2-SAT with up to 108 qubits,  New Journal of Physics 16 (2014) 045006. doi:10.1088/1367-2630/16/4/045006.
  * Douglass et al. (2015) A. Douglass, A. D. King, J. Raymond,  Constructing SAT filters with a quantum annealer,  in: M. Heule, S. Weaver (Eds.), Theory and Applications of Satisfiability Testing – SAT 2015, Springer, 2015, pp. 104–120.
  * Bian et al. (2017) Z. Bian, F. A. Chudak, W. G. Macready, A. Roy, R. Sebastiani, S. Varotti,  Solving SAT and MaxSAT with a quantum annealer: Foundations and a preliminary report,  in: C. Dixon, M. Finger (Eds.), Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings, volume 10483 of Lecture Notes in Computer Science, Springer, 2017, pp. 153–171. doi:10.1007/978-3-319-66167-4\\_9.
  * Bian et al. (2020) Z. Bian, F. A. Chudak, W. G. Macready, A. Roy, R. Sebastiani, S. Varotti,  Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results,  Inf. Comput. 275 (2020) 104609. doi:10.1016/j.ic.2020.104609.
  * Choi (2010) V. Choi,  Minor-embedding in adiabatic quantum computation: II. minor-universal graph design,  Quantum Information Processing 10 (2010) 343–353. doi:10.1007/s11128-010-0200-3.
  * Bian et al. (2014) Z. Bian, F. Chudak, R. Israel, B. Lackey, W. G. Macready, A. Roy,  Discrete optimization using quantum annealing on sparse ising models,  Frontiers in Physics 2 (2014). doi:10.3389/fphy.2014.00056.