[Link].

(2024) 18:20
[Link] Mathematics in Computer Science

SAT Solving Using XOR-OR-AND Normal Forms

Bernhard Andraschko · Julian Danner ·
Martin Kreuzer

Received: 26 October 2023 / Revised: 14 August 2024 / Accepted: 5 September 2024 / Published online: 24 October 2024
© The Author(s) 2024

Abstract This paper introduces the XOR-OR-AND normal form (XNF) for logical formulas. It is a generalization
of the well-known Conjunctive Normal Form (CNF) where literals are replaced by XORs of literals. As a first
theoretic result, we show that every CNF formula is equisatisfiable to a formula in 2-XNF, i.e., a formula in XNF
where each clause involves at most two XORs of literals. Subsequently, we present an algorithm which converts
Boolean polynomials efficiently from their Algebraic Normal Form (ANF) to formulas in 2-XNF. Experiments with
the cipher ASCON-128 show that cryptographic problems, which by design are based strongly on XOR-operations,
can be represented using far fewer variables and clauses in 2-XNF than in CNF. In order to take advantage of
this compact representation, new SAT solvers based on input formulas in 2-XNF need to be designed. By taking
inspiration from graph-based 2-CNF SAT solving, we devise a new DPLL-based SAT solver for formulas in 2-
XNF. Among others, we present advanced pre- and in-processing techniques. Finally, we give timings for random
2-XNF instances and instances related to key recovery attacks on round reduced ASCON-128, where our solver
outperforms state-of-the-art alternative solving approaches.

Keywords SAT solving · XOR constraint · Algebraic normal form · Implication graph · Cryptographic attack

Mathematics Subject Classification 03B70 · 13P15 · 05C90 · 94A60

1 Introduction

SAT solvers are programs which decide the Boolean Satisfiability Problem for propositional logic formulas. In the
last decades there has been a substantial effort to improve their performance, and they have grown into versatile
tools for tackling computational problems in various domains such as automatic theorem proving, graph theory,
hardware verification, artificial intelligence, and cryptanalysis.

B. Andraschko · J. Danner (B)· M. Kreuzer

Fakultät für Informatik und Mathematik, Universität Passau, 94030 Passau, Germany
e-mail: [Link]@[Link]
B. Andraschko
e-mail: [Link]@[Link]
M. Kreuzer
e-mail: [Link]@[Link]
20 Page 2 of 26 B. Andraschko et al.

Especially problems from the latter domain have been shown to be hard for conventional SAT solvers that take
a conjunctive normal form (CNF) as input. Although many new attacks on cryptosystems and other cryptographic
protocols have been designed based on the idea of encoding the computational problem as an instance for CNF-
based SAT solvers (see for instance [20,23,29,31,33,34]), many problems are still out of range (e.g., see [14,20]).
This can be mainly attributed to the fact that cryptographic primitives are often built using exclusive disjunctions
(XORs) of variables which lead to an exponential blow-up when encoded in CNF.
To speed up the performance of SAT solvers for such instances, one can either try to modify the problem
encodings such that they lead to smaller instances [11,28,29], or one can try to improve the solving strategy
altogether. For example, the latter approach has been pursued by attempts to integrate support for XOR constraints
on the input variables [24,36,39,41] or by combining logical SAT solving with algebraic reasoning [11,26]. While
purely algebraic solving techniques (as developed for instance in [9,12,13]) have had some success in cryptanalysis
[4,10,14], a very promising line of research seems to be to combine logic and algebraic solving paradigms.
One such attempt was initiated in [27] and refined in [26], where a new proof system called s-Res was introduced.
Its input are products of linear Boolean polynomials, or, in the language of logic, disjunctions of XORs of literals.
Thus the s-Res proof system is innately suitable for dealing with cryptanalytic instances, as these tend to be rich
in XOR connectives. The core inference rule of s-Res is called s-resolution. It is both a generalization of the
classical resolution rule of propositional logic and of Buchberger’s S-polynomials which form the basis of Gröbner
basis computations [30]. In [26,27] initial DPLL-based refutation methods utilizing s-resolvents were introduced.
As of today, no highly efficient implementation of these algorithms exists, and procedures to use s-Res for finding
satisfying assignments are lacking as well.
In the first part of this paper we strive to develop efficient methods for converting propositional logic formulas
to suitable inputs for s-Res type proof systems. After recalling some basic definitions and properties of the
ring of Boolean polynomials in Sect. 2, we introduce and study a new XOR-based normal form in Sect. 3. More
precisely, the new normal form is called the XOR-OR-AND normal form (XNF) for propositional logic formulas
(see Definition 3.2). It generalizes the CNF by replacing the literals with XORs of literals which we simply call
linerals. From an algebraic perspective, a lineral corresponds to a linear Boolean polynomial, and a disjunction of
linerals corresponds to a product of linear Boolean polynomials. Using this identification, one sees that formulas in
XNF occur naturally in the proof system s-Res. Since XNF generalizes CNF, it is clear that every propositional
logic formula is equivalent to one in XNF.
While conversions from the algebraic normal form (ANF) of a Boolean polynomial to the CNF of the correspond-
ing propositional logic formula and back have been studied carefully (see for instance [11,28,29]), conversions
to systems offering some native support for XOR have been introduced only sparingly and elaborated much less
systematically [32,36,39].
It is well-known that one can introduce new variables and convert every Boolean polynomial system to one
involving only polynomials of degree at most two. Here we show that, in fact, every XNF formula is equisatisfiable
to one in 2-XNF, i.e., to an instance of XNF where each clause involves at most two linerals (see Proposition 3.7).
Algebraically speaking, systems of quadratic Boolean polynomial equations can be transformed to systems con-
sisting of products of at most two linear polynomials. Furthermore, we try to optimize this transformation by
introducing as few additional variables as possible (see Propositions 3.15 and 3.17). To illustrate the potential of the
conversion to 2-XNF, we apply it to instances related to algebraic attacks on the cipher Ascon-128 [18] which
was recently selected for standardization by NIST for lightweight cryptography. We get 2-XNF representations
which are substantially more compact than state-of-the-art representations in CNF (see Example 3.22).
In the second part of the paper we make use of this 2-XNF representation and take the first few steps towards
translating the foundations of efficient CNF-based SAT solving to XNF-based SAT solving. In particular, using
ideas based on efficient 2-CNF solvers and CNF pre-processing [5,25], we develop a graph based 2-XNF solver. To
start with, we define an implication graph structure (IGS) (L , V, E) for a given formula F which consists of a set L
of linear Boolean polynomials known to be in the ideal I F , which is the algebraic representation of F, and a directed
graph (V, E) whose edges ( f, g) mean that f ∈ I F implies g ∈ I F (see Definition 4.1 and Remark 4.2). Our solving
algorithm then starts with a trivial IGS for F (see Remark 4.4) and simplifies it using a suitable ordering on the IGSs
SAT Solving Using XOR-OR-AND Normal Forms Page 3 of 26 20

(see Definition 4.6). Then we gradually improve the IGS by propagation, in-processing and guessing until we arrive
at an implication graph structure with an empty graph, i.e., a case where the corresponding ideal is generated by
linear polynomials. Given that the guesses were correct, a satisfying assignment for F can be deduced immediately
from a solution of the corresponding system of linear equations. The improvement of an IGS is measured in terms
of the size of the linear part L and in the size of the graph (V, E).
Propagation is achieved using a generalization of the classical Boolean Constraint Propagation which we call
Gaußian Constraint Propagation (see Proposition 4.8). Two pre-processing methods are examined which yield new
linear forms or new edges for the IGS (see Proposition 4.10). Unfortunately, they are too expensive to be executed
repeatedly during the main solving procedure. For such in-processing methods, we provide two more efficient
suggestions. Firstly, using the calculation of strongly connected components of (V, E), we are able to reach an
acyclic graph (see Proposition 4.13). Secondly, we introduce the notion of failed linerals (see Definition 4.14) and
apply them in order to learn new linear polynomials in I F (see Proposition 4.17).
Several heuristics for producing good decisions for an IGS, i.e., for making good guesses (see Definition 4.20) are
discussed next. Moreover, we offer some suggestions how to implement these heuristics efficiently (see Remarks 4.22
and 4.23). Finally, we combine everything and present our new graph-based 2-XNF solver (see Proposition 4.24)
together with suggestions how to implement it well using suitable data structures (see Remark 4.25).
The last section contains the results of some experiments and comparisons to established CNF-based SAT
solvers, especially ones that offer some support for XOR constraints. Usually, they allow separate XOR constraints
on variables in addition to a CNF, a type of input that is known as CNF-XOR. One of the first solvers for such
formulas was described in [38,39] and is implemented in CryptoMiniSat. Another one is xnfSAT [36] which
uses stochastic local search methods for CNF-XOR inputs. The solver Bosphorus allows ANF and CNF inputs,
but no CNF-XOR inputs [11]. Moreover, we compare our method with the winner of the 2023 SAT competition
SBVA-CaDiCaL [22] which admits CNF formulas.
In our experiments we compare the new 2-XNF solver, called 2-Xornado, using the three decision heuristics
explained in Sect. 4 to the CNF-XOR solvers CryptoMiniSat and xnfSAT, to the algebraic solver PolyBoRi
[9], to a brute force XNF solver xnf_ bf, and to the CNF solver SBVA-CaDiCaL. We created timings for two
types of inputs. The first type are random 2-XNF instances. It turns out that our graph based 2-XNF solver involving
merely some basic DPLL techniques outperforms state-of-the-art solving approaches on small random instances,
both for satisfiable and unsatisfiable cases (see Fig. 4a, b).
The second type of experiments was to try the solvers on key recovery attacks for round reduced versions of the
Ascon-128 cryptosystem. This lightweight cipher was recently selected for standardization by NIST. Again it
turns out that, even with our very simple decision heuristics, the graph based 2-XNF solver performs surprisingly
well (see Fig. 5). Here it may be worthwhile to note that some of these round reduced key recovery attacks can
be solved already in the pre-processing phase. Altogether, one main advantage of XNF solving is that the more
compact problem representations require fewer decisions, and this leads to meaningful speed-ups. Finally, let us
point out that the desirable extension of XNF solving to include CDCL techniques [35] is not straightforward and
will require non-trivial new tools.
Due to its simpler description, we chiefly use the algebraic point of view when we work with formulas in XNF,
i.e., we regard them as products of linear Boolean polynomials. Unless explicitly noted otherwise, we use the
definitions and notation introduced in [28] and [30]. The algorithms of Sect. 3 were implemented by B. Andraschko
and the solving methods of Sect. 4 by J. Danner. All source code is available at [Link]
sat_solving.

2 The Ring of Boolean Polynomials

Throughout this paper we let F2 be the field with two elements, n ∈ N+ , and P = F2 [X 1 , . . . , X n ] the polynomial
ring over F2 in the indeterminates X 1 , . . . , X n . Recall that the ring of Boolean polynomials is
Bn = P/X 12 − X 1 , . . . , X n2 − X n 
20 Page 4 of 26 B. Andraschko et al.

where In = X 12 − X 1 , . . . , X n2 − X n  is also called the field ideal in P. Whenever additional indeterminates are
required, we write
Bn,m = F2 [X 1 , . . . , X n , Y1 , . . . , Ym ]/In,m
where In,m = X 12 − X 1 , . . . , X n2 − X n , Y12 − Y1 , . . . , Ym2 − Ym . For i ∈ {1, . . . , n} and j ∈ {1, . . . , m}, we denote
the residue class of X i in Bn and Bn,m by xi and the residue class of Y j in Bn,m by y j . These residue classes
will be called the indeterminates of Bn and Bn,m , respectively, and the elements of these rings are called Boolean
polynomials.
Every Boolean polynomial f ∈ Bn can be uniquely written as a sum of distinct square-free terms, where a term
is a product of distinct residue classes xi . This is known as the algebraic normal form (ANF) of f . (See for instance
[26, Sec. 2.1] or [8] for an in-depth study of ANFs.) Altogether, we have Bn = F2 [x1 , . . . , xn ] as an F2 -algebra
and dimF2 (Bn ) = 2n .
Given f ∈ Bn \ {0} in ANF, replacing each xi by X i yields its canonical representative F ∈ P. Then the support
of f is Supp( f ) = {t + In | t ∈ Supp(F)} and the degree of f is given by
deg( f ) = min{deg(F) | F ∈ P, f = F + In }.
The F2 -linear span of all Boolean polynomials of degree ≤ 1 plays a major role subsequently. It is denoted by
Ln = 1, x1 , . . . , xn F2 = F2 ⊕ F2 x1 ⊕ · · · ⊕ F2 xn
and called the vector space of linear Boolean polynomials. (Note that Ln includes the element 1.)
In Sect. 4 we also need division with remainders for Boolean polynomial rings. Let σ be a term ordering on P, and
let f, g1 , . . . , gs ∈ Bn be Boolean polynomials in ANF. Let F, G 1 , . . . , G s ∈ P be the canonical representatives of
f, g1 , . . . , gs , respectively. Then the normal remainder of f under the division by G = (g1 , . . . , gs ) is defined by
NRσ,G ( f ) = NRσ,(G 1 ,...,G s ) (F) + In .
Moreover, we denote the ordering induced by σ on the terms in Bn by σ again and call LTσ ( f ) = LTσ (F) + In
the leading term of f with respect to σ . For the definitions and an explanation of these concepts in P see [30],
Chapter I, and for more details about orderings on Boolean polynomial rings see [8].

3 Logical Representations of Boolean Polynomials

In the following we let Bn = F2 [x1 , . . . , xn ] be the ring of Boolean polynomials. Our goal is to connect Boolean
polynomials to propositional logic formulas. We assume that the readers are familiar with the syntax of propositional
logic and identify true ≡ 1 as well as false ≡ 0.
Definition 3.1 Let S be a subset of Bn , and let F be a propositional logic formula in the logical variables X 1 , . . . , X n .
(a) The set Z(S) = {(a1 , . . . , an ) ∈ Fn2 | f (a1 , . . . , an ) = 0 for all f ∈ S} is called the zero set of S.
(b) The set S(F) = {(a1 , . . . , an ) ∈ Fn2 | F| X 1 →a1 ,...,X n →an ≡ true} is called the set of satisfying assignments
of F.
(c) Given an ideal I in Bn , a propositional logic formula F is called a logical representation of I if S(F) = Z(I ).
(d) Given a propositional logic formula F, the uniquely determined ideal I F in Bn such that Z(I F ) = S(F) is
called the algebraic representation of F.
Recall that Bn is a principal ideal ring in which every ideal has a unique generator and that every propositional
logic formula is equivalent to a formula in conjunctive normal form (CNF). Effective transformations between
these representations have been studied extensively (see for instance [11,29]).
One disadvantage of converting Boolean polynomials to CNF is that sums correspond to XOR connectives and
a long chain of XOR connectives yields an exponentially large set of CNF clauses. To address this problem, we
introduce a new type of normal form next. Afterwards, we examine algorithms for converting Boolean polynomials
to this normal form and back.
SAT Solving Using XOR-OR-AND Normal Forms Page 5 of 26 20

Definition 3.2 (XOR-OR-AND Normal Form) Let F be a propositional logic formula.

(a) A formula of the form L 1 ⊕ L 2 ⊕ · · · ⊕ L m with literals L 1 , . . . , L m is called a lineral.
(b) A disjunction of linerals is called an XNF clause.
(c) The formula F is said to be in XOR-OR-AND normal form (XNF) if F is a conjunction of XNF clauses.
(d) Let k ∈ N. If F is in XNF and every XNF clause of F involves at most k linerals then we say that F is in k-XNF.

Notice that every literal is also a lineral. Hence every formula in CNF is already in XNF. The negation of a lineral
is a lineral because of
¬(L 1 ⊕ L 2 ⊕ · · · ⊕ L m ) ≡ ¬L 1 ⊕ L 2 ⊕ · · · ⊕ L m .
 
Moreover, every lineral is equivalent to a lineral of the form i X i or ¬( i X i ).
Observe that [36] introduces a normal form with the same name, but for formulas that consist of CNF clauses
and XOR constraints on the variables. In the terminology defined here, these are XNF unit clauses. We also refer
to a formula of this type as a CNF-XOR, consistent with related research [19,29,32,38,39,41].
The motivation for introducing the XNF is its algebraic representation which can be described as follows.

Remark 3.3 Let X 1 , . . . , X n be propositional logic variables.

(a) Let L = X i1 ⊕ · · · ⊕ X it be a lineral with i 1 , . . . , i t ∈ {1, . . . , n}. Then the algebraic representation of L is the
ideal xi1 + · · · + xit + 1 in Bn . Thus linerals correspond to linear polynomials in Bn .
(b) Let L 1 , . . . , L s be linerals, and let C = L 1 ∨ · · · ∨ L s be an XNF clause. For i ∈ {1, . . . , s}, let i ∈ Ln
be the algebraic representation of L i . Then 1 · · · s  is the algebraic representation of C. Thus XNF clauses
correspond to products of linear Boolean polynomials.
(c) Let C1 , . . . , Cr be XNF clauses, and let F = C1 ∧ · · · ∧ Cr be a logical formula in XNF. For i ∈ {1, . . . , r }, let
ci ∈ Bn be the product of linear Boolean polynomials representing Ci . Then the algebraic representation of F
is the ideal c1 , . . . , cr  in Bn .

For the converse transformation, we could use the logical representation of a Boolean polynomial which is in
CNF, and hence in XNF. However, as we are striving for logical formulas in XNF which have few and short clauses,
i.e., correspond to few low-degree Boolean polynomials, we proceed along a different path in the following two
subsections.
Moreover, the XNF is the natural input to the proof system s-Res [26], and therefore builds the basis for
any s-Res-based solving algorithms.

3.1 Reduction of Formulas in XNF to 2-XNF

It is a well-known property of propositional logic formulas that they can be transformed to equisatisfiable formulas
in 3-CNF by introducing additional variables. In the following we focus on an analogous transformation of formulas
in XNF.

Definition 3.4 Let S ⊆ Fn2 , and let T ⊆ Fn+m 2 for some n, m ∈ N. Then we write S ≡n T if the projection map
π : Fn+m
2 −→ Fn defined by π((a , . . . , a
2 1 n+m = (a1 , . . . , an ) induces a bijection π |T : T −→ S.
))

The relation ≡n has the following useful properties.

Remark 3.5 Let F be a logical formula involving the variables X 1 , . . . , X n , and let G be a formula involving the
variables X 1 , . . . , X n , Y1 , . . . , Ym .
(a) If we have S(F) ≡n S(G) then the formulas F and G are clearly equisatisfiable. More precisely, the satisfying
assignments of G are in one-to-one correspondence with the satisfying assignments of F via the projection π
to the first n coordinates.
20 Page 6 of 26 B. Andraschko et al.

(b) In general, the relation ≡n is not symmetric, but it is transitive in the following sense. Let k, m, n ∈ N, let
S ⊆ Fn2 , let T ⊆ Fn+m
2 , and let U ⊆ F2n+m+k . If we have S ≡n T and T ≡n+m U then S ≡n U .
The following lemma provides the key step for the reduction of formulas in XNF to 2-XNF. It can be easily
verified using a truth table.
Lemma 3.6 Let L 1 , L 2 be two linerals, and let Y be an additional logical variable. Then we have
Y ↔ (L 1 ∨ L 2 ) ≡ (Y ∨ ¬L 2 ) ∧ (¬(Y ⊕ L 1 ) ∨ L 2 ).
Notice that the left side of the equivalence in this lemma is symmetric in L 1 and L 2 . Thus, swapping L 1 and L 2
on the right-hand side of the equivalence also yields an equivalent formula. The following Algorithm 1 converts
logical formulas in XNF to 2-XNF.

Algorithm 1: XNFto2XNF – XNF to 2-XNF Conversion

Input : A logical formula F in XNF involving n variables.
Output: A logical formula G in 2-XNF with S (F) ≡n S (G).

1 Let i = 0 and M = ∅. Write F = rk=1 Ck .
2 for k = 1 to r do
3 while Ck contains
 more than two linerals do
4 Write Ck = sj=1 L j with linerals L j .
5 Increase i by 1 and letYi be a new variable.
6 Replace Ck by (Yi ∨ sj=3 L j ).
7 Adjoin {(Yi ∨ ¬L 2 ), (¬(Yi ⊕ L 1 ) ∨ L 2 )} to M.
8 Append Ck to M.

9 return M.

Proposition 3.7 Let F be a propositional logic formula in XNF involving n logical variables. Then XNFto2XNF
is an algorithm which returns a logical formula G in 2-XNF such that S(F) ≡n S(G).
Proof As the number of linerals in Ck is decreased with every execution of Line 6, the loop in Lines 3-7 stops after
finitely many iterations. Thus the algorithm terminates after finitely many steps.
To prove correctness, we first observe that every XNF clause which is added to M contains at most two linerals,
so the output formula is indeed in 2-XNF. Moreover, by Lemma 3.6, we have
  
S(Ck ) ≡n+i−1 S (Yi ∨ sj=3 L j ) ∧ (Yi ∨ ¬L 2 ) ∧ (¬(Yi ⊕ L 1 ) ∨ L 2 )
 
in Line 5 of the algorithm. Hence we obtain S( M ∧Ck ) ≡n+i−1 S( M  ∧Ck ) in Line 7, where M  and Ck denote
the values of M and Ck , respectively, after their modification inside the loop (Lines 3-7). By Remark 3.5.b, this
implies S(F) ≡n S( M) after every iteration of the outer loop (Lines 2-8), and consequently after its termination.


Example 3.8 Consider the formula F = X 1 ∨ X 2 ∨ X 3 in 3-CNF. Applying XNFto2XNF to F yields the logical
formula
G = (Y1 ∨ X 3 ) ∧ (Y1 ∨ ¬X 2 ) ∧ (¬(Y1 ⊕ X 1 ) ∨ X 2 ).
where Y1 is a new variable, and we have S(F) ≡3 S(G).
Remark 3.9 Suppose a formula F is in k-XNF for some k ∈ N and contains r XNF clauses. Then XNFto2XNF
introduces at most r (k − 2) new variables and 2r (k − 2) new clauses, since at most k − 2 new variables are added
for each clause. This shows that every formula in CNF can be converted to a formula in 2-XNF in polynomial time.
Consequently, the decision problem for 2-XNF instances is NP-complete.
SAT Solving Using XOR-OR-AND Normal Forms Page 7 of 26 20

In spite of this seemingly negative worst-case complexity, it is well-known that 2-CNF formulas can be solved
in linear time [5]. In Sect. 4, we will further address how some of the core ideas of 2-CNF solving can be translated
to solving formulas in 2-XNF. Finally, note that one can not only reduce the size of the XNF clauses, but also the
length of its linerals, i.e., the number of variables it contains, by using additional variables.
Remark 3.10 Let L , L 1 , L 2 be linerals with L ≡ L 1 ⊕ L 2 . If Y is an additional logical variable, then we have
L ≡ (L 1 ⊕ Y ) ∧ (L 2 ⊕ ¬Y ). Repeated application and addition of new variables shows that every XNF formula
can be reduced to a 2-XNF formula in which each lineral is a XOR of at most 3 variables.
Better constructions to trade the length of linerals with additional variables can be derived from the methods of
[21,36].

3.2 2-XNF Representations of Boolean Polynomials

In order to apply 2-XNF solving algorithms to practical instances, we first need to create tools to convert problems
given via Boolean polynomials in ANF to logical formulas in 2-XNF.
A straightforward approach is to search for XORs of variables in a CNF representation of the problem which
correspond to XNF clauses of size 1 as for instance done in [36]. While this produces XNF instances, in many
situations it does not capture the XOR-rich information well. In fact, we should find non-trivial XNF clauses
when they exist to harness the full potential of XNF-SAT solvers. This is why we suggest to start with an ANF
representation of the problem under investigation, as it is more compact and uses fewer variables. So, in this section
we show how Boolean polynomials can be converted to 2-XNF. To illustrate the algorithm, we apply it to problems
with a cryptographic background.
To ease the notation we switch completely to the algebraic point of view. Not only the input of our conversion
algorithm is denoted algebraically, but also the output 2-XNF. In view of Remark 3.3, the following definition
captures this approach.
Definition 3.11 (2-XNF Representation) Let I be an ideal in Bn . A set of Boolean polynomials of the form S =
{ f 1 g1 , . . . , f k gk , 1 , . . . , s } ⊆ Bn,m with f i , gi ,  j ∈ Ln is called a 2-XNF representation of I if Z(I ) ≡n Z(S).
Similarly, a set S ⊆ Bn,m as above is called a 2-XNF representation of a Boolean polynomial f ∈ Bn if S is a
2-XNF representation of  f .
Now Proposition 3.7 immediately implies the following result.
Corollary 3.12 Let I be an ideal in Bn . Then there exists a 2-XNF representation of I .
The next proposition shows a direct way to compute 2-XNF representations of certain polynomials. It is an
algebraic formulation of Lemma 3.6.
Proposition 3.13 Let g = 1 2 + 3 ∈ Bn , where 1 , 2 , 3 ∈ Ln , and let
S = {3 (2 + 1), 2 (1 + 3 )}.
Then we have S = g. In particular, the set S is a 2-XNF representation of g.
Proof From g = 3 (2 + 1) + 2 (1 + 3 ), we obtain g ∈ S and hence g ⊆ S. Moreover, we have 3 (2 + 1) =
(2 + 1)g ∈ g and 2 (1 + 3 ) = 2 g ∈ g, which implies S ⊆ g and hence S ⊆ g. 

Remark 3.14 To see the connection with Lemma 3.6, let L 1 and L 2 be linerals and Y an additional variable.
Let 1 , 2 , 3 ∈ Ln such that i  is the algebraic representation of L i for i ∈ {1, 2} and 3  is the algebraic
representation of Y . Then the ideal 1 2 + 3  is the algebraic representation of Y ↔ (L 1 ∨ L 2 ), the ideal
3 (2 + 1) is the algebraic representation of (Y ∨ ¬L 2 ), and the ideal 2 (1 + 3 ) is the algebraic representation
of (¬(Y ⊕ L 1 ) ∨ L 2 ).
20 Page 8 of 26 B. Andraschko et al.

Algorithm 2: ANFto2XNF – Boolean Polynomials to 2-XNF

Input : A Boolean polynomial f ∈ Bn .
Output: A 2-XNF representation of f .
1 Set i = 0 and M = ∅.
2 for t ∈ Supp( f ) do
3 while deg(t) > 1 do
4 Increase i by 1 and let yi be a new indeterminate.
5 Write f = t + f  and t = 1 2 s where s is a term, 1 , 2 are distinct indeterminates, and f  ∈ Bn,i−1 .
6 Replace t by yi s and f by yi s + f  .
7 Adjoin {yi (2 + 1), 2 (1 + yi )} to M.

8 return M ∪ { f }.

Proposition 3.13 immediately yields the following Algorithm 2 for computing a 2-XNF representation of a given
Boolean polynomial.

Proposition 3.15 Let f ∈ Bn . Then ANFto2XNF is an algorithm which returns a 2-XNF representation S =
ANFto2XNF( f ) of f .

Proof First we see that in each iteration of the inner loop (Lines 3-7), the degree of t decreases by one, so it
eventually reaches 1. Moreover, the polynomial f is updated in Line 6 in such a way that the term t in the support of
f is replaced by a term of smaller degree. Thus the outer loop (Lines 2-7) terminates eventually and the procedure
stops in Line 8. In particular, at this point f is linear and all elements of M ∪ { f } are linear or products of two
linear polynomials. Hence the output is in 2-XNF.
For the correctness, assume that we are in the i-th iteration of the inner loop (Lines 3-7). Denote the values of
f and M after the i-th iteration by f i and Mi , respectively. Here we let M0 = ∅ and f 0 denote the initial input
value of f . Consider the ideals J = Mi−1 ∪ { f i−1 } ⊆ Bn,i−1 and J  = Mi−1 ∪ { f i−1 } ∪ {yi + 1 2 } ⊆ Bn,i .
For c = (c1 , . . . , cn+i ) ∈ Fn+i 
2 , we see that c ∈ Z(J ) if and only if (c1 , . . . , cn+i−1 ) ∈ Z(J ) and cn+i =

(i  j )(c1 , . . . , cn+i−1 ). Hence Z(J ) ≡n+i−1 Z(J ).
Now observe that f i = f i−1 + s(1 2 + yi ) ≡ f i−1 mod J  , and hence J  = Mi−1 ∪ { f i } ∪ {yi + 1 2 }. Thus
Proposition 3.13 shows J  = Mi ∪ { f i }. Therefore we have Z( f 0 ) ≡n Z(M ∪ { f }) after every iteration of the
inner loop, i.e., the output in Line 8 is indeed a 2-XNF representation of the input f . 


Example 3.16 Consider the polynomial f = x1 x2 x3 ∈ B3 . The ideal  f  is the algebraic representation of the
clause ¬X 1 ∨ ¬X 2 ∨ ¬X 3 . We introduce a new indeterminate y1 and construct the ideal

I =  f, y1 + x1 x2  =  y1 x3 , y1 (x2 + 1), x2 (x1 + y1 )  ⊆ B3,1 .

Then we have Z( f ) ≡3 Z(I ), which shows that the set S = {y1 x3 , y1 (x2 + 1), x2 (x1 + y1 )} ⊆ B3,2 is a 2-XNF
representation of f . Note that S corresponds to the 2-XNF formula

(¬Y1 ∨ ¬X 3 ) ∧ (¬Y1 ∨ X 2 ) ∧ (¬X 2 ∨ ¬(X 1 ⊕ Y1 ) )

in the variables X 1 , X 2 , X 3 , Y1 .

Notice that ANFto2XNF employs Proposition 3.13 only for replacing products of two indeterminates. For
quadratic polynomials, this uses one additional variable for every non-linear term. With the following optimised
Algorithm 3, one may replace more than one term at a time.

Proposition 3.17 Let f ∈ Bn with deg( f ) ≤ 2. Then QANFto2XNF is an algorithm which returns a 2-XNF
representation S = QANFto2XNF( f ) of f .
SAT Solving Using XOR-OR-AND Normal Forms Page 9 of 26 20

Algorithm 3: QANFto2XNF – Quadratic Boolean Polynomials to 2-XNF

Input : A Boolean polynomial f ∈ Bn with deg( f ) ≤ 2.
Output: A 2-XNF representation of f .
1 Let i = 0 and M = ∅.
2 while deg( f ) = 2 do
3 Increase i by 1 and let yi be a new indeterminate.
4 Write f = 1 2 + f  for distinct 1 , 2 ∈ Ln and for f  ∈ Bn,i−1 such that Supp( f  ) contains fewer non-linear terms than
Supp( f ).
5 Set f = yi + f  .
6 Adjoin {yi (2 + 1), 2 (1 + yi )} to M.
7 return M ∪ { f }.

Proof After each iteration of the loop (Lines 2-6), the support of f contains fewer non-linear terms. Therefore f
eventually becomes linear and the loop terminates.
For proving correctness, consider the iterations of the loop. As in Proposition 3.15, we see that Mi−1 ∪ { f i−1 } ∪
{yi + 1 2 } = Mi ∪ { f i }, where Mi and f i denote the values of f and M after the i-th iteration, and f 0 is the
initial value of f . In particular, this shows that we have Z( f 0 ) ≡n Z(M ∪ { f }) after every iteration. Thus the output
is a 2-XNF representation of the input f . 

To implement Line 4 of QANFto2XNF efficiently, we may use different approaches. The following remark
collects some of them.
Remark 3.18 Let f ∈ Bn be of degree ≤ 2. In order to find 1 , 2 ∈ Ln such that Supp( f − 1 2 ) contains fewer
quadratic terms than Supp( f ), we may use one of the following methods.
(a) Write f = xi i + gi with i ∈ {1, . . . , n} and i ∈ Ln \F2 such that no term in the support of gi is divisible
by xi . Then the support of f − xi i = gi is a proper subset of Supp( f ). In particular, it contains fewer quadratic
terms. Repeating this step requires at most n − 1 substitutions until all non-linear terms in f have been replaced.
Hence any quadratic polynomial f ∈ Bn has a 2-XNF representation   that uses fewer than n − 1 additional
indeterminates, even though the support of f may contain up to n2 quadratic terms.
(b) Let y1 , . . . , yn , z 1 , . . . , z n be new indeterminates, and let
G = (y1 x1 + · · · + yn xn ) · (z 1 x1 + · · · + z n xn ) ∈ Bn [y1 , . . . , yn , z 1 , . . . , z n ]
be a product of two generic linear Boolean polynomials. By multiplying out, we obtain a representation
 
n
G = G i j xi x j + Hk xk .
1≤i< j≤n k=1
with G i j , Hk ∈ F2 [y1 , . . . , yn , z 1 , . . . , z n ].
 n
Write f = 1≤i< j≤n f i j x i x j + k=1 f k x k + f 0 with f i j , f k , f 0 ∈ F2 . If we find a tuple c =
(a1 , . . . , an , b1 , . . . , bn ) ∈ F2 such that as many of the equations f i j = G i j (c) as possible are satisfied,
2n

then the linear Boolean polynomials 1 = a1 x1 + · · · + an xn and 2 = b1 x1 + · · · + bn xn satisfy the property

that f − 1 2 contains as few quadratic terms in its support as possible. Such a tuple c can be found using
an OMT solver, e.g., using OptiMathSAT [37]), or by rephrasing the optimization problem as a MaxSAT
problem and using an adequate solver, e.g., using MaxHS [16].
The strategy of part (b) works well on small inputs, say polynomials having fewer than 20 indeterminates. For
cases involving larger numbers of indeterminates, it is better to combine part (a) with the next observation.
Lemma 3.19 Let f ∈ Bn and 1 , 2 , 1 , 2 ∈ Ln with Supp(1 2 ) ⊆ Supp( f ) and Supp(1 2 ) ⊆ Supp( f ). Then
we have Supp(m 1 m 2 ) ⊆ Supp( f ) for
 
m 1 = (Supp(1 ) ∪ Supp(1 )) and m 2 = (Supp(2 ) ∩ Supp(2 )).
20 Page 10 of 26 B. Andraschko et al.

Proof Let t = xi1 xi2 ∈ Supp(m 1 m 2 ) where xi1 ∈ Supp(m 1 ) and xi2 ∈ Supp(m 2 ). Then xi1 ∈ Supp(1 ) or
xi1 ∈ Supp(1 ), and xi2 ∈ Supp(2 ) ∩ Supp(2 ). This shows xi1 xi2 ∈ Supp(1 2 ) or xi1 xi2 ∈ Supp(1 2 ). Both
imply t ∈ Supp( f ). 


Using the method of Remark 3.18.a, we can now find many distinct pairs (1 , 2 ) ∈ L2n with Supp(1 2 ) ⊆
Supp( f ). Applying the Lemma randomly to two such pairs of linear polynomials, we find more pairs (m 1 , m 2 ) ∈ L2n
with Supp(m 1 m 2 ) ⊆ Supp( f ). Repeating this procedure for some time can generate many non-trivial such pairs,
and we can simply choose the one which eliminates the most non-linear terms. This has proven to produce very
good results, even for polynomials with a high number of indeterminates.

Example 3.20 Let us apply Algorithm QANFto2XNF to the Boolean polynomial f = x1 x3 + x2 x3 + x1 x4 + x2 x4 +

x1 ∈ B4 . In Line 4 we try to cancel out as many non-linear terms as possible, following the above approach. Using
Remark 3.18.a, we see that Supp( x1 · (x3 + x4 + 1) ) ⊆ Supp( f ) and Supp( x2 · (x3 + x4 ) ) ⊆ Supp( f ). By
applying Lemma 3.19 with m 1 = x1 + x2 and m 2 = x3 + x4 , we get Supp(m 1 m 2 ) ⊆ Supp( f ). Let y1 be a new
indeterminate and write f = m 1 m 2 + x1 . Now we replace f by y1 + x1 and set

M = { y1 (x3 + x4 + 1), (x3 + x4 )(x1 + x2 + y1 ) }.

Notice that the loop now ends, as f is linear, and the 2-XNF representation { f }∪ M of f is returned. This corresponds
to the 2-XNF formula

(¬Y1 ∨ (X 3 ⊕ X 4 )) ∧ (¬(X 3 ⊕ X 4 ) ∨ ¬(X 1 ⊕ X 2 ⊕ Y1 )) ∧ ¬(Y1 ⊕ X 1 ))

in the variables X 1 , X 2 , X 3 , X 4 , Y1 .

After discussing the effective computation of 2-XNF representations of individual polynomials, we now turn
our attention to Boolean polynomial ideals given by several generators. In this case we can avail ourselves of the
following approaches.

Remark 3.21 Let f 1 , . . . , f s ∈ Bn \{0}, and let I =  f 1 , . . . , f s . The following methods can be applied to find a
2-XNF representation of I .
(a) The most basic approach is to apply ANFto2XNF (or QANFto2XNF) to f i for i ∈ {1, . . . , s} and to combine
the individual 2-XNF representations to get one for I . Unfortunately, this tends to introduce more additional
variables than necessary, since the same terms in different polynomials will be replaced with distinct additional
indeterminates.
(b) If f 1 , . . . , f s are quadratic, the problem in (a) can be counteracted as follows. During the computation of the
2-XNF representations of the f 1 , . . . , f s , we remember how the additional indeterminates y1 , . . . , ym were
used to substitute products 11 12 , . . . , m1 m2 in the execution of Lines 4-5 of QANFto2XNF. After those
individual conversions, we compute an F2 -basis {h 1 , . . . , h t } ⊆ Lm of the set of relations
{g ∈ Lm | g(11 12 , . . . , m1 m2 ) = 0}.
Then we return the union of all the individual 2-XNF representations and {h 1 , . . . , h t }. Each of these linear
Boolean polynomials eliminates one variable in the process of computing Z(I ).

In particular, instances coming from cryptographic attacks can be converted efficiently using those approaches.
In many ciphers the only non-linearity appears in the so-called S-Boxes. Usually, these involve only a small number
of indeterminates, i.e., they can be represented by relatively few non-linear polynomials in a small number of
indeterminates. To illustrate this approach, let us examine the encryption map of the Ascon cryptosystem [18]
which has been selected for the standardization of lightweight ciphers by NIST.

Example 3.22 As specified in [18], the Ascon cryptosystem is a 128-bit lightweight cipher.
SAT Solving Using XOR-OR-AND Normal Forms Page 11 of 26 20

(a) Let s : F52 → F52 be the 5-bit S-box used in the Ascon cipher. Consider the Boolean polynomial ring B5,5 =
F2 [x1 , . . . , x5 , y1 , . . . , y5 ] and let I ⊆ B5,5 be the vanishing ideal of the set of points {(a, s(a)) | a ∈ F52 } ⊆
2 . Using [6], we know that I is generated by five quadratic polynomials in B5,5 . Applying QANFto2XNF
F10
together with the method from Remarks 3.18b and 3.21b, we obtain a 2-XNF representation of I consisting
of 10 products of two linear polynomials and not a single additional indeterminate.
(b) Altogether, these methods construct a 2-XNF representation of the entire Ascon-128 cipher (processing 8
bytes of plaintext) involving as little as 6080 variables and 17 664 clauses.
For comparison, converting the same polynomials to CNF using PolyBoRi [9] requires 12 224 variables and
137 739 clauses, the methods from [29] require 55 825 variables and 214 024 clauses, and the conversion tool
within Bosphorus [11] requires 49 289 variables and 1 424 034 clauses for the logical representation of the
cipher.

This shows that encoding XOR-rich formulas in 2-XNF yields far more compact representations than state-of-
the-art conversions to sets of CNF clauses.

Remark 3.23 To efficiently store instances in XNF, we suggest a derivation of the established DIMACS standard
for CNFs: in the place of literals (encoded as -L or L) we encode linerals as literals connected (without whitespace)
with the symbol +. Then the Ascon S-Box has the following XNF-representation:
p xnf 10 10
-2 4+5+6 0 -4 2+3+8 0
2+3 -1+2+4+5+7 0 1 -2+3+4+5+9 0
-1 2+3+9 0 2 -1+3+4+6 0
-2+3 1+5+7 0 2 -4+5+10 0
-2 1+4+10 0 4 2+3+5+8 0
Note that solvers supporting this encoding can also process usual DIMACS CNF files correctly.

4 Graph-Based 2-XNF SAT Solving

It is well-known that a satisfiable assignment of a 2-CNF instance F, i.e., a propositional logic formula in CNF
where every clause has at most two literals, can be found with linear time and space complexity [5]. The key idea
is to express the formula F by a (directed) implication graph whose set of vertices is the set of literals occurring
in F and their respective negations, and for which every clause L i ∨ L j of F corresponds to the pair of edges
(¬L i , L j ) and (¬L j , L i ). Then a greedy algorithm working along a topological ordering of the strongly connected
components of this graph constructs a satisfying assignment. In this section we present a graph-based 2-XNF solver
that follows a DPLL approach where the above ideas form the basis of the in-processing step.

4.1 Implication Graph Structures

Recall that, for a propositional logic formula F in 2-XNF, the algebraic representation I F ⊆ Bn is of the form
I F =  f 1 g1 , . . . , f k gk , 1 , . . . , s  ⊆ Bn
for some f i , gi ,  j ∈ Ln . Based on the central idea of implication graph based linear time 2-CNF solving, we
introduce the following notion.

Definition 4.1 (Implication Graph Structures)

Let F be a formula in 2-XNF.
(a) A tuple (L , V, E), where L , V ⊆ Ln and E ⊆ V 2 , is called an implication graph structure (IGS) for F if
the following conditions are satisfied:
20 Page 12 of 26 B. Andraschko et al.

(1) I F = L +  f g | ( f + 1, g) ∈ E.

(2) (Skew-Symmetry) For all ( f + 1, g) ∈ E, we have (g + 1, f ) ∈ E.
(3) For all f ∈ V , we have ( f, f ) ∈
/ E.
(b) Let σ be a term ordering. An IGS (L , V, E) for F is called σ -reduced if the polynomials in L have pairwise
distinct leading terms and

LTσ (L) ∩ f ∈V Supp( f ) = ∅.
For an IGS (L , V, E), the pair (V, E) is clearly a graph. Such graphs are called implication graphs in view of
the following observation.
Remark 4.2 Let (L , V, E) be an IGS for a formula F, and let ( f, g) ∈ E. By definition, we then have ( f +1)g ∈ I F ,
and therefore
f ∈ IF ⇒ g = f g + ( f + 1)g ∈ I F .
In other words, if the source node of an edge in the graph (V, E) is contained in the ideal I F , then its target node
is in I F , too. The set L simply collects all known linear information of I F .
Given an IGS G = (L , V, E) for a formula F, a sequence f 1 , . . . , f s ∈ V with ( f i , f i+1 ) ∈ E for i ∈
{1, . . . , s − 1} is called a path in G. In this case we also write f 1 → f s .
Lemma 4.3 Let G be an IGS for a formula F, and let f → g be a path in G. Then we have ( f + 1)g ∈ I F .
Proof Let the path f → g be given by ( f i , f i+1 ) ∈ E for i ∈ {1, . . . , s − 1}, where f = f 1 and g = f s for some
s ∈ N+ . We show the claim by induction on s. By Definition 4.1, the statement is true if s = 1. Assume that the
claim is correct for paths of length s − 1. Then we have ( f 2 + 1) f s ∈ I F , and by Definition 4.1 also ( f 1 + 1) f 2 ∈ I F .
This shows
( f 1 + 1) f s = ( f 1 + 1) f 2 f s + ( f 1 + 1)( f 2 + 1) f s ∈ I F .


This lemma implies that the transitive closure (V, E  ) of (V, E) yields an implication graph structure (L , V, E  )
for F. It is easy to find an implication graph structure for a formula in 2-XNF, as the next remark indicates.
Remark 4.4 (Trivial Implication Graph Structures)
Let F be a formula in 2-XNF with an algebraic representation of the form
I F =  f 1 g1 , . . . , f k gk , 1 , . . . , s  ⊆ Bn
where f i , gi ,  j ∈ Ln are pairwise distinct.
(a) Then the implication graph structure (L , V, E) given by L = {1 , . . . , s },
k k
V = { f i , f i + 1, gi , gi + 1 }, and E = { ( f i + 1, gi ), (gi + 1, f i ) }
i=1 i=1
is called the trivial implication graph structure for F.
(b) The implication graph structure (L , V, E) given by L = {1 , . . . , s },

V = { f i , f i + 1, gi , gi + 1, f i + gi , f i + gi + 1 | 1 ≤ i ≤ k}, and
k
E = { ( f i + 1, gi ), ( f i + 1, f i + gi + 1), ( f i + gi , gi ) }
i=1
k
∪ { (gi + 1, f i ), ( f i + gi , f i ), (gi + 1, f i + gi + 1) }
i=1

is called the extended trivial implication graph structure for F.

SAT Solving Using XOR-OR-AND Normal Forms Page 13 of 26 20

Fig. 1 Implication graph x2 + x5

(V0 , E 0 ) from Example 4.5
x1 + x3 x1 + x2 + x3 + 1 x5 + 1

x1 x2 x3 + 1 x4 + 1

x4 x3 x2 + 1 x1 + 1

x5 x1 + x2 + x3 x1 + x3 + 1

x2 + x5 + 1

In both cases the size of the graph (V, E) is linear in the input size of the formula F, because we have #V ≤ 6k
and #E ≤ 3k.
Example 4.5 Let F be a formula in 2-XNF with algebraic representation

I F = (x1 + 1)x2 , (x2 + 1)(x1 + x3 ), (x2 + 1)x4 , (x5 + x2 + 1)(x1 + x3 ),

(x1 + x3 + 1)(x1 + x2 + x3 + 1), (x4 + 1)x3 , (x5 + 1)x4 ⊆ B5 .

Then the trivial IGS of F is (L 0 , V0 , E 0 ) where L 0 = ∅ and (V0 , E 0 ) is the graph given in Fig. 1.

Our solving algorithm starts with such a trivial IGS for F and improves it gradually by propagation, in-processing
and guessing until we arrive at an IGS with an empty graph, i.e., a case where the corresponding ideal is generated
just by linear polynomials. Given that the guesses were correct, a satisfying assignment of F can then be deduced
immediately from a solution to the corresponding system of linear equations. This improvement is measured in
terms of the size of the linear part L and in the size of the graph (V, E). The following relation specifies this in
detail.
Definition 4.6 Let F be a formula in 2-XNF, and let G  = (L  , V  , E  ) as well as G = (L , V, E) be two implication
graph structures for F. Then we write G   G if and only if L  F2 ⊇ LF2 and #V  ≤ #V . Moreover, if one of
the two conditions is strict, we write G  ≺ G.
The relation  defines a partial quasi-ordering on the set of all implication graph structures, i.e., it is reflexive,
transitive, and by the following lemma it satisfies the descending chain condition. The latter property is the key
ingredient for proving finiteness of the upcoming algorithms.
Lemma 4.7 (Descending Chain Condition for Implication Graph Structures) Let F be a formula in 2-XNF. Then
there is no infinite, strictly descending chain of implication graph structures for F.
Proof For a contradiction, assume there is an infinite strictly descending chain (L 1 , V1 , E 2 )  (L 2 , V2 , E 2 )  · · ·
of implication graph structures for F. By definition, it follows that there is an ascending chain of subspaces
L 1 F2 ⊆ L 2 F2 ⊆ · · · in Bn . Since Bn is a finite-dimensional F2 -vector space, this chain becomes eventually
stationary, i.e., there exists a number k ∈ N+ such that L k F2 = L i F2 for all i ≥ k. By Definition 4.6, this
implies #Vi+1 < #Vi for all i ≥ k. In this way, the #Vi form a decreasing sequence in N which eventually becomes
stationary. Consequently, at some point in the sequence, we have L i+1 F2 = L i F2 and #Vi+1 = #Vi , i.e. the
chain is not strictly decreasing. 

To conclude this section, we present the updating Algorithm 4 of our solver which computes the σ -reduction of
any given IGS. The method is an adaption of Gaußian Constraint Propagation (see [26, Algorithm 5.7]) to impli-
cation graph structures. Note that Gaußian Constraint Propagation itself is a generalization of Boolean Constraint
Propagation, also known as Unit Propagation, in traditional CNF-based SAT solvers.
20 Page 14 of 26 B. Andraschko et al.

Algorithm 4: GGCP – Graph Gaußian Constraint Propagation

Input : An IGS G for a formula F, a term ordering σ .
Output: A σ -reduced IGS G  for F with G   G.
1 Write G = (L , V, E) and LTσ -interreduce L.
2 Let (L  , V  , E  ) = (L , ∅, ∅).
3 for ( f, g) ∈ E do
4 Let f  = NRσ ( f, L) and g  = NRσ (g, L).
5 if f  = 0 and g  = 0 then append g  to L  .
6 if g  = 1 and f  = 1 then append f  + 1 to L  .
7 if f  ∈
/ F2 and g  ∈ / F2 and f  = g  then
8 append ( f  , g  ) to E  , append f  and g  to V  .

9 if L = L  then set (L , V, E) = (L  , V  , E  ) and go to Line 2.

10 else return (L  , V  , E  ).

Proposition 4.8 Let σ be a term ordering, let F be a formula in 2-XNF, and let G be an IGS for F. Then GGCP is
an algorithm which returns a σ -reduced implication graph structure G  = GGCPσ (G) for F such that G   G.

Proof Since (L , V, E) is an IGS for F, we have L ⊆ I F and ( f + 1)g ∈ I F for every pair ( f, g) ∈ E. Thus we
see that ( f  + 1)g  = (NRσ ( f, L) + 1) NRσ (g, L) ∈ I F holds in Line 4.
For f  = 0, this yields g  ∈ I F , and for g  = 1, we get f  + 1 ∈ I F . For all other cases, where f  ∈ F2 , g  ∈ F2 ,
or f  = g  , we have ( f  + 1)g  = 0, and the corresponding edge can be ignored. This shows that after Lines 3-8
have been executed, the tuple G  = (L  , V  , E  ) is indeed an IGS for F. Moreover, G  is σ -reduced, because for
all f  ∈ V  we have LTσ (L) ∩ Supp( f  ) = ∅ by construction.
Finally, note that we always have L  F2 ⊇ LF2 and #V  ≤ #V . This implies G   G for every iteration
of Lines 2-8, and this relation is strict if L = L  . By Line 9, these steps are repeated as long as this is the case,
and the implication graph structures (L  , V  , E  ) resulting from these iterations form a strictly descending chain.
By Lemma 4.7, this chain must be finite, i.e., there can only be finitely many iterations, and the procedure has to
terminate in Line 10. 


4.2 Pre-Processing Techniques

In this subsection we present two results which allow us to deduce new information from a given implication graph
structure. The first one derives new linerals, and the second one finds new edges between the vertices of a given
implication graph. These techniques are computationally rather expensive and should be seen as pre-processing
techniques which are only applied once before the main solving procedure.

Definition 4.9 Let F be a formula in 2-XNF, and let (L , V, E) be an IGS for F.

(a) The set of descendants of a vertex f ∈ V is defined by
D f = { f } ∪ {g ∈ V | there is a path f → g in (V, E)}.
Note that we consider f as a descendant of itself, since we have ( f + 1) f = 0 ∈ I F .
(b) The vector space  f = D f F2 ⊆ Ln will be called the space of descendants of f .

Note that, for a vector subspace U of Ln , we let 1 + U = { f + 1 | f ∈ U } be the affine subspace of Ln

representing the negation of U . The space of descendants of f ∈ V has the following useful properties.

Proposition 4.10 Let F be a formula in 2-XNF, let (L , V, E) be an implication graph structure for F.
(a) For all f ∈ V and g ∈  f , we have ( f + 1)g ∈ I F .
SAT Solving Using XOR-OR-AND Normal Forms Page 15 of 26 20

Fig. 2 Implication graph x5 + x2 x5 + 1

(V1 , E 1 ) from
Example 4.11
x2 + x3 x3 + 1 x4 + 1

x2 x2 + 1

x4 x3 x2 + x3 + 1

x5 x5 + x2 + 1

(b) Let f, g ∈ V . If  f ∩ (1 + g ) = ∅ then ( f + 1)(g + 1) ∈ I F .

(c) For all f ∈ V , we have  f ∩  f +1 ⊆ I F .
k
Proof To show (a), let g ∈  f . We write g = j=1 g j with g j ∈ D f . By Lemma 4.3, we have ( f + 1)g j ∈ I F
 k
for j ∈ {1, . . . , k}. Hence we obtain ( f + 1)g = j=1 ( f + 1)g j ∈ I F .
To prove (b), let h ∈  f and h + 1 ∈ g . Then (a) implies ( f + 1)h ∈ I F and (g + 1)(h + 1) ∈ I F . This shows

( f + 1)(g + 1) = ( f + 1)h(g + 1) + ( f + 1)(h + 1)(g + 1) ∈ I F .

For the proof of (c), let g ∈  f ∩  f +1 . From (a) we get ( f + 1)g ∈ I F and f g ∈ I F , and therefore
g = f g + ( f + 1)g ∈ I F . 


Example 4.11 In the situation of Example 4.5, we have x1 + x2 ∈ x2 ∩ x2 +1 . Proposition 4.10.c then implies
x1 + x2 ∈ I F , and thus (L 0 ∪ {x1 + x2 }, V0 , E 0 ) is an IGS for F as well. Let σ = lex and apply GGCPlex to this
tuple to get an IGS (L 1 , V1 , E 1 ) for F where L 1 = {x1 + x2 } and (V1 , E 1 ) is the graph given in Fig. 2.

Using this proposition, we construct the following straightforward pre-processing Algorithm 5. It runs in poly-
nomial time in the size of F and can find new linear information as well as new edges. Notice that numerous
intersections of affine F2 -subspaces of Fn2 have to be computed.

Algorithm 5: PP – (Edge-Extending) Pre-Processing

Input : An IGS G for a formula F, a term ordering σ .
Output: A σ -reduced IGS G  for F.
1 Let (L  , V  , E  ) = GGCPσ (G), let L pp = ∅ and let E pp = ∅.
2 for f ∈ V do
3 Add a basis of  f ∩  f +1 to L pp .
4 for g ∈ V \ { f + 1} do
5 if  f ∩ (1 + g ) = ∅ then add ( f + 1, g) and (g + 1, f ) to E pp

6 if L pp = ∅ or E pp = ∅ then set G = (L  ∪ L pp , V  , E  ∪ E pp ) and go to Line 1.

7 else return (L  , V  , E  )

It is clear that there is room for optimization of this algorithm if G does not contain any cycles. In this case
it suffices to check whether  f ∩ (1 + g ) = ∅ (see Line 5) initially only for sources f, g ∈ V of G, i.e., for
vertices with no incoming edges. Only if those spaces have a non-empty intersection, we need to consider their
corresponding descendants. (This follows immediately from the fact that Dg ⊆ D f if there is a path f → g.) Even
with this optimization, finding new edges is still computationally quite expensive. Hence Lines 4 and 5 are skipped
in our implementation by default.
20 Page 16 of 26 B. Andraschko et al.

4.3 In-Processing Techniques

Next we introduce two algorithms which deduce new linear polynomials from a given implication graph structure
more efficiently. Therefore they are suited as default in-processing techniques during the main solving procedure. In
particular, the methods we look at here are (partial) generalizations of the notions of equivalent and failed literals,
as discussed in [25].
As usual for directed graphs G = (V, E), a subset S ⊆ V is called a strongly connected component (SCC)
of G if, for all f, g ∈ S, there is a path f → g in G and if S is maximal with this property. It is well-known that
for any directed graph, the set of all SCCs can be computed in O(#V + #E) space and time [40]. The following
proposition indicates how these components can be used to deduce new linear information.

Proposition 4.12 Let F be a formula in 2-XNF, and let G = (L , V, E) be an IGS for F. Denote the set of SCCs
of (V, E) by C.
(a) Let { f 1 , . . . , fr } ∈ C. Then f 1 + f i ∈ I F for i ∈ {1, . . . , r }.
(b) If #C is odd, then F is unsatisfiable, i.e., we have I F = 1.

Proof Due to the skew-symmetry of implication graph structures, for every strongly connected component S =
{ f 1 , . . . , fr } ∈ C also S + 1 = { f 1 + 1, . . . , fr + 1} is an SCC of (V, E).
To show (a), we let i ∈ {1, . . . , r } and note that f 1 , f i ∈ S implies that there are paths f 1 → f i and f i → f 1
in G. By the skew-symmetry, we get f 1 + 1 → f i + 1. This shows f 1 , f i ∈ D f1 and f 1 + 1, f i + 1 ∈ D f1 +1 ,
and hence f 1 + f i ∈  f1 as well as f 1 + f i = ( f 1 + 1) + ( f i + 1) ∈  f1 +1 . By Proposition 4.10.c, we thus have
f1 + fi ∈ I F .
For the proof of (b), notice that we can write C = {S1 , . . . , Sc , S1 + 1, . . . , Sc + 1} for some c ∈ N, where we
have Si = S j and Si = S j + 1 for i = j. If #C is odd, there exists an index i ∈ {1, . . . , r } with Si = Si + 1. For
f ∈ Si , we then have f + 1 ∈ Si + 1 = Si and thus 1 = f + ( f + 1) ∈ I F by (a). 


By repeatedly computing all linear polynomials resulting from the strongly connected components and prop-
agating them using GGCP, one can update a given implication graph structure (L , V, E) such that it contains no
cycles, i.e., such that (V, E) becomes a directed acyclic graph (DAG). This is important, as for many graph-theoretic
problems there are linear time algorithms if the underlying graph is a DAG. Algorithm 6 performs these updates.

Algorithm 6: crGGCP – cycle-removing GGCP

Input : An IGS G for a formula F, a term ordering σ .
Output: An acyclic σ -reduced IGS G  for F with G   G.
1 Compute (L  , V  , E  ) = GGCPσ (G) and let L SCC = ∅.
2 Compute the set C of all strongly connected components of (V  , E  ).
3 if #C is odd then return (Ln , ∅, ∅).
4 for S ∈ C do
5 Write S = { f 1 , . . . , fr } and for all i ∈ {2, . . . , r } append f 1 + f i to L SCC .
6 if L SCC = ∅ then set G = (L  ∪ L SCC , V  , E  ) and go to Line 1.
7 else return (L  , V  , E  ).

Proposition 4.13 Let σ be a term ordering, let F be a formula in 2-XNF, and let G be an IGS for F. Then crGGCP
is an algorithm which returns a tuple G  = crGGCPσ (G) with the following properties.
(a) The tuple G  = (L  , V  , E  ) is a σ -reduced implication graph structure for F.
(b) We have G   G.
(c) The graph (V  , E  ) is acyclic.
SAT Solving Using XOR-OR-AND Normal Forms Page 17 of 26 20

Proof First note that if the procedure terminates in Line 3, the output is correct by Proposition 4.12.b. Thus we may
assume that the procedure does not terminate in Line 3.
The tuples (L  , V  , E  ) and (L  ∪ L SCC , V  , E  ) in Lines 1 and 6 are implication graph structures for F with
(L  , V  , E  )  (L , V, E) by Propositions 4.8 and 4.12. Moreover, if L SCC = ∅ then it contains at least one linear
polynomial f with LTσ ( f ) ∈ / LTσ (L  ), as (L  , V  , E  ) is a σ -reduced IGS. This shows (L  ∪ L SCC , V  , E  ) ≺
 
(L , V , E ). 

Next we observe that the repeated iterations of Lines 1-6 yield a strictly descending chain of IGSs which has
to become stationary after finitely many steps by Lemma 4.7. Therefore we eventually have L SCC = ∅, and the
procedure terminates in Line 7. In that case, the graph (V  , E  ) cannot contain any cycles, as otherwise there would
be a strongly connected component, and hence Line 5 would create elements in L SCC .
Finally, note that (L  , V  , E  ) is σ -reduced by Proposition 4.8 and the fact that this tuple is not changed in the
last iteration of Lines 2-6. 


As a second in-processing technique, we adapt the concept of failed literals, as discussed in [25], to our more
general setting.

Definition 4.14 Let F be a formula in 2-XNF, and let G = (L , V, E) be an implication graph structure for F.
(a) A vertex f ∈ V is called a failed lineral of G if 1 ∈  f .
(b) A failed lineral f ∈ V of G is called trivial if there is an element g ∈ V with f → g, and with f → g + 1 or
f → f + 1.

These literals are of interest for in-processing, if they can be found efficiently, since for every failed lineral we
learn a new linear polynomial in I F in the following way.

Lemma 4.15 Let F be a formula in 2-XNF, and let G = (L , V, E) be an IGS for F. If f ∈ V is a failed lineral
of G, then f + 1 ∈ I F .

Proof Let f be a failed lineral of G. Then 1 ∈  f yields f + 1 ∈  f . Using Proposition 4.10.c and f + 1 ∈  f +1 ,
we get f + 1 ∈  f ∩  f +1 ⊆ I F . 


To find a failed lineral, it is sufficient to check whether the vector subspace  f contains the constant polynomial 1.
# D ×(n+1)
This can be done for instance by computing the row-echelon form of a matrix in F2 f . Thus we obtain an
in-processing algorithm which runs in polynomial time and space. However, trivial failed linerals can be found in
near-linear time, as the next remark indicates.
For an implication graph structure (L , V, E) for a formula F in 2-XNF, we denote the set of ancestors of a
vertex f ∈ V by
A f = { f } ∪ {g ∈ V | there is a path g → f in (V, E)}.

Remark 4.16 Let F be a formula in 2-XNF, and let (L , V, E) be an acyclic implication graph structure for F.
(a) For every g ∈ V , all common ancestors of g and g + 1, i.e., the elements of A g ∩ A g+1 , are trivial failed linerals
by definition.
 Conversely, every trivial failed lineral f ∈ V is contained in A g ∩ A g+1 for some g ∈ V . Thus
the set g∈V (A g ∩ A g+1 ) consists exactly of the trivial failed linerals of G.
(b) If g ∈ V is a failed lineral then every f ∈ A g is a failed lineral as well, since Dg ⊆ D f . Thus, instead of
searching for all common ancestors of g and g + 1, it suffices to find the so-called lowest common ancestors,
i.e., the vertices f ∈ V such that no out-neighbour of f is a common ancestor of both g and g + 1.
(c) For sparse graphs, one of the lowest common ancestors of two vertices can be found in constant time after a
near-linear time pre-processing phase, see [15]. This produces many, but in general not all, trivial failed linerals
rather quickly under the assumption that the graph (V, E) is sparse (see Remark 4.4).
20 Page 18 of 26 B. Andraschko et al.

Algorithm 7: tFLS – Trivial Failed Lineral Search

Input : An acyclic IGS G for a 2-XNF formula F.
Output: All trivial failed linerals L TF of G.
1 Write G = (L , V, E), let M = ∅, and let L TF = ∅.
2 Compute the set S of sources of (V, E).
3 for s ∈ S do
4 if s + 1 ∈ Ds then append (s, s + 1) to M.
5 for all g ∈ V with s → g and s → g + 1 do append (s, g) to M.
6 for (s, g) ∈ M do
7 Append all common ancestors of g and g + 1 to L TF .
8 return L TF

Our implementation does not feature this advanced method for finding trivial failed linerals, as the corresponding
algorithms seem hard to implement. Instead we resort to the following simple Algorithm 7 which can be implemented
using only breadth-first-searches (BFS). Moreover, unlike the method of the previous remark, it computes all trivial
failed linerals.

Proposition 4.17 Let F be a formula in 2-XNF, and let G be an acyclic implication graph structure for F. Then
tFLS is an algorithm which returns a set L = tFLS(G) containing all trivial failed linerals of G satisfying
1 + L ⊆ IF .
In particular, the algorithm can be implemented to run in O (#V · (#V + #E)) time and space.

Proof The finiteness of the procedure is clear, since the graph (V, E) is finite. The correctness follows from
Remark 4.16 and the fact that in Line 7 the elements of L TF are exactly the common ancestors of vertices g and
g + 1 for all g ∈ V . Now L + 1 ⊆ I F follows immediately from Proposition 4.15. The claimed run-time complexity
is a consequence of the observation #M ≤ #V and the facts that Lines 4-5 can be implemented by a single BFS
starting at s, and that Line 7 amounts to two BFSs starting at g and g + 1 on the graph with reversed edges. 


To end this section we remark that our pre-processing algorithm PP is superior to our in-processing methods in
that it learns at least the same linear information, but might also increase the number of edges of the implication
graph.

Remark 4.18 Let σ be a term ordering, let F be a formula in 2-XNF, let G be an IGS for F, and let G  =
(L  , V  , E  ) = PPσ (G). Then we have 1 + tFLS(G) ⊆ L  F2 and G   crGGCP(G).
This follows immediately from the fact that tFLS is based on Lemma 4.15 whose proof already shows that all
failed linerals are contained in  f ∩  f +1 ⊆ I F for some f ∈ V . Thus these linerals are also found by PP.
Similarly, Algorithm crGGCP is based on Proposition 4.12 whose proof shows that all linear polynomials which
can be learnt here are already contained in  f ∩  f +1 for some f ∈ V . Once again, these linerals are found and
propagated by PP. Altogether, we see that PP essentially emulates both crGGCP and tFLS. As a consequence,
Algorithm PP also ensures that its output implication graph structure G  is acyclic.

While this shows that pre-processing with PP is more powerful than in-processing with tFLS and crGGCP,
keep in mind that it is also rather expensive due to its polynomial runtime.

Example 4.19 Let (L 1 , V1 , E 1 ) be the IGS from Example 4.11, then we have tFLS(L 1 , V1 , E 1 ) = {x2 }, since
there is a path x2 → x2 + 1 (see Fig. 2). This shows that x2 is a failed lineral and we get x2 + 1 ∈ I F . An application
of GGCPlex to (L 1 ∪ {x2 + 1}, V1 , E 1 ) yields the IGS (L 2 , V2 , E 2 ) where L 2 = {x1 + 1, x2 + 1} and (V2 , E 2 ) is
given in Fig. 3.
Notice that (V2 , E 2 ) has two strongly connected components. Thus we can use Proposition 4.12.a with the SCC
{x3 , x4 , x5 } to get x3 + x5 , x4 + x5 ∈ I F . Another application of GGCPlex to (L 2 ∪ {x3 + x5 , x4 + x5 }, V2 , E 2 )
SAT Solving Using XOR-OR-AND Normal Forms Page 19 of 26 20

Fig. 3 Implication graph x5 + 1 x3 x4

(V2 , E 2 ) from
Example 4.19
x3 + 1 x4 + 1 x5

yields the IGS (L 3 , ∅, ∅) for F with L 3 = {x1 +1, x2 +1, x3 + x5 , x4 + x5 }. By definition we now have I F = L 3 ,
i.e., a solution of F can be found by solving a system of linear equations.
Note that this is exactly the IGS that is also derived by applying PPlex to (L 0 , V0 , E 0 ) from Example 4.5.

4.4 Decision Heuristics

Before we introduce our main DPLL-Solving Algorithm in the final subsection, we discuss decision heuristics, i.e.,
methods to make good guesses. First of all, let us define what we precisely mean when we talk about decisions.

Definition 4.20 Let F be a formula in 2-XNF, and let G = (L , V, E) be an IGS for F. A decision for G is a tuple
(L 0 , L 1 ) with L 0 , L 1 ⊆ Ln such that the following conditions are satisfied.
(a) L 0 \ LF2 = ∅ and L 1 \ LF2 = ∅.
(b) Z(I F ) ⊆ Z(I F + L 0 ) ∪ Z(I F + L 1 ).

These conditions ensure that guessing either L 0 or L 1 will lead to a solution of F – if there exists one at
all. Moreover, it means that a decision (L 0 , L 1 ) for G = (L , V, E) implies that G 0 = (L ∪ L 0 , V, E) and
G 1 = (L ∪ L 1 , V, E) satisfy G  G 0 and G  G 1 , i.e., both parts of the decision improve our implication graph
structure.
Traditionally, CNF-based SAT solvers use decisions of the form ({xi }, {xi + 1}) or ({xi + 1}, {xi }). Our more
general point of view on decisions allows us to guess multiple linerals at once. Before we explicitly suggest three
decision heuristics, let us consider the following general constructions.

Proposition 4.21 Let σ be a term ordering, let F be a formula in 2-XNF, and let G = (L , V, E) be a σ -reduced
IGS for F.
(a) For every f ∈ V , the tuple (D f , D f +1 ) is a decision for G.
(b) If f 1 → · · · → fr is a path in G then ({ f 1 + f i | i ∈ {2 . . . , r }}, { f 1 + 1, fr }) is a decision for G.

Proof Let f ∈ V . Then the fact that G is σ -reduced yields f, f + 1 ∈ / LF2 . For every a ∈ Z(I F ), we have
f (a) = 1 or f (a) = 0. This shows that ({ f }, { f + 1}) is a decision for G. Now it suffices to note that I F +  f  =
I F +  f = I F + D f F2 by Proposition 4.10 and Remark 4.2.
Next we let f 1 → · · · → fr be a path as in (b). Then we have f 1 + fr , fr ∈ / LF2 , since G is σ -reduced. Consider
a point a ∈ Z(I F ). If (( fr + 1) f 1 )(a) = 1 then fr (a) = 0 and f 1 (a) = 1, i.e., we have a ∈ Z(I F +  f 1 + 1, fr ).
Otherwise, we have (( fr + 1) f 1 )(a) = 0. In this case a is a zero of ( fr + 1) f 1 . Using Proposition 4.10, we deduce
from a ∈ Z(I F ) that a is a zero of ( f i + 1) f j for all i, j ∈ {1, . . . , r } with i < j, as there is a path f i → f j in G.
It follows that ( f i + 1) fr · f 1 + ( fr + 1) f 1 · ( f i + 1) = ( f i + 1) f 1 vanishes at a for all i ∈ {1, . . . , r }. This
shows that the point a is a zero of ( f 1 + 1) f i + ( f i + 1) f 1 = f 1 + f i for all i ∈ {2, . . . , r }. Finally, we get that
a ∈ Z(I F +  f 1 + f i | i ∈ {2, . . . , r }), and the claim follows. 


This proposition allows us to introduce several simple decision heuristics. In the next section, we will see that
they prove quite effective on certain types of inputs.

Remark 4.22 (Decision Heuristics) Let σ be a term ordering, let F be a 2-XNF formula, and let (L , V, E) be a
σ -reduced acyclic IGS.
20 Page 20 of 26 B. Andraschko et al.

MaxReach. Find a source f ∈ V such that the number of paths starting at f ∈ V is maximal. Then we consider
the decision (D f , { f + 1}). Since f is a source, the vertex f has no in-going edges. Thus the skew-symmetry of G
implies that f + 1 has no out-going edges. This yields D f +1 = { f + 1}.
MaxBottleneck. Instead of focusing on the first part of the decisions, another approach is to find f ∈ V such that
the sum of the number of paths ending in f and the number of paths starting at f is maximal. Then we consider
the decision (D f , D f +1 ).
MaxPath. Let f 1 → · · · → fr be a maximal path in (V, E). Then we consider the decision ({ f 1 + f i | 1 ≤ i ≤
r }, { f 1 + 1, fr }). Conceptually speaking, this means that instead of guessing vertices in the graph, we guess the
edge fr → f 1 , i.e., the polynomial ( fr + 1) f 1 . In view of the proof of Proposition 4.21 and of Remark 4.2, this
yields a strongly connected component of (V, E).
While the first two of these heuristics are close to the classical approach to decisions, the MaxPath heuristic is
a rather new one. Note, however, that these heuristics are just some initial suggestions and should be combined
with well-studied heuristics of established CDCL SAT solvers. Unfortunately, the adaptions of those heuristics to
linerals are not straightforward.
The heuristics suggested in the previous remark are designed such that we can compute them efficiently, i.e., in
linear time and space. Let us give some more information on how this can be done.
Remark 4.23 (Efficient Implementation of Decision Heuristics) Recall that a topological ordering of a directed
acyclic graph (V, E) is a linear ordering  of V such that ( f, g) ∈ E implies f  g, and that such an ordering can
be computed in linear time and space [5]. 
MaxReach. For f ∈ V , denote the number of paths starting at f by p f . Then we have p f = 1 + ( f,g)∈E pg
for every f ∈ V . This means that traversing the graph in a reverse topological order once allows us to find p f for
all f ∈ V . In particular, the vertex f ∈ V which maximizes p f can be found in linear time.
MaxBottleneck. Similarly, we can find the number of paths ending in each vertex f ∈ V by a single traversal of
the graph in topological order. Thus the vertex f ∈ V which has the most paths starting and ending in f can be
found by a total of two graph traversals.
MaxPath. For f ∈ V , denote the length of the longest path starting at f by  f . Then we have  f = 1 +
max( f,g)∈E g . The value  f for all f ∈ V can now be computed by a single traversal of the graph in a reverse
topological order. By storing the vertex g ∈ V for which g is largest at every f ∈ V with ( f, g) ∈ E, the path of
length  f starting at f can be recovered in linear time. Altogether, the MaxPath heuristic can be implemented in
linear time and space.

4.5 Graph-Based 2-XNF DPLL-Solving

Finally, we have all the tools at our disposal to present our graph-based 2-XNF solver which is based on the
well-known DPLL-technique [17].

Proposition 4.24 Let F be a formula in 2-XNF with an implication graph structure (L , V, E), and let σ be a
term ordering. Then G_2XNF_ DPLL is an algorithm which returns UNSAT if and only if S(F) = ∅. Otherwise, it
returns an element a ∈ S(F).
Proof First notice that Line 1 ensures that the IGS (L , V, E) is always σ -reduced and acyclic. Hence Line 6 can
be performed efficiently, as explained in Remark 4.23.
Next we show the finiteness of the procedure. In every iteration of Lines 1-3 where L FL = ∅ the IGS (L , V, E)
decreases strictly w.r.t. ≺. By Lemma 4.7, we eventually reach L FL = ∅ in Line 3, and the loop stops after finitely
many steps. For the finiteness of the recursive calls observe that if (L 0 , L 1 ) is a decision for (L , V, E) as in Line 6,
then dimF2 LF2 < dimF2 L ∪ L 0 F2 and dimF2 LF2 < dimF2 L ∪ L 1 F2 . This means that the dimension of LF2
increases strictly with every recursive call. Now it suffices to note that this dimension is bounded from above by
n + 1, and in case dimF2 LF2 = n + 1 we have 1 ∈ LF2 , i.e., the procedure terminates in Line 4.
SAT Solving Using XOR-OR-AND Normal Forms Page 21 of 26 20

Algorithm 8: G_2XNF_ DPLL – Graph-Based 2-XNF DPLL-Solver

Input : An IGS (L , V, E) for a formula F in 2-XNF, a term ordering σ .
Output: UNSAT or an assignment a ∈ S (F).
1 Let (L , V, E) = crGGCPσ (L , V, E). // propagation
2 Let L FL = tFLS(L , V, E) and adjoin L FL to L. // in-processing
3 if L FL = ∅ then go to Line 1.
4 if 1 ∈ LF2 then return UNSAT
5 if E = ∅ then return a ∈ Z (L) ⊆ Fn2 .
6 Use Remark 4.22 to compute a decision (L 0 , L 1 ) for (L , V, E). // decision
7 if G_2XNF_ DPLLσ (L ∪ L 0 , V, E) returns a ∈ Fn2 then return a.
8 else return G_2XNF_ DPLLσ (L ∪ L 1 , V, E).

To prove correctness, note that if the algorithm terminates in Line 4, then F cannot have any solution since
LF2 ⊆ I F . Similarly, if it terminates in Line 5, the implication graph must be empty and we get I F = L, i.e.,
a ∈ Z(L) = Z(I F ) = S(F). Next we show by induction on d that the output in all lines is correct if dimLF2 = d
for d ∈ {0, . . . , n + 1}. Note that dimF2 LF2 = n+1 implies 1 ∈ LF2 ⊆ I F , i.e., the algorithm terminates already
in Line 4 and is correct by the above. Now suppose that the algorithm terminates correctly if dim F2 LF2 > s for some
s ∈ {0, . . . , n} and let dimF2 LF2 = s. It suffices to consider the case where the algorithm terminates in Lines 7 or 8.
Note that by definition of the decision (L 0 , L 1 ) from Line 6 we have Z(I F ) ⊆ Z(I F + L 0 ) ∪ Z(I F + L 1 ), and as
above the dimension of LF2 is strictly smaller than the dimensions of L ∪ L 0 F2 and L ∪ L 1 F2 , respectively. Thus
the recursive call in Line 7 terminates correctly, i.e., returns UNSAT if and only if Z(I F + L 0 ) = ∅, otherwise it
returns a ∈ Z(I F + L 0 ) ⊇ Z(I F ). If the algorithm does not terminate here, then we must have Z(I F + L 0 ) = ∅
and the algorithm terminates with the recursive call in Line 8. Analogous to the call in Line 7, we get UNSAT if and
only if Z(I F + L 1 ) = ∅, which occurs if and only if Z(I F ) ⊆ Z(I F + L 0 ) ∪ Z(I F + L 1 ) = ∅. Otherwise it
returns a satisfying assignment a ∈ Z(I F + L 1 ) ⊇ Z(I F ) = S(F) of F. 

To obtain an efficient implementation we need appropriate data structures which support fast backtracking. The
following method allows us to avoid creating a copy of the entire implication graph structures in the recursive calls
of Lines 7 and 8.
Remark 4.25 (Data Structures for Implication Graph Structures) In order to store an implication graph structure
(L , V, E) internally, it is beneficial to actually store a graph (V  , E  ) based on integer vertices V  ⊆ Z and a map
λ : V  → Ln such that V = λ(V  ) and such that E = { (λ(v), λ(w)) | (v, w) ∈ E  }.
Let us suggest two data structures, one for the labeling map λ, and one for the graph (V  , E  ) which are tailored
towards efficient backtracking.
(a) To efficiently represent λ, we use a prefix tree, i.e., a tree whose non-root vertices are elements of {1, x1 , . . . , xn },
where the children of every node are bigger than their parent w.r.t. a term ordering σ , and where the root is
t0 = 0. Then every vertex v ∈ V  is associated to a vertex η(v) of the tree such that the unique path starting at
the root t0 → · · · → tr = η(v) satisfies λ(v) = t0 + · · · + tr .
Note that insertion can be performed in amortized linear time in the size of Supp(λ(v)) if the children are
accessed by hash maps, and deletion can be performed in constant time. If λ needs to be copied, it suffices to
copy η(v) for every v ∈ V  . The actual linear polynomials λ(v) are not copied. For the backtracking, we simply
replace η internally, and the previous λ is restored immediately.
(b) For the graph itself, we suggest to use a modified lean hybrid graph representation, as devised in [1–3]. This
data structure was proposed only for undirected graphs, but an extension to directed skew-symmetric graphs is
possible. The data structure is rather advanced and allows backtracking of edge deletions and vertex contractions
in constant time. In particular, it allows us to store any state of the graph with a space complexity of O(#V ).
Backtracking to such a previous state has complexity O(#V ).
Altogether, it is possible to implement the algorithm with a space complexity of O((n + 1) · #V + #E), where
(V, E) is part of the initial trivial IGS.
20 Page 22 of 26 B. Andraschko et al.

Notice that G_2XNF_ DPLL is based on the well-known DPLL framework. An extension to a conflict-driven
clause learning (CDCL) directive encounters the following obstacles.

Remark 4.26 (Conflict-Driven XNF Clause Learning) Although the 2-XNF theory originates from the s-Res
proof system which in turn is a generalization of classical resolution, it is not easy to extend conflict-driven clause
learning to 2-XNF instances. This is mainly due to two problems:

(1) The resolvent of two clauses may be the zero clause, i.e., resolving the conflict clause may lead to a clause that
is trivially satisfied [26].
(2) In general, the resolvent is not in 2-XNF, i.e., it cannot be added to the implication graph structure in a straight-
forward way.

Overcoming these obstacles is an important objective of future research, because CDCL techniques promise sig-
nificant speed-ups of XNF solvers.

5 Experiments and Timings

In this section we evaluate the methods of Sect. 4 on random 2-XNF instances and on instances coming from
round-reduced Ascon-128 key-recovery attacks. For comparison, we ran our C++ implementation of Algorithm
G_2XNF_ DPLL, which we named 2-Xornado, against SAT solvers with XOR support, i.e., CNF-based SAT
solvers that can read and process XOR constraints on the variables natively. We say that formulas of the type
processed by these solvers are in CNF-XOR.
State-of-the-art SAT solvers that support CNF-XOR input are CryptoMiniSat [39], an established CDCL-
based solver, and xnfSAT [36], which is based on a stochastic local search approach, i.e., it can only be used on
satisfiable instances. (Note that xnfSAT, despite its name, cannot work with XNFs as introduced in this article. It
only supports CNF-XOR instances.) To use these solvers on XNF instances, we use the following reduction.

Remark 5.1 Let F be a 2-XNF formula involving n variables. Then we can write the XNF clauses of F as C1 , . . . , Cr ,
L 1 , . . . , L s , where Ci = L i,1 ∨ L i,2 with linerals L i, j , and where L 1 , . . . , L s are already linerals. Now we introduce
2r additional variables Yi, j and consider the CNF-XOR formula G consisting of the clauses Ci = Yi,1 ∨ Yi,2 , the
XOR constraints ¬Yi, j ⊕ L i, j for i ∈ {1, . . . , r } and j ∈ {1, 2}, and the original XOR constraints L 1 , . . . , L s . Then
we have Z(F) ≡n Z(G).

Furthermore, a 2-XNF instance can also be seen as a system of quadratic Boolean polynomial equations that
can be solved by an algebraic solver such as PolyBoRi [9]. This package offers an implementation of the Buch-
berger algorithm adapted to Boolean polynomial rings and employs highly optimized data structures. Additionally,
we consider the solver Bosphorus [11], which employs both algebraic and logical reasoning, and processes
ANF (and CNF) input. For instances with fewer than 40 variables, we also compare the solvers to xnf_ bf, our
C++ implementation of a brute-force XNF solver. Finally, we also consider the winner of the 2023 SAT com-
petition SBVA-CaDiCaL [22] which processes CNF inputs. The CNF files were generated from the CNF-XOR
representation by converting the additional XOR constraints on the variables to a set of CNF clauses. Since a direct
encoding of long XORs results in exponentially many CNF clauses, they are split using new variables such that
we only consider direct encodings of XOR constraints involving at most 5 variables. This corresponds to a linear
encoding with cutting number 5 [36].
All experiments were run on an Intel Xeon E5-2623 v3 processor with 128GB of RAM under Debian 10.
We used CryptoMiniSat version 5.8, xnfSAT version 03v, Bosphorus version 3.0, and SBVA-CaDiCaL
with CaDiCaL 2.0 [7].
SAT Solving Using XOR-OR-AND Normal Forms Page 23 of 26 20

Random 2-XNF Clauses

First we consider random 2-XNF instances involving n variables and m clauses. Every clause in the formula is
generated by picking two linerals uniformly at random in Ln \F2 . With m = 3·n and n ∈ {21, . . . , 40}, experiments
showed that such an instance is UNSAT with a probability of at least 98%. If a solution is desired, we simply choose
a ∈ Fn2 at random and for every clause that is not satisfied by a, we randomly flip the constant of one of the
two linerals. This ensures that a indeed forms a satisfying assignment of the generated 2-XNF instance. Two
random benchmark suites are considered, each containing 400 random instances with n ∈ {21, . . . , 40} variables
in m = 3 · n clauses, where we have 20 instances for every n. One set contains only satisfiable instances, the other
only unsatisfiable ones.
The cactus plots in Fig. 4 show that such small random instances are hard for state-of-the-art CNF and CNF-XOR
solvers. In particular, we see that xnfSAT and SBVA-CaDiCaL are even out-performed by a simple brute-force
implementation. Algebraic solving with PolyBoRi performs not significantly worse than CryptoMiniSat.
While the plot clearly shows that 2-Xornado performs best on this benchmark, one should note that this is
not due to some clever data structures that allow very fast propagation. The main reason for its better overall
performance is that the required number of decisions of 2-Xornado (with any heuristic) is smaller by a factor of
60-80 compared to the number of decisions taken by CryptoMiniSat.

Round-Reduced Ascon Key Recovery Attacks

Our second benchmark set consists of instances related to key-recovery attacks on round-reduced versions of the
cipher Ascon-128 [18]. In particular, we consider attacks where the 128-bit nonce and the 320-bit internal state
are known and the goal is to undo the initialization step consisting of 12 rounds in order to obtain the 128-bit secret
key. If this problem can be solved efficiently, the cipher is broken in a nonce-misuse scenario, see [6]. Here we
consider round-reduced variants: 20 instances with 2 rounds, 20 instances with 3 rounds and knowledge of the
first k key bits for each k ∈ {55, . . . , 64}, and 20 instances with 4 rounds and knowledge of the first k key bits for
each k ∈ {92, . . . , 100}. The instances were generated by applying QANFto2XNF to a polynomial representation
of the cryptosystem, see Example 3.22, augmented with some additional XNF clauses, which speed up propagation
in GGCP.
Figure 5 contains a cactus plot for these cryptographic instances. Here xnfSAT was not included due to its
bad performance on the random set. It turns out that for the 2-round version 2-Xornado can already solve all
instances (starting with the trivial IGS) during pre-processing in less than 0.3 s on average. On these instances,
CryptoMiniSat requires more than 80 000 decisions and several seconds; and SBVA-CaDiCaL about 20 000
decisions and one second. Our solver 2-Xornado with the MaxBottleneck or the MaxReach heuristic and in-
processing with tFLS also performs very well on the remaining benchmark and comes out as the average best
solver. The bad performance with the MaxPath heuristic may be attributed to the fact that the corresponding decision
linerals contain more variables and therefore crGGCP execution requires more time, increases the average length of
linerals of the implication graph vertices, i.e., increases its memory footprint, and thereby makes backtracking more
expensive. It should be noted that on the 4-round instances the CNF-XOR solver CryptoMiniSat had a better
performance with fewer timeouts. So its advanced decision heuristics, the highly optimized data structures, and the
conflict-learning methods do pay off on larger instances. Nonetheless 2-Xornado still requires fewer decisions
by a factor of 60-80. The CNF-SAT solver SBVA-CaDiCaL, however, with data structures and conflict-learning
methods similar to CryptoMiniSat could only solve 8 of these instances. This highlights the effectiveness of the
encodings of these innately XOR-rich problems in CNF-XOR and XNF. Also note that PolyBoRi could not solve
a single instance when given in its ANF format, however when feeding it with the system of quadratic equations
corresponding to the 2-XNF, some instances could be solved. The situation for Bosphorus is similar, with better
performance on the input that comes from our XNF encoding.
20 Page 24 of 26 B. Andraschko et al.

1000
2-Xornado MaxPath (2-XNF)
2-Xornado MaxReach (2-XNF)
800 2-Xornado MaxBottleneck (2-XNF)
CryptoMiniSat (CNF-XOR)
PolyBoRi (ANF)
CPU time (s)

600 SBVA-CaDiCaL (CNF)

Bosphorus (CNF-XOR)
xnf bf (2-XNF)
400 xnfSAT (CNF-XOR)

200

0
0 50 100 150 200 250 300 350 400
instances

1000
2-Xornado MaxPath (2-XNF)
2-Xornado MaxReach (2-XNF)
800 2-Xornado MaxBottleneck (2-XNF)
CryptoMiniSat (CNF-XOR)
PolyBoRi (ANF)
CPU time (s)

600 SBVA-CaDiCaL (CNF)

Bosphorus (CNF-XOR)
xnf bf (2-XNF)
400

200

0
0 50 100 150 200 250 300 350 400
instances

Fig. 4 Cactus plots for the random benchmark suites

Conclusions

A generalization of the well-known CNF that allows compact representations of XOR-rich problems, like those
originating from cryptographic attacks, has been introduced. On top of that we generalized pre- and in-processing
techniques and introduced a DPLL-based solving algorithm with a simplistic decision heuristic that outperforms
other state-of-the-art solving approaches on random instances and on problems originating from cryptographic
attacks on Ascon-128. An extension to CDCL-based solving is in preparation and better decision heuristics will
be investigated.
SAT Solving Using XOR-OR-AND Normal Forms Page 25 of 26 20

1000
2-Xornado MaxPath (2-XNF)
2-Xornado MaxReach (2-XNF)
800 2-Xornado MaxBootleneck (2-XNF)
CryptoMiniSat (CNF-XOR)
PolyBoRi (2-XNF)
CPU time (s)

600 SBVA-CaDiCaL (CNF)

Bosphorus (ANF)
Bosphorus (2-XNF)
400

200

0
0 50 100 150 200 250 300 350 400
instances
Fig. 5 Cactus plot for the benchmark suite consisting of 400 satisfiable instances related to key-recovery attacks on round-reduced
Ascon-128

Acknowledgements During part of this research, the second author was supported by the DFG project Algebraische Fehlerangriffe
KR 1907/6-2. The first author gratefully acknowledges Cusanuswerk e.V. for financial support.

Funding Open Access funding enabled and organized by Projekt DEAL.

Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s)
and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party
material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material.
If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or
exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit
[Link]

References

1. Abu-Khzam, F.N., Jahed, K.A., Mouawad, A.E.: A hybrid graph representation for exact graph algorithms, preprint 2014, available
at arXiv:1404.6399 (accessed on 23 February 2023)
2. Abu-Khzam, F.N., Kim, D., Perry, M., Wang, K., Shaw, P.: Accelerating vertex cover optimization on a GPU architecture. In: Int.
Symposium on Cluster, Cloud and Grid Computing (CCGRID), Washington 2018, IEEE Xplore, pp.616–625
3. Abu-Khzam, F.N., Langston, M.A., Nolan, C.P.: A hybrid graph representation for recursive backtracking algorithms. In Frontiers
in Algorithmics (FAW 2010), LNCS 6213, Springer-Verlag, Berlin 2010, pp. 136–147
4. Albrecht, M., Cid, C., Grassi, L., Khovratovich, D., Lüftenegger, R., Rechberger, C., Schofnegger, M.: Algebraic cryptanalysis of
STARK-friendly designs: application to MARVELlous and MiMC, in: Proc. Advances in Cryptology (ASIACRYPT 2019), Kobe
2019, LNCS 11923, Springer Int. Publ., Cham 2019, pp. 371–397
5. Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inform.
Process. Lett. 8, 121–123 (1979)
6. Baudrin, J., Canteaut, A., Perrin, L.: Practical cube attack against nonce-misused Ascon. IACR Trans. Symm. Cryptol. 4, 120–144
(2022)
7. Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0, In: Proc. Computer Aided Verification (CAV
2024), Montreal 2024, LNCS 14681, Springer Nature Switzerland, Cham, pp. 133–152 (2024)
8. Brickenstein, M.: Boolean Gröbner Bases, Springer-Verlag, Berlin 2010
9. Brickenstein, M., Dreyer, A.: PolyBoRi: A framework for Gröbner-basis computations with Boolean polynomials. J. Symbolic
Comput. 44, 1326–1345 (2009)
10. Castryck, W., Decru, T.: An efficient key recovery attack on SIDH, In: Proc. Advances in Cryptology (EUROCRYPT 2023); Lyon
2023, LNCS 14008, Springer Int. Publ., Cham, pp. 423–447 (2023)
20 Page 26 of 26 B. Andraschko et al.

11. Choo, D., Soos, M., Chai, M.A., Meel, K.S.:Bosphorus: Bridging ANF and CNF solvers, In: Proc. Design, Automation, and Test
in Europe (DATE), Florence 2019, IEEE Xplore, pp. 468–473
12. Courtois, N., Klimov, A., Patarin, J., Shamir, A.: Efficient algorithms for solving overdefined systems of multivariate polynomial
equations. In: Proc. Advances in Cryptology (EUROCRYPT 2000), Brugge 2000, LNCS 1807, Springer-Verlag, Berlin 2000, pp.
392–407
13. Courtois, N., Sepehrdad, P., Sušil, P., Vaudenay, S.: The ElimLin algorithm revisited. In: Proc. Fast Software Encryption (FSE
2012), Washington 2012, LNCS 7549, Springer-Verlag, Berlin 2012, pp. 306–325
14. Danner, J., Kreuzer, M.: A fault attack on KCipher-2. Int. J. Comput. Math. Comput. Syst. Theory 6, 281–312 (2021)
15. Dash, S.K., Scholz, S.-B., Herhut, S., Christianson, B.: A scalable approach to computing representative lowest common ancestor
in directed acyclic graphs. Theoret. Comput. Sci. 513, 25–37 (2013)
16. Davies, J.: Solving MAXSAT by Decoupling Optimization and Satisfaction, Dissertation. University of Toronto, Toronto (2013)
17. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394–397 (1962)
18. Dobraunig, C., Eichlseder, M., Mendel, F., Schläffer, M.: Ascon v1.2: Technical report, National Institute of Standards and Tech-
nology (2019)
19. Dudek, J.M., Meel, K.S., Vardi, M.Y.: The hard problems are almost everywhere for random CNF-XOR formulas. In: Proc. Int.
Joint Conference on Artificial Intelligence (IJCAI’17), Melbourne (2017) pp. 600–606
20. Dwivedi, A.D., Klouček, M., Morawiecki, P., Nikolić, I., Pieprzyk, J., Wójtowicz, S.: SAT-based cryptanalysis of authenticated
ciphers from the CAESAR competition. In: Proc. Int. Joint Conference on e-Business and Telecommunications (ICETE 2017),
SECRYPT, Madrid, 2017; pp. 237–246
21. Emdin, G., Kulikov, A.S., Mihajlin, I., Slezkin, N.: CNF Encodings of Symmetric Functions. Theory Comput. Sys. (2024)
22. Haberlandt, A., Green, H., Heule, M.J.H.: Effective auxiliary variables via structured reencoding. In: Proc. Theory and applications
of satisfiability testing (SAT 2023), Alghero 2023, LIPIcs 271, Leibniz-Zentrum für Informatik, Dagstuhl 2023, pp. 11:1–11:19
23. Hadipour, H., Eichlseder, M.: Autoguess: a tool for finding guess-and-determine attacks and key bridges, in: Proc. Applied Cryp-
tography and Network Security (ACNS 2022), Rome 2022, LNCS 13269, Springer Nature Switzerland, Cham 2022, pp. 230–250
24. Han, C.S., Jiang, J.H.R.: When Boolean satisfiability meets Gaussian elimination in a simplex way. In: Proc. Computer Aided
Verification (CAV 2012), Berkeley 2012, LNCS 7358, Springer-Verlag, Berlin 2012, pp. 410–426
25. Heule, M.J.H., Matti, J., Biere, A.: Revisiting hyper binary resolution. In: Integration of AI and OR techniques in constraint
programming for combinatorial optimization problems (CPAIOR 2013), LNCS 7874, Springer-Verlag, Berlin (2013) pp. 77–93
26. Horáček, J.: Algebraic and Logic Solving Methods for Cryptanalysis, Dissertation. Universität Passau, Passau (2020)
27. Horáček, J., Kreuzer, M.: Refutation of products of linear polynomials. In: Proc. Third Int. Workshop on Satisfiability Checking
and Symbolic Computation (SC2 ), Oxford (2018) [Link]
28. Horáček, J., Kreuzer, M.: On conversions from CNF to ANF. J. Symbolic Comput. 100, 164–186 (2020)
29. Jovanovic, P., Kreuzer, M.: Algebraic attacks using SAT-solvers. Groups Complex. Cryptol. 2, 247–259 (2010)
30. Kreuzer, M., Robbiano, L.: Computational Commutative Algebra 1. Springer-Verlag, Berlin (2000)
31. Lafitte, F., Nakahara, J., Van Heule, D.: Applications of SAT solvers in cryptanalysis: finding weak keys and preimages. J. Satisf.
Boolean Model. Comput. 9, 1–25 (2014)
32. Laitinen, T., Junttila, T., Niemelä, I.: Conflict-Driven XOR-Clause Learning. In: Proc. Theory and Applications of Satisfiability
Testing (SAT 2012), Trento 2012, LNCS 7317, Springer-Verlag, Berlin 2012, pp. 383–396
33. Leventi-Peetz, A., Zendel, O., Lennartz, W., Weber, K.: CryptoMiniSat switches-optimization for solving cryptographic instances.
In: Proc. Pragmatics of SAT 2015 and 2018, EPiC Series in Computing 59, EasyChair 2019, pp. 79–93
34. Mironov, I., Zhang, L.: Applications of SAT solvers to cryptanalysis of hash functions. In: Proc. Theory and applications of
satisfiability testing (SAT 2006), Seattle 2006, LNCS 4121, Springer-Verlag, Berlin (2006) pp. 102–115
35. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. Design
Automation Conference (DAC), Las Vegas 2001, ACM, New York 2001, pp. 530–535
36. Nawrocki, W., Liu, Z., Fröhlich, A., Heule, M.J.H., Biere, A.: XOR local search for Boolean brent equations. In: Theory and
applications of satisfiability testing (SAT 2021), LNCS 12831, Springer Nature Switzerland, Cham 2021, pp. 417–435
37. Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. J. Automat. Reason. 64, 423–460 (2020)
38. Soos, M., Meel, K.S.: BIRD: Engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting.
In: Proc. AIII conference on artificial intelligence 2019, vol. 33, AIII Press, Palo Alto 2019, pp. 1592–1599
39. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Theory and applications of satisfiability
testing (SAT 2009), LNCS 5584, Springer-Verlag, Berlin 2009, pp. 244–257
40. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1, 146–160 (1972)
41. Trimoska, M., Ionica, S., Dequen, G.: Parity (XOR) reasoning for the index calculus attack. In: Proc. principles and practice of
constraint programming (CP 2020), Louvain-la-Neuve 2020, Springer Int. Publ., Cham 2020, pp. 774–790

Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.