*Example 37.* For the remaining ADP problem ({(20)}, {(22)} ∪ (A1(RdivL) \ {(20)})) from Example 34, we can apply the reduction pair processor using the polynomial interpretation from the end of Sect. 3.1 which maps 0 and nil to 0, s(x) to x + 1, cons(y, *xs*) to *xs* + 1, DL(x, *xs*) to *xs*, and all other symbols to their first arguments. Then, (20) is oriented strictly (i.e., it is in P), and (22) and all other base ADPs are oriented weakly. Hence, we remove the annotation from (20) and move it to the base ADPs. Now there is no main ADP anymore, and thus the dependency graph processor returns ∅. This proves SN for (A1(RdivL), A2(Bmset2)), hence RdivL/Bmset2 is also SN.

*Example 38.* Regard the ADPs a → b and f → d(F,A) for the redex-creating Example 4 again. When using a polynomial interpretation Pol that maps c0 to 0 and c2(x, y) to x + y, then for the reduction pair processor one has to satisfy Pol(A) ≥ 0 and Pol(F) ≥ Pol(F)+Pol(A), i.e., one cannot make any of the ADPs strictly decreasing.

In contrast, for the variant with the terminating base rule f(s(y)) → d(f(y), a) from Example 28, we have the ADPs a → b and f(s(y)) → d(F(y),A). Here, the second constraint is Pol(F(s(y))) ≥ Pol(F(y))+Pol(A). To make one of the ADPs strictly decreasing, one can set Pol(F(x)) = x, Pol(s(x)) = x+ 1, and Pol(A)=1 or Pol(A) = 0. Then the reduction pair processor removes the annotations from the strictly decreasing ADP and the dependency graph processor proves SN.

#### **6 Evaluation and Conclusion**

In this paper, we introduced the first notion of (annotated) dependency pairs and the first DP framework for relative termination, which also features suitable dependency graph and reduction pair processors for relative ADPs. Of course, further classical DP processors can be adapted to our relative ADP framework as well. For example, in our implementation of the novel ADP framework in our tool AProVE [13], we also included a straightforward adaption of the classical *rule removal processor* [11], see [24].8 While the soundness proofs for the processors in the new relative ADP framework are more involved than in the standard DP framework, the new processors themselves are quite analogous to their original counterparts and thus, adapting an existing implementation of the ordinary DP framework to the relative ADP framework does not require much effort. In future work, we will investigate how to use our new form of ADPs for full (instead of innermost) rewriting also in the probabilistic setting and for complexity analysis.

To evaluate the new relative ADP framework, we compared its implementation in "*new* AProVE" to all tools that participated in the most recent *termination competition (TermComp 2023)* [14] on relative rewriting, i.e., NaTT [36], TTT2 [27], MultumNonMulta [9], and "*old* AProVE" which did not yet contain the contributions of the current paper. In *TermComp 2023*, 98 benchmarks were used for relative termination. However, these benchmarks only consist of examples where the main TRS R dominates the base TRS B (i.e., which can be handled by Theorem 11 from [21]) or which can already be solved via simplification orders directly.

Therefore, we extended the collection by 32 new "typical" examples for relative rewriting, including both RdivL/Bmset from Examples 1 and 2, and our leading example RdivL/Bmset2 from Examples 2 and 14 (where only *new* AProVE can prove SN). Except for RdivL/Bmset, in these examples R does not dominate B. Most of these examples adapt well-known classical TRSs from the *Termination Problem Data Base* [33] used at *TermComp* to the relative setting. Moreover, 5 of our new examples illustrate the application of relative termination for proving confluence, i.e., in these examples one can prove confluence with the approach of [19] via our new technique for relative termination proofs.

In the following table, the number in the "YES" ("NO") row indicates for how many of the 130 examples the respective tool could prove (disprove) relative termination and "MAYBE" refers to the benchmarks where the tool could not

8 This processor works analogously to the preprocessing at the beginning of Sect. 4 which can be used to remove duplicating rules: For an ADP problem (P, S), it tries to find a reduction pair (-, ) where is closed under contexts such that -(P∪S) ⊆ -. Then for P ⊆ P∪S with -(P) ⊆ , the processor replaces the ADP by (P\P, S\P).

solve the problem within the timeout of 300 s per example. The numbers in brackets are the respective results when only considering our new 32 examples. "AVG(s)" gives the average runtime of the tool on solved examples in seconds.

The table clearly shows that while *old* AProVE was already the second most powerful tool for relative termination, the integration of the ADP framework in *new* AProVE yields a substantial advance in power (i.e., it only fails on 26 of the examples, compared to 57 and 69 failures of NaTT and *old* AProVE, respectively). In particular, previous tools (including *old* AProVE) often have problems with relative TRSs where the main TRS does not dominate the base TRS, whereas the ADP framework can handle such examples.

A special form of relative TRSs are *relative string rewrite systems (SRSs)*, where all function symbols have arity 1. Due to the base ADPs with two annotated symbols on the right-hand side, here the ADP framework is less powerful than dedicated techniques for string rewriting. For the 403 relative SRSs at *TermComp 2023*, the ADP framework only finds 71 proofs, mostly due to the dependency graph and the rule removal processor, while termination analysis via AProVE's standard strategy for relative SRSs succeeds on 209 examples, and the two most powerful tools for relative SRSs at *TermComp 2023* (MultumNonMulta and Matchbox [35]) succeed on 274 and 269 examples, respectively.

Another special form of relative rewriting is *equational rewriting*, where one has a set of equations E which correspond to relative rules that can be applied in both directions. In [10], DPs were adapted to equational rewriting. However, this approach requires E-unification to be decidable and finitary (i.e., for (certain) pairs of terms, it has to compute finite complete sets of E-unifiers). This works well if E are AC- or C-axioms, and for this special case, dedicated techniques like [10] are more powerful than our new ADP framework for relative termination. For example, on the 76 AC- and C-benchmarks for equational rewriting at *TermComp 2023*, the relative ADP framework finds 36 proofs, while dedicated tools for AC-rewriting like AProVE's equational strategy or MU-TERM [15] succeed on 66 and 64 examples, respectively. However, in general, the requirement of a finitary E-unification algorithm is a hard restriction. In contrast to existing tools for equational rewriting, our new ADP framework can be used for arbitrary (non-duplicating) relative rules.

For details on our experiments, our collection of examples, and for instructions on how to run our implementation in AProVE via its *web interface* or locally, see: https://aprove-developers.github.io/RelativeDTFramework/.

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.

# Solving Quantitative Equations

Georg Ehling(B) and Temur Kutsia

RISC, Johannes Kepler University Linz, Linz, Austria<EMAIL_ADDRESS>
Abstract. Quantitative equational reasoning provides a framework that extends equality to an abstract notion of proximity by endowing equations with an element of a quantale. In this paper, we discuss the unification problem for a special class of shallow subterm-collapse-free quantitative equational theories. We outline rule-based algorithms for solving such equational unification problems over generic as well as idempotent Lawvereian quantales and study their properties.

Keywords: Quantitative equational reasoning · Lawvereian quantales · Equational unification

# 1 Introduction

Extending the equality predicate to a notion that expresses similarity or proximity is a task that has been addressed in various ways. While fuzzy reasoning [8,23] approaches this endeavor by equipping equations with real numbers between 0 and 1 to express the degree to which they hold true, quantitative algebraic reasoning [4,17] follows a more proximity-oriented approach, attempting to establish a notion of distance between two terms.

Recently, Gavazzo and Di Florio [12] introduced a framework of metric and quantitative equational reasoning that generalizes these approaches (with a slight modification). It is based on the idea of modeling abstract quantities in quantales [22], following Lawvere's fundamental work [16]. In this framework, equations between terms are endowed with an element of a Lawvereian quantale that expresses, in one sense or another, the degree to which they hold true. The exact meaning of this degree depends on the choice of the quantale; for instance, it could correspond to the distance of two terms in a metric space, or to the probability that the terms are equal. This approach is quite general and includes various known quantitative theories as special cases.

In recent years, quantitative and approximate techniques have become increasingly popular due to various applications. In these applications, e.g., in those related to reasoning about probabilistic computations [5], reasoning about privacy and security of systems [1,21], reasoning about resource consumption during computation [7], approximate program transformations [13], etc. equalities are replaced with their quantitative approximations to model distances between programs, processes, or systems, resulting in metric-based approximate relations. Various techniques have been used to model such metric reasoning principles, among them quantitative equational logic, discussed in [3,4,17,18].

In this paper, we address one of the central problems in equational reasoning: unification (or solving equations). We approach this problem in the framework as described in [12], studying a generalization of classical unification to solving equations in a quantitative equational theory in Lawvereian quantales.

The theories we consider in this paper are induced by shallow subtermcollapse-free equations of a special form, between terms whose arguments are the same sequence of variables, e.g. f(x1,...,xn) and g(x1,...,xn). This is a natural first step toward investigating quantitative equational unification since such quantitative equations generalize the principle of "extending proximity between function symbols to proximity between terms" of unification in the fuzzy quantale to unification in an arbitrary Lawvereian quantale. Despite their simple form, such theories still pose several challenges (originating from, e.g., tensor-based transitivity or extending proximity between arguments to whole terms), which affect the notions of completeness and minimality of unifier sets. We redefine these notions and show that unification (modulo the abovementioned theories) in arbitrary Lawvereian quantale is finitary, while for idempotent Lawvereian quantales, it becomes unitary. We develop the corresponding unification algorithms and study their properties. Due to space limitations, we refer to the more detailed technical report [10] for some of the proofs.

# 2 Preliminaries

We start by introducing the basic notions and fixing the terminology.

*Quantales.* For the notions in this part, we follow [11,12].

Definition 1 (Quantale). *A (unital)* quantale **˙** = (Ω, -, ⊗, κ) *consists of a monoid* (Ω, k, ⊗) *and a complete lattice* (Ω, -) *(with join* ∨ *and meet* ∧*) satisfying the following distributivity laws:* δ ⊗ - i∈I εi = i∈I (δ ⊗ εi) *and* - i∈I εi ⊗ δ = i∈I (εi ⊗ δ)*.*

The element κ is called the *unit* of the quantale, and ⊗ is called its *tensor* (or multiplication). Besides κ, we use Greek letters ε, δ, η, ζ, ι, and ω to denote elements of Ω. The *top* and *bottom* elements of a quantale are denoted by and ⊥, respectively. Quantales in which the unit κ coincides with are called *integral quantales*. A quantale is *commutative* if its underlying monoid is. It is *non-trivial* if κ = ⊥. It is *cointegral* if ε ⊗ δ = ⊥ implies either ε = ⊥ or δ = ⊥.

We assume our quantales are commutative, integral, cointegral, and nontrivial. Such quantales are called *Lawvereian*. (Note that the fuzzy quantale **I** is Lawvereian for the Gödel and product T-norms, but not for the Łukasiewicz T-norm.)

Tensors in quantales always have left and right *adjoints*. For commutative quantales, these adjoints are the same, defined as ε δ := {η | ε ⊗ η δ}.

Table 1. Correspondence between quantales **˙** (generic), **2** (Boolean), **L** (Lawvere), **L**max (strong Lawvere), and **I** (fuzzy).

An element ι ∈ Ω is an *idempotent element* (or simply an *idempotent*) of a quantale **˙** if it satisfies ι ⊗ ι = ι. A quantale is called *idempotent* if every element is idempotent. Among the quantales in Table 1, the idempotent ones are **2**, **L**max, and **I** for the minimum (Gödel) T-norm.

In any Lawvereian quantale, (i) ⊗ is monotonous: α β ⇒ α ⊗ γ β ⊗ γ (using distributivity: (α ⊗ γ)∨(β ⊗ γ)=(α∨β) ⊗ γ = β ⊗ γ); (ii) α ⊗ β α∧β (using monotonicity and integrality: α ⊗ β α ⊗ = α).

Given a quantale **˙** and ε, δ ∈ Ω, the *way-below relation* is defined as δ ε iff for every Ψ ⊆ Ω, if ε - Ψ then there exists a finite subset Ψ0 ⊆ Ψ such that δ- Ψ0. A quantale **˙** is called *continuous* if ε = δε δ for all ε ∈ Ω.

Definition 2 (**˙**-relations, **˙**-ternary relations). *An* **˙**-relation R *between sets* A *and* B *is a function* R: A×B → Ω*. For any set* A*, the identity* **˙***-relation* ΔA : A × A → Ω *maps the diagonal elements* (a, a) *to* κ*, and all other elements to* ⊥*. The composition* (R; S): A × C → Ω *of two* **˙***-relations* R: A × B → Ω *and* S : B × C → Ω *is defined as* (R; S)(a, c) := b∈B - R(a, b) ⊗ S(b, c) *.*

*An* **˙**-ternary relation *over* A × B *is a ternary relation* R ⊆ A × Ω × B *such that* R(a, ε, b) *implies* R(a, δ, b) *for any* δ ε*.*

*Any* **˙***-ternary relation* R *induces an* **˙***-relation* R•(a, b) := R(a,ε,b) ε*, and any* **˙***-relation* R *induces an* **˙***-ternary relation* R◦(a, ε, b) :⇐⇒ ε - R(a, b)*. Moreover, we have* R•◦ = R◦• = R*, and we can freely switch between* **˙***-ternary relations and* **˙***-relations.*

The complete lattice structure of **˙** lifts to **˙**-relations pointwise, and we can say that an **˙**-relation R on A × A is reflexive if ΔA - R; transitive if (R; R) - R; symmetric if R− - R (where R− is defined as R−(b, a) := R(a, b)). Thus, we get the notions of a preorder (i.e., reflexive and transitive) and equivalence (i.e., reflexive, transitive, and symmetric) **˙**-relation.

*Terms and Substitutions.* We assume that the reader is familiar with the standard notions of unification theory, see, e.g., [2]. A *signature* F is a set of function symbols, each equipped with a fixed nonnegative arity. The set of *terms* over a signature F and a set of variables V is denoted by T(F, V). Given a term t ∈ T(F, V), we denote by V(t) the set of variables appearing in t. A term is *ground* if it contains no variables. The notion of a *position* in a term is defined in the standard way.

The set of *leaves* of a term is defined as (e) := {e}, if e is a constant symbol or a variable, and (f(t1,...,tn)) := n i=1 (ti). (The leaves of a term t correspond to the leaves of the tree representing t.) If s is a subterm of t, then the *depth of* s *in* t as the minimal length of a position at which s occurs in t.

A *substitution* is a map σ : V → T(F, V) which maps all but finitely many variables to themselves. Greek letters σ, ϕ, ϑ, τ are used for them, while *Id* denotes the identity substitution. The set of substitutions is denoted by *Sub*. We use the set notation for substitutions, writing σ explicitly as a finite set {x → σ(x) | x = σ(x)}. The *domain* of σ is defined as *dom*(σ) := {x | x = σ(x)}. A substitution σ extends naturally to an endomorphism on T(F, V). The image of a term t under this endomorphism is denoted tσ.

# 3 Quantitative Equational Theories

We now fix a signature F, a set of variables V, and a Lawvereian quantale **˙**.

Let ≈E be an **˙**-ternary relation, assumed to be induced from a given set E of triples (t, ε, s), which we write as ε t ≈E s (called **˙**-equalities). A *quantitative equational theory* (or **˙***-equational theory*) =E is an **˙**-ternary relation generated from ≈E by the rules in Fig. 1. We call E a *presentation* of =E. Informally, we read ε t =E s as "t and s are at most ε-apart modulo E" or "t and s are equal modulo E with degree ε".

Fig. 1. Quantitative equational theory

Observe that the **˙**-relation =• E induced from =E (i.e., t =• E s := εt=*E*s ε) is a reflexive, symmetric, transitive quantitative relation that contains ≈• E and where function symbols and substitutions behave in a non-expansive way:

$$\begin{aligned} \left(t\_1 =\_E^\bullet s\_1 \otimes \cdots \otimes t\_n =\_E^\bullet s\_n\right) & \stackrel{\bullet}{\sim} \left(f(t\_1, \ldots, t\_n) =\_E^\bullet f(s\_1, \ldots, s\_n)\right),\\ \left(t =\_E^\bullet s\right) & \stackrel{\bullet}{\sim} \left(t\sigma =\_E^\bullet s\sigma\right). \end{aligned}$$

We will often slightly abuse terminology by calling both =• E and a presentation E a quantitative equational theory.

The rules in Fig. 1 were introduced in [11] with the aim of generalizing previous approaches to quantitative reasoning [4,17]. This generalization is achieved up to a slight modification of the (NExp) rule, whose analogue in [17] would feature the join of ε1,...,εn rather than their tensor product.1

It should further be remarked that the (Join) rule also applies to an empty hypothesis, whence ⊥ t =E s holds for any t and s. The infinitary (Arch) rule is needed to guarantee the semantic completeness of the deduction system in [17], but has no effect on =E whenever the presentation E is finite, whence it can be safely ignored in that case.

Analogous to classical equational theories, an **˙**-equation ε t = s, where s is a proper subterm of t, is called a *subterm-collapse equation*. A quantitative equational theory E is said to be *simple* (or *subterm-collapse-free*) if whenever ε t =E s with ε = ⊥ holds, the equation ε t = s is not subterm-collapsing. An equation ε t = s is called *shallow* [6] if the depth of each variable occurrence in t or in s is at most 1. An equational theory is called shallow if each equation in its presentation is shallow.

Definition 3. *Let* E *be an* **˙***-equational theory and* X *be a set of variables. A ternary relation* E,X ⊆ *Sub* × Ω × *Sub is defined as*

E,X (σ, ε, ϑ) *iff there exists a* ϕ *such that* ε xσϕ =E xϑ *for all* x ∈ X *.*

*In this case, we say that the substitution* σ is more general than ϑ modulo E on X up to ε*. We shortly write* σ E,X ,ε ϑ *and call* ϑ *an* (E, X , ε)-instance *of* σ *(or an* (E, X )*-instance with degree* ε*).*

It is not hard to see that E,X is an **˙**-ternary relation over *Sub* × *Sub*. To show this, we need to prove that σ E,X ,ε ϑ implies σ E,X ,δ ϑ for any δ ε, which follows from the definition of =E.

Lemma 1. *If* σ E,X ,ε ϑ *and* ϑ E,Y,δ ψ*, then* σ E,X ∩Y,ε⊗δ ψ*.*

*Proof.* By definition of E,X and E,Y , we have ε xσϕ1 =E xϑ for all x ∈ X , and δ yϑϕ2 =E yψ for all y ∈ Y. From these equalities, for all z ∈X ∩Y by the Subst rule we get ε zσϕ1ϕ2 =E zϑϕ2 and δ zϑϕ2 =E zψ. Therefore, by ⊗-transitivity (the Trans rule) we obtain ε⊗δ zσϕ1ϕ2 =E zψ for all z ∈ X ∩Y, which, by definition of E,X ∩Y , gives σ E,X ∩Y,ε⊗δ ψ.

1 The reason for this modification in [11] is that (NExp) should be compatible with (Trans), which is based on the tensor rather than the join. Without it, one would obtain a system where performing various transformation steps one after the other would lead to a different distance than performing the same steps in parallel.

Corollary 1. *If* σ E,X ,ε ϑ *and* ϑ E,X ,δ ψ*, then* σ E,X ,ε⊗δ ψ*.*

Theorem 1. *Given a set of* **˙***-equalities* E *and a set of variables* X *, the* **˙** *relation* • E,X *induced by* E,X *is a preorder on Sub.*

*Proof.* We should show that • E,X is reflexive and transitive.

The equivalence relation on substitutions induced by E,X is denoted by ∼=E,X . It is an **˙**-ternary relation. We write σ ∼=E,X ,ε ϑ if ε - (σ ∼=• E,X ϑ).

*Example 1.* Let **˙** be the Lawvere quantale **L** = ([0,∞], , +, 0) and consider E = {1 a ≈ b, 1 b ≈ c}, ε = 2 and X = {x}. Let σ = {x → a}, ϑ = {x → b}, and ϕ = {x → c}. Then we have:

Hence, σ ∼=E,X ,ε ϑ, ϑ ∼=E,X ,ε ϕ, and σ ∼=E,X ,ε ϕ.

Theorem 2. *Given* E*,* X *,* t*, and* s *such that* V(t)∪ V(s) ⊆ X *, let* R *denote* =• E *and* S *denote* • E,X *. Assume* σ *and* ϑ *are substitutions such that* R(tσ, sσ) = ε *and* S(σ, ϑ) = δ*. Then* ε ⊗ ⊗n+m i=1 δ - R(tϑ, sϑ)*, where* n *and* m *are the number of occurrences of variables from* X *in* t *and* s*, respectively.*

*Proof.* From S(σ, ϑ) = δ we know that there exists ϕ such that δ - R(xσϕ, xϑ) holds for all x ∈ X . From this, by structural induction over terms, we can prove ⊗n i=1δ - R(tσϕ, tϑ) and ⊗m i=1δ - R(sσϕ, sϑ). From R(tσ, sσ) = ε we get ε - R(tσϕ, sσϕ). Applying transitivity twice we get ε ⊗ ⊗n+m i=1 δ -R(tϑ, sϑ).

*Example 2.* In the Boolean quantale **2**, this theorem implies the well-known fact that if σ is a unifier of t and s and ϑ is an instance of σ, then ϑ is also a unifier of t and s. (In that case, ε = δ = 1.)

Consider the fuzzy quantale **I** with the minimum T-norm, E = {0.5 a ≈ b, 0.7 b ≈ c}, t = f(x, x, y), s = f(y, b, c), X = {x, y}, σ = {x → b, y → b}, and ϑ = {x → a, y → c}. Then 0.5 a =E c and

$$\begin{aligned} t\sigma &= f(b, b, b), \quad s\sigma = f(b, b, c), \quad \varepsilon = 0.7, \qquad 0.7 \Vdash t\sigma =\_E s\sigma; \\ \delta &= 0.5, \qquad \sigma \lessapprox\_{E, \{x, y\}, 0.5} \vartheta \text{ (actually, } \sigma \cong\_{E, \{x, y\}, 0.5} \vartheta\text{)}; \\ t\vartheta &= f(a, a, c), \quad s\vartheta = f(c, b, c); \\ \text{Variables of } \mathcal{X} \text{ occur in } t \text{ and } s \text{ in total 4 times;} \\ \min(0.7, 0.5, 0.5, 0.5, 0.5) &= 0.5; \qquad 0.5 \Vdash t\vartheta =\_E s\vartheta. \end{aligned}$$

Now consider the Lawvere quantale **L** with E = {1 a ≈ b, 1 b ≈ c, 1 c ≈ d, 1 f(x) ≈ g(x)}, t = x, s = f(y), X = {x, y}, σ = {x → g(y)}, and ϑ = {x → g(a), y → d}. Besides, -= and we have

$$\begin{aligned} t\sigma &= g(y), \quad s\sigma = f(y), \quad \varepsilon = 1, \quad 1 \Vdash t\sigma =\_E s\sigma; \\ \delta &= 2, \qquad \sigma \overset{\rightharpoonup}{\underset{\approx}{\approx}} E, \{x, y\}, 2 \; ^0 \vartheta; \\ t\vartheta &= g(a), \quad s\vartheta = f(d); \\ \text{Variables of } \mathcal{X} \text{ occur in } t \text{ and } s \text{ in total twice;} \\ \varepsilon + 2\delta &= 5; \\ 5 \Vdash t\vartheta &= E \text{ s}\vartheta. \text{ (In fact, } \stackrel{\bullet}{=} E \text{ (}t\vartheta, s\vartheta) = 1 + 3 = 4 \text{ and } 5 \nmid 4.) \end{aligned}$$

Theorem 2 implies that if δ is an idempotent element of the quantale and it can be absorbed by ε (i.e., ε ⊗ δ = ε), then ε tϑ =E sϑ. Obviously, this will be fulfilled if δ = κ. In idempotent quantales, it will also hold when ε δ. For idempotent elements, a stronger version of transitivity holds. Namely, if ι is an idempotent element of a quantale, then we have for all E, t, s, r, X , σ, ϑ, ϕ:

– ι t =E s and ι s =E r imply ι t =E r, – σ E,X ,ι ϑ and ϑ E,X ,ι ϕ imply σ E,X ,ι ϕ.

# 4 Quantitative Equational Unification

Definition 4 (Quantitative equational unification). *A quantitative equational unification problem is formulated as follows:*

Given: *A quantale* **˙***,* ε ∈ Ω *(called the threshold) with* ε = ⊥*, a set of* **˙***-equalities* E *(a presentation of an equational theory), and two terms* t *and* s*.* Find: *A substitution* σ *such that* ε tσ =E sσ*.*

*We call this problem* (E,ε)-unification problem over **˙***. The quantale name is usually skipped when it does not cause confusion. For unification problems, we use the notation* ε t =? E s*, called a* unification equation*, where the question mark indicates that the equation is supposed to be solved. For simplicity, we write the problem as* t =? E,ε s*, and further skip* E *if it is clear from the context.*

*The substitution* σ*, if it exists, is called an* (E,ε)-unifier *of* t *and* s *(alternatively, a unifier or a solution of* t =? E,ε s*) over* **˙***. In such a case we say that the given unification problem is* solvable*, or that the terms* t *and* s *are* (E,ε) unifiable *over* **˙***. The set of all unifiers of* t =? E,ε s *is denoted by* UE,ε(t, s)*.*

For a given presentation E, a function symbol from F is called *free* if it does not appear in E. If F contains a free m-ary function symbol for some m > 1, the unification problem formulated above is equivalent to a problem of finding a solution of a system of unification equations (instead of a single equation) formulated as a constrained problem:

In such a case we can write the unification problem as a pair of a set of unification equations and a --constraint: {t1 =? E,**α**1 s1,...,tn =? E,**α***n* sn}; ε **α**1 ⊗···⊗ **α**n, where **α**i are new metavariables whose values are also to be found alongside with variables that appear in the given t's and s's. This problem can be transformed to a single-equation problem. For instance, the constrained problem {t1 =? E,**α**1 s1, t2 =? E,**α**2 s2, t3 =? E,**α**3 s3}; ε **α**1 ⊗ **α**2 ⊗ **α**3 can be transformed to f(f(t1, t2), t3) =? E,ε f(f(s1, s2), s3), where f is a free binary function symbol. The two problems are equivalent in the sense that they have exactly the same set of (E,ε)-unifiers.If the arity of f is bigger than the number of equations, the missing arguments will be filled in by fresh variables. For instance, for a quaternary f, the problem above can be encoded as f(t1, t2, t3, x) =? E,ε f(s1, s2, s3, x), where x is fresh.

In classical unification, an important property of the instantiation relation is that any substitution that is less general than a given unifier of two terms will still be a unifier. In the quantitative case, we should take into account the approximation, which complicates things. First, we have the following fact as a consequence of Theorem 2:

Fact 1. *If* σ *is an* (E,ε)*-unifier of* t *and* s *and* σ E,V(t,s),δ ϑ *for some* δ*, then* ϑ *is an* (E,ε ⊗ δk)*-unifier of* t *and* s*, where* k *is the total number of occurrences of variables in* t *and* s*.*

Some results become simpler for idempotent elements:

Lemma 2. *Let* ι *be an idempotent element of* **˙***, and* σ *and* ϑ *be substitutions.*

*Proof.* Part (i) is proved by structural induction, using idempotence. For (ii), as σ E,V(t,s),ι ϑ, there exists a substitution ϕ such that ι xσϕ =E xϑ holds for every variable x ∈ V(t, s). Thus, ι rσϕ =E rϑ holds for any term r ∈ T(F, V(t, s)) by (i). Hence, we have ι sϑ =E sσϕ, ε sσϕ =E tσϕ, and ι tσϕ =E tϑ. From these equalities, using ε ⊗ ι = ε, we get ε sϑ =E tϑ.

This lemma implies that (E, V(t, s), κ)-instances of (E,ε)-unifiers of t and s are still their (E,ε)-unifiers. Besides, it has the following corollary:

Corollary 2. *Let* **˙** *be an idempotent quantale, in which* σ *is an* (E,ε)*-unifier of* t *and* s*,* σ E,V(t,s),δ ϑ*, and* ε δ*. Then* ϑ *is an* (E,ε)*-unifier of* t *and* s *in* **˙***.*

These results motivate a specialized version of the notion of a minimal complete set of unifiers that we use in this paper:

Definition 5 (Minimal ι-complete set of unifiers). *Let* P *be an* (E,ε)*-unification problem over a quantale* **˙** *and signature* F*. Let* X = V(P) *be the set of all variables of* P*, and let* ι *be an idempotent element of* **˙** *such that* ε ⊗ ι = ε*. An* ι-complete set of (E,ε)-unifiers *of* P *is a set* C *of substitutions such that*

*(1)* C ⊆ UE,ε(P)*, i.e., each element of* C *is an* (E,ε)*-unifier of* P*, (2) for each* ϑ ∈ UE,ε(P) *there exists* σ ∈ C *such that* σ E,X ,ι ϑ*.*

*The set* C *is a* minimal ι-complete set of (E,ε)-unifiers *of* P *iff it is an* ι*-complete set that satisfies the following minimality property:*

*(3) for all* σ, σ ∈ C*, if* σ E,X ,ι σ *, then* σ = σ *.*

*We denote a minimal* ι*-complete set of* (E,ε)*-unifiers of* P *by mcsu*E,ε,ι(P)*.*

Given a unification problem with threshold ε, in order to make use of this definition, one first needs to find an idempotent element ι such that ε ⊗ ι = ε. In an arbitrary quantale, we can always take ι = κ. If ε is idempotent itself, then we can also choose ι = ε. 2

Let P be an (E,ε)-unification problem. If it is unsolvable, then for any idempotent ι with ε ⊗ ι = ε we have *mcsu*E,ε,ι(t, s) = ∅. Depending on E, ε, and ι, minimal ι-complete sets of (E,ε)-unifiers may not always exist. Even if they do, they may be infinite. When they exist, they are unique modulo the instantiation equivalence relation ∼=E,X ,ι. 3

*Example 3.* Let **˙** be the Lawvere quantale **L**, E be the set of equations E = {1 a ≈ b, 1 b ≈ c, 1 c ≈ d}, ε = 1, t = f(x, b), and s = f(c, x).

The substitutions σ = {x → b}, ϑ = {x → c} are (E,ε)-unifiers of t and s:

– tσ = f(b, b), sσ = f(c, b) and 1 f(b, b) =E f(c, b), – tϑ = f(c, b), sϑ = f(c, c) and 1 f(c, b) =E f(c, c).

In fact, {σ, ϑ} = *mcsu*E,ε,0(t, s). Note that we have σ ∼=E,X ,1 ϑ, but also σ ∼=E,X ,1 {x → a} and ϑ ∼=E,X ,1 {x → d}. However, neither {x → a} nor {x → d} is an (E,ε)-unifier of t and s (but they are (E, 3)-unifiers of t and s).

The notion of an *occurrence cycle* will be needed later on.

Definition 6 (Occurrence cycle). *A set of unification equations* {x1 ≈? ε1 t1, ...,xn ≈? ε*n* tn} *constitutes an* occurrence cycle *if* ti *is a non-variable term for at least one* i*,* xi ∈ V(ti−1) *for* 1 < i n *and* x1 ∈ V(tn)*.*

2 This is how it is done, e.g., for fuzzy proximity/similarity relations [9,14,15,19,20, 23].

3 ∼=E,*X*,ι is a standard binary relation on *Sub* induced by the **˙**-ternary relation ∼=E,*X* for a fixed ι.

#### 4.1 Unification: Simple Shallow Theories (Special Form)

In this section, we will consider **˙**-equational theories that admit a presentation consisting of a finite number of equations of the form γ f(x1,...,xn) ≈ g(x1,...,xn), where n 0, f = g, and all x's are pairwise distinct. Also, the γ's in different equations can be different. This is the very basic form of quantitative axioms. The quantale **˙**, as said above, is an arbitrary Lawvereian quantale. In the next subsection we consider the special case of idempotent Lawvereian quantales.

The presentation is shallow. One can easily show that the theory generated from such a presentation is simple. Hence, we consider simple shallow quantitative equational theories (of a special form). We will refer to such theories by Essh. In them, it makes sense to speak about the *approximation degree of two function symbols*, which is defined as dEssh (f,g) := - f(x1,...,xn) =• Essh g(x1,...,xm) for an n-ary f and m-ary g. (Obviously, dEssh (f,g) = ⊥ if n = m.) We say that f and g are (Essh, ε)-proximal, if ε dEssh (f,g).

*Remark 1.* Since the equational theories we consider here are finitely presented, the degree of two function symbols of the same arity can be effectively computed as dEssh (f,g) = {γ | γ f(x1,...,xn) = g(x1,...,xn) ∈ C}, where C is the closure of the presentation of Essh under the (Trans) and (Sym) rules.

Theorem 3. Essh*-unification is finitary in a Lawvereian quantale* **˙** *in the sense that for any* ε ∈ Ω*, every* (Essh, ε)*-unification problem* t =? Essh,ε s *has a finite minimal* κ*-complete set of unifiers.*

*Proof (Sketch).* Let NEssh,ε(r) denote an ε-neighborhood of a term r with respect to Essh, defined as the set of all terms obtained from r by replacing some function symbols by their (Essh, ε)-proximal ones. Then *mcsu*Essh,ε,κ(t, s) ⊆ ∪t-∈T ,s-∈S{*mgu*(t =? s )}, where T = NEssh,ε(t), S = NEssh,ε(s), and *mgu*(t =? s ) is a most general unifier of the syntactic unification problem t =? s . Since the presentation of theories of the form Essh is finite, the set NEssh,ε(r) is finite for ε = ⊥ for any r. Hence, the set ∪t-∈T ,s-∈S{*mgu*(t =? s )} is finite, which implies that *mcsu*Essh,ε,κ(t, s) is finite as well.

*Remark 2.* In principle, the above proof already outlines an Essh-unification algorithm. However, there are several reasons for not using it: first, it would be a brute-force approach blindly replacing symbols with all their proximal ones in all possible ways. Second, it would not be sound because non-unifier answers would be returned and we would have to clean the computed set afterwards. Third, we want to keep our approach flexible, leaving equations between variables as a part of the output instead of forcing them to have only a syntactic solution.

In the following, we use bold-face upright Greek letters **α**, **β**, **γ** for metavariables that range over the domain of the quantale. The rules constituting our unification method operate on configurations whose form is stated below.

Definition 7 (Configuration). *A* configuration *is either a special symbol F or a quadruple* P; C; δ; σ*, where*

*In* C*, we also allow for the case where* n = 0*, in which the empty product on the right-hand side is* κ *by convention.*

The solving rules for a theory Essh are given below. They operate on configurations and are formulated modulo associativity and commutativity of ⊗. We use f and g to denote (not necessarily distinct) n-ary function symbols, t, ti and si for terms and x to denote a variable symbol. The symbol Δ denotes the tensor product of finitely many metavariables.

#### Tri: Trivial

$$\{t =\_\mathfrak{a}^?t\} \uplus P; \zeta \ndot \otimes \Delta; \delta; \sigma \Longrightarrow P; \zeta \ndot \Delta; \delta; \sigma.$$

#### Dec: Decompose

$$\begin{aligned} \{f(t\_1, \ldots, t\_n) =\_\mathfrak{a}^? g(s\_1, \ldots, s\_n)\} &\uplus P; \zeta \stackrel{\scriptstyle}{\sim} \mathfrak{a} \otimes \Delta; \delta; \sigma \Longrightarrow\\ \{t\_1 =\_{\mathfrak{k}\_1}^? s\_1, \ldots, t\_n =\_{\mathfrak{k}\_n}^? s\_n\} &\cup P;\\ \mathfrak{d}\_{E\_{\text{ub}}}(f, g) \dashv \zeta \not\simeq \mathfrak{f}\_1 \otimes \cdots \otimes \mathfrak{f}\_n \otimes \Delta; \delta \otimes \mathfrak{d}\_{E\_{\text{ub}}}(f, g); \sigma, \end{aligned}$$

where **β**1,..., **β**n are new metavariables and ζ dEssh (f,g).

#### Cla: Clash

$$\{f(t\_1, \ldots, t\_n) =\_{\mathfrak{a}}^? g(s\_1, \ldots, s\_m)\} \uplus P; \zeta \nsubseteq \mathfrak{a} \otimes \Delta; \delta; \sigma \Longrightarrow \mathbf{F}, \text{ if } \zeta \not\subset \mathfrak{d}\_{E\_{\mathfrak{a}\mathfrak{b}}}(f, g).$$

#### L-Sub: Substitute (lazy)

$$\begin{aligned} \{x =\_{\mathfrak{a}}^{?} f(s\_1, \dots, s\_n)\} \uplus P; \zeta \precsim \mathfrak{a} \otimes \Delta; \delta; \sigma \implies\\ \{x\_1 =\_{\mathfrak{b}\_1}^{?} s\_1, \dots, x\_n =\_{\mathfrak{b}\_n}^{?} s\_n\} \cup P\rho;\\ \mathfrak{d}\_{E\_{\text{ub}}}(f, g) \rightharpoonup \zeta \precsim \mathfrak{f}\_1 \otimes \dots \otimes \mathfrak{b}\_n \otimes \Delta; \delta \otimes \mathfrak{d}\_{E\_{\text{ub}}}(f, g); \sigma \rho, \end{aligned}$$

where x does not appear in an occurrence cycle in {x=? **α** f(s1,...,sn)} ∪ P, and ρ = {x → g(x1,...,xn)} with x1,...,xn being fresh variables and ζ dEssh (f,g).

#### CCh: Cycle check

{x =? **α** t} P; C; δ; σ =⇒ F,

if x appears in an occurrence cycle in {x =? **α** t} P.

#### Ori: Orient

$$\{t =\_{\mathfrak{a}}^{?} x\} \uplus P; C; \delta; \sigma \Longrightarrow P \cup \{x =\_{\mathfrak{a}}^{?} t\}; C; \delta; \sigma, \text{ where } t \notin \mathcal{V}.$$

To solve an (Essh, ε)-unification problem between terms t and s, we create the initial configuration {t =? **α** s}; ε **α**; κ;*Id* and start applying the rules as long as possible. The equation to be transformed is chosen arbitrarily ("don't care nondeterminism"). We call the obtained algorithm QUnif.

Note that a configuration P; C; σ obtained from an (Essh, ε)-unification problem satisfies the following properties:

We will refer to such configurations as *admissible*.

To prove termination of QUnif, we introduce some terminology.

Definition 8. *Let* P *be a set of quantitative equations and let* Pst *be the set of standard equations obtained from* P *by ignoring the indices:* Pst := {t = s | ε t = s ∈ P}*. Then* DecNFEssh (P) *denotes the decomposition normal form of* P *with respect to* Essh*, which is the set of standard equations obtained from* Pst *by applying the following version of the decomposition rule as long as possible:*

$$\{f(t\_1, \ldots, t\_n) = g(s\_1, \ldots, s\_n)\} \uplus S \Longrightarrow \{t\_1 = s\_1, \ldots, t\_n = s\_n\} \cup S,$$

*where* dEssh (f,g) = ⊥*.*

It is easy to see that every equation in DecNFEssh (P) is of the form x = s where s is an arbitrary term, or t = x where t is not a variable.

For a set of (quantitative) equations P, the *variable dependency graph* Γ(P) is constructed as follows:

	- If l is a constant, then we add an edge x →d+1 G (with weight d + 1).
	- If l is a variable y, then we add an edge x →d y (with weight d).

In this way, we obtain a directed, weighted graph Γ(P), which is acyclic (hence, a *dag*) if and only if P does not contain any occurrence cycles.

For any variable x occurring in P, we define now the level *lev* P (x) of x with respect to P as the maximal weight of a walk in Γ(P) starting in x. Here, the weight of a walk is defined as the sum of the weights of its edges. Note that *lev* P may take the value ∞ if P contains occurrence cycles.

We now consider the multiset λ(P) := {*lev* P (x) | x ∈ V(P)}. (It will be used as a component of a termination measure below.) We compare such multisets via the multiset extension >*m* of the standard order on **N** ∪ {∞}, which is wellfounded. The following lemma is the main ingredient for the termination proof. Its proof can be found in [10].

Lemma 3. *Let* C = P; C; δ; σ *be a configuration.*

*(i) If* P ; C ; δ ; σ *is obtained from* C *by L-Sub, then* λ(P) >*m* λ(P ). *(ii) If* P ; C ; δ ; σ *is obtained from* C *by Tri, Dec, or Ori, then* λ(P)*m* λ(P ).

Theorem 4 (Termination of QUnif).*For a given* (Essh, ε)*-unification problem, the algorithm* QUnif *terminates either with the configuration F (indicating failure) or with a configuration of the form* V ; C; δ; σ *(indicating success), where* V *is a set of unification equations between variables.*

*Proof.* A simple analysis of the rules of QUnif shows that all terminal configurations are of the form described above. In order to prove that the algorithm terminates, first note that the Cla and CCh rules terminate the derivation immediately, so it suffices to show that the remaining rules cannot yield an infinite derivation. For this purpose, we consider the measures λ, n2 and n3, where n2 is the size of P and n3 is the number of equations of the form t =? **α** x in P such that t is a non-variable term. By Lemma 3, L-Sub decreases λ while all other rules do not increase it; Dec and Tri decrease n2, and Ori decreases n3 while leaving n2 invariant. Hence, the lexicographical combination of λ with n2 and n3 yields a measure that strictly decreases upon each of the aforementioned rules with respect to a well-founded order, thus proving termination.

Proceeding now to the soundness and completeness proofs for QUnif, we fix a notion of solution of a configuration.

Definition 9 (Solution of a configuration). *A substitution* τ *is a* solution *of the configuration* P; ζ **α**1 ⊗ **α**2 ⊗···⊗ **α**n; δ; σ *if there exists a function* μ *mapping metavariables to elements of* Ω *such that*

*(S1)* ζ μ(**α**1) ⊗ μ(**α**2) ⊗···⊗ μ(**α**n) *is valid, (S2)* μ(**β**) sτ =E tτ *holds for every equation* s =? **β** t *in* P*. (S3)* xτ = xστ *(syntactic equality) holds for every variable* x ∈ *dom*(σ)*.*

*The configuration F has no solutions.*

This definition is compatible with Definition 4 in the following sense:

Lemma 4. *Let* ε ∈ Ω*. A substitution* τ *is an* (E,ε)*-unifier of* t *and* s *if and only if* τ *is a solution for the corresponding initial configuration* {t =? **α** s}; ε **α**; κ;*Id.*

*Proof.* By definition, τ solves {t =? **α** s}; ε **α**; κ;*Id* iff there exists μ such that ε μ(**α**) and μ(**α**) tτ =E sτ , which is equivalent to ε tτ =E sτ .

The lemma below is needed to show soundness and completeness of QUnif. Its proof can be found in [10].

Lemma 5. *Let* C *be an admissible configuration.*

Theorem 5 (Soundness and completeness of QUnif). *Consider an* (Essh, ε)*-unification problem between terms* t *and* s*.*

	- *(ii)* μ(**α**i) xiϕ =Essh yiϕ *for all* 1 i n*;*
	- *(iii)* xσϕ = xτ *for all* x ∈ V(s, t)*.*

*Proof.* For soundness, suppose that QUnif produces a derivation C0 =⇒ ... =⇒ Cm, where C0 is the initial configuration {t =? **α** s}; ε **α**; κ;*Id* and Cm is a terminal configuration given by V ; S; δ; σ. If τ is a solution of Cm then τ is also a solution of C0 (by Lemma 5(i)), and therefore, τ is an (Essh, ε)-unifier of t and s (by Lemma 4).

For completeness, suppose that τ is an (E,ε)-unifier of t and s. Then τ solves the corresponding initial configuration C0 (by Lemma 4). If C0 is not terminal, then there exists a rule application C0 =⇒ C1 and a substitution τ1 such that τ1|*dom*(τ) = τ and τ1 solves C1 (by Lemma 5(ii)). Iterating this argument, we obtain a derivation C0 =⇒ C1 =⇒ ... and a sequence of substitutions τ,τ1,... . After a finite number of steps, this derivation reaches a terminal configuration Cm by Theorem 4, and with it, we obtain a solution τm such that τm|V(s,t) = τ . Since τm solves Cm, there exist ϕ and μ satisfying (i) and (ii), as well as xσϕ = xτm for all x ∈ V(Cm), yielding (iii).

*Remark 3.* In particular, a κ-complete set of solutions for the problem t =? ε s can be obtained by determining for every terminal configuration obtained via QUnif the set of substitutions that meet conditions (i)–(iii) above. If one is just interested in finding some solution, it suffices to compute a terminal configuration V ; ζ - Δ; δ; σ and compose σ with a substitution that maps all variables in V to a fresh variable. The value of δ corresponds to the "degree" to which such a solution τ solves the unification problem, i.e. δ = (tτ =• Essh sτ ).

*Example 4.* Consider the unification problem f(y, g(x, x)) =? E,ε g(f(c, a), y), where **˙** = **L**, E = {1 a ≈ b, 1 b ≈ c, 1 f(x1, x2) ≈ g(x1, x2)} and ε = 5. The following derivation can be obtained by QUnif:

{f(y, g(x, x)) =? **α** g(f(c, a), y)}; 5 **α**; 0; *Id* =⇒Dec {y =? **β**1 f(c, a), g(x, x) =? **β**2 y}; 4 **β**1 + **β**2; 1; *Id* =⇒y →f(z1,z2) L-Sub {z1 =? **γ**1 c, z2 =? **γ**2 a, g(x, x) =? **β**2 f(z1, z2)}; 4 **γ**1 + **γ**2 + **β**2; 1; {y → f(z1, z2)} =⇒z1 →b L-Sub { z2 =? **γ**2 a, g(x, x) =? **β**2 f(b, z2)}; 3 **γ**2 + **β**2; 2; {y → f(b, z2), z1 → b} =⇒Dec {z2 =? **γ**2 a, x =? **δ**1 b, x =? **δ**2 z2}; 2 **γ**2 + **δ**1 + **δ**2; 3; {y → f(b, z2), z1 → b} =⇒z2 →a L-Sub {x =? **δ**1 b, x =? **δ**2 a}; 2 **δ**1 + **δ**2; 3; {y → f(b, a), z1 → b, z2 → a} =⇒x →a L-Sub {a =? **δ**2 a}; 1 **δ**2; 4; {y → f(b, a), z1 → b, z2 → a, x → a} =⇒Tri ∅; 1 0; 4; {y → f(b, a), z1 → b, z2 → a, x → a}

This leads to the solution {y → f(b, a), x → a} (with degree 4). Further solutions can be obtained via different choices in the Subst steps.

*Example 5.* Consider **˙** = **L**, E = {1 f(x, y) ≈ g(x, y)}, and the E-unification problem g(a, x) =? 3 f(y, g(b, z)). A derivation of QUnif is given below.

$$\begin{split} & \{ g(a, x) = \stackrel{?}{!}\_{\bullet} \{ y, (g(b, z)) \}; 3 \geqslant \mathfrak{a}; 0; \operatorname{Id} \\ & \Longrightarrow\_{\mathsf{Dex}} \{ a = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} \, y, \, x = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} \, g(b, z) \}; 2 \geqslant \mathfrak{P}\_{1} + \mathfrak{P}\_{2}; 1; \operatorname{Id} \\ & \Longrightarrow\_{\mathsf{Or}} \{ y = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} \, a, \, x = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} \, g(b, z) \}; 2 \geqslant \mathfrak{P}\_{1} + \mathfrak{P}\_{2}; 1; \operatorname{Id} \\ & \Longrightarrow\_{\mathsf{L} \cdot \mathsf{Sub}}^{y \mapsto a} \{ x = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} \, g(b, z) \}; 2 \geqslant \mathfrak{P}\_{2}; 1; \{ y \mapsto a \} \\ & \Longrightarrow\_{\mathsf{L} \cdot \mathsf{Sub}}^{x \mapsto f(x\_{1}, x\_{2})} \{ x\_{1} = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}}, b, \, x\_{2} = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} z \}; 1 \geqslant \mathfrak{p}\_{1} + \mathfrak{p}\_{2}; 2; \{ y \mapsto a, x \mapsto f(x\_{1}, x\_{2}) \} \\ & \Longrightarrow\_{\mathsf{L} \cdot \mathsf{Sub}}^{x\_{1} \mapsto b} \{ x\_{2} = \stackrel{?}{\mathsf{P}}\_{\mathsf{P}} z \}; 1 \geqslant \mathfrak{p}\_{2}; 2; \{ y \mapsto a, x \mapsto f(b, x\_{2}), x\_{1} \mapsto b \} \end{split}$$

The computed terminal configuration still contains equations between variables. For any ψ such that 1 x2ψ =E zψ, the substitution {y → a, x → f(b, x2)}ψ is an (E,ε)-unifier of the given terms. In particular, unifiers that can be obtained from this configuration include, e.g., {y → a, x → f(b, u), z → u}, where u is a fresh variable (with degree 2), and also {y → a, x → f(b, f(a, a)), z → g(a, a)} (with degree 3).

#### 4.2 Idempotent Quantales

Now we consider the case where **˙** is idempotent. Under this hypothesis, we can strengthen our results and show that – with the right definitions – the unification problem is unitary, and that a simplified version of QUnif computes a most general unifier of two given terms. For the fuzzy quantale **˙** = **I**min = ([0, 1], , min), our algorithm coincides with Sessa's weak unification algorithm [23].

Note that in any integral idempotent quantale, meet and tensor coincide. As a consequence, in an idempotent quantale, α β implies β α = α.

Definition 10 (Weak mgu). *A substitution* σ *is a* weak most general (E,ε) unifier of t and s*, denoted wmgu*E,ε(t, s)*, if* UE,ε(t, s) = {τ | σ E,V(t,s),ε τ}*.*

By Lemma 2 (ii), σ = *wmgu*E,ε(t, s) iff σ ∈ UE,ε(t, s) and σ E,V(t,s),ε τ holds for every τ ∈ UE,ε(t, s); that is, iff {σ} = *mcsu*E,ε,ε(t, s).

In the idempotent setting, the rules L-Sub and CCh from QUnif can be replaced by simpler versions:

E-Sub: Substitute (eager)

{x =? **α** s} P; ζ **α** ⊗Δ; δ; σ =⇒ P{x → s}; ζ -Δ; δ; σ{x → s}, if x /∈ V(s). OCh: Occurrence check

$$\{x =\_{\mathfrak{a}}^{?} s\} \uplus P; C; \delta; \sigma \Longrightarrow \mathbf{F}, \quad \text{if } x \in \mathcal{V}(s) \text{ and } s \neq x.$$

Note that both of these rules constitute steps that could also be achieved by the rules from QUnif: E-Sub can be viewed as a composition of L-Sub and Dec steps, and OCh is just a restricted version of CCh. As before, we use these rules to transform the initial configuration corresponding to a given (Essh, ι) unification problem. As an output, we return Failure if F has been obtained, or σ if a terminal configuration P; C; δ; σ has been reached. We denote the resulting algorithm by QUnif-id.

In order to obtain a stronger completeness theorem than in the general case, we refine the notion of a solution of a configuration.

Definition 11 (ι-solution of a configuration). *Let* ι ∈ Ω *be idempotent. A substitution* τ *is an* ι-solution *of the configuration* P; ζ **α**1 ⊗ **α**2 ⊗···⊗ **α**n; δ; σ *if there exists a function* μ *mapping metavariables to elements of* Ω *such that*

*(*ι*1)* ζ μ(**α**1) ⊗ μ(**α**2) ⊗···⊗ μ(**α**n) *is valid, (*ι*2)* μ(**β**) tτ =E sτ *holds for every equation* t =? **β** s *in* P*. (*ι*3)* ι xτ =E xστ *holds for every variable* x ∈ *dom*(σ)*.*

*The configuration F has no solutions.*

Note that the only difference in comparison with Definition 9 is that (ι3) features a quantitative equality over Essh, whereas in (S3) we have a syntactic equality.

The lemmas below are needed in the proof of soundness and completeness of QUnif-id (see [10] for their proofs).

Lemma 6. *Let* **˙** *be a (not necessarily idempotent) quantale,* ι ∈ Ω *be an idempotent element of* **˙***,* τ *be a substitution, and* t *and* s *be terms.*

Lemma 7. *Let* **˙** *be an idempotent quantale,* ι ∈ Ω*, and* C *be a configuration obtained from an* (Essh, ι)*-unification problem in* **˙** *by applying rules from* QUnif-id*. If* C *is obtained from* C *by a rule from* QUnif-id*, then a substitution* τ *is an* ι*-solution of* C *iff it is an* ι*-solution of* C *.*

Theorem 6 (Soundness and completeness of QUnif-id). *Consider an* (Essh, ι)*-unification problem between terms* t *and* s *in an idempotent quantale* **˙***, where* ι ∈ Ω*. Any run of* QUnif-id *starting from* {t =? **α** s}; **α** ι; κ;*Id terminates and returns wmgu*Essh,ι(t, s) *if it exists, or fails otherwise.*

*Proof.* Termination follows from termination of QUnif (Theorem 4). For soundness and completeness, by Lemma 6(i), a substitution τ is an (Essh, ι)-unifier of t and s iff it is an ι-solution of the initial configuration C0. By Lemma 7, the latter holds iff τ is an ι-solution for any terminal configuration ∅; C; δ; σ, or equivalently, iff σ Essh,V(t,s),ι τ (by Lemma 6(ii)), concluding the proof.

*Example 6.* We demonstrate algorithm QUnif-id for the problem f(x, c)=? **I**,0.4,E h(a, x) in the (idempotent) fuzzy quantale **I** with the min T-norm modulo E = {0.5 a ≈ b, 0.5 b ≈ c, 0.6 f(x1, x2) ≈ g(x1, x2), 0.7 g(x1, x2) ≈ h(x1, x2)}.

A derivation of QUnif-id is shown below:

$$\begin{aligned} & \{ f(x, c) =\_{\mathfrak{a}}^{?} h(a, x) \}; 0.4 \leqslant \mathfrak{a}; 1; Id \\ & \Longrightarrow\_{\mathsf{Dec}} \{ x =\_{\mathfrak{P}\_1}^{?} a, \ c =\_{\mathfrak{P}\_2}^{?} x \}; 0.4 \leqslant \min(\mathfrak{P}\_1, \mathfrak{P}\_2); 0.6; Id \\ & \Longrightarrow\_{\mathsf{L} \cdot \mathsf{Sub}}^{x \mapsto a} \{ c =\_{\mathfrak{P}\_2}^{?} a \}; 0.4 \leqslant \mathfrak{P}\_2; 0.6; \{ x \mapsto a \} \\ & \Longrightarrow\_{\mathsf{Dec}} \emptyset; 0.4 \leqslant 1; 0.5; \{ x \mapsto a \} . \end{aligned}$$

Choosing the other equation in the L-Sub step would lead to a different unifier {x → c} with the same degree 0.5. The solution {x → b} (with degree 0.5) is not computed. All three solutions are 0.5-equivalent.

# 5 Conclusion

In the quantitative setting, equality is replaced by its quantitative counterpart modeling the abstract notion of proximity between terms. A quantitative unification problem asks for finding a substitution that brings the given terms close to each other within a predefined range (with respect to this abstract proximity). However, unlike the standard unification, here it is not guaranteed that an instance of a unifier is still a unifier. The reason is that the instantiation is also quantitative, and it might move the more specific substitution "too far away" from a unifier of the given problem.

In studying quantitative unification, one has to address such and related challenges. We investigated the quantitative equational unification problem in Lawvereian quantales modulo theories presented by axioms of the form γ f(x1,...,xn) ≈ g(x1,...,xn). Our notion of a minimal complete set of unifiers takes into account two (abstract) distances: between terms to be unified and between substitutions via instantiation. We showed that our unification problems in arbitrary Lawvereian quantales are finitary, while for idempotent Lawvereian quantales, they are unitary. The corresponding algorithms were developed and their properties were studied.

The equational theories that we considered here are a special case of simple shallow theories. An interesting future work would be to extend this work to a larger class of shallow theories (which have some desirable properties in the standard case [6]). Further, the related problem of disunification in Lawvereian quantales is worth investigating.

Acknowledgments. Supported by the Austrian Science Fund (FWF) under project P 35530 (SQUEE).

Disclosure of Interests. The authors have no competing interests to declare that are relevant to the content of this article.

# References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.

# **Equivalence Checking of Quantum Circuits by Model Counting**

Jingyi Mei(B) , Tim Coopmans, Marcello Bonsangue, and Alfons Laarman

Leiden University, Leiden, The Netherlands<EMAIL_ADDRESS>
**Abstract.** Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams.

**Keywords:** Quantum computing · Circuit equivalence · Satisfiability · #SAT · Weighted model counting · Pauli basis

## **1 Introduction**

Physicists and chemists regularly deal with 'quantum NP'-hard problems, for example when finding the ground state (energy) of a physical system [30] or assessing the consistency of local density matrices (the quantum analog of deciding the consistency of marginal probability distributions) [32]. Quantum computing not only holds the potential to provide a matching computational resource for tackling these challenges but also serves as a bridge to incorporate classical reasoning techniques for tackling nature's hardest problems. Quantum circuits, in particular, offer a precise view into these problems, because the quantum circuit equivalence checking problem is also 'quantum NP'-hard.

Circuit equivalence [2,4,8,22,23,52,55,56,61] also has many important applications. Since quantum computers are highly affected by noise, it is necessary to optimize the circuits to maximize the performance when running them on a real device. Furthermore, many devices can only handle shallow-depth circuits and are subject to various constraints such as connectivity, topology, and native gate sets. An essential aspect of designing and optimizing quantum circuits isverifying whether two quantum circuits implement the same quantum operation.

Equivalence checking for so-called Clifford circuits is tractable [52], which is surprising considering their wide applicability, e.g. in quantum error correction [9,48,49]. Extending the Clifford gate set with any non-Clifford gate, however, e.g. with a T or Toffoli gate, makes the problem immediately 'quantum NP'-hard, that is: NQP-hard to compute exactly [51] and QMA-hard to approximate [24], even for constant-depth circuits [25].1 The exact formulation of equivalence checking allows its discretization [29], exposing the underlying combinatorial problem that classical reasoning methods excel in. Indeed, exact reasoning methods based on decision diagrams are even used to compute the approximate version of the problem (see e.g. [23,57]).

Our aim is to use reasoning tools based on satisfiability (SAT) for *exact* equivalence checking of *universal* quantum circuits. Like SAT solvers [7,16], model counters, or #SAT solvers, can handle complex constraints from industrial-scale applications [40,47], despite the #P-completeness of the underlying problem.

We propose a new equivalence-checking algorithm based on weighted model counting (WMC). To do so, we generalize the WMC encoding of quantum circuit simulation from [34], showing that it essentially only relies on expressing quantum information in the so-called Pauli basis [18], thus obviating the need for the arguably more complex stabilizer theory [20,63]. In addition, we extend the encoding with support for the (non-Clifford) Toffoli gate, allowing more efficient encodings for many circuits. We then prove that a folklore theorem on quantum circuit equivalence checking [52] enables the reduction of the problem to a sequence of weighted Boolean formulas that can be solved using existing weighted model counters (provided they support negative weights [34]).

We show how the WMC encoding satisfies the conditions of the theorem from [52] and implement the proposed equivalence checking algorithm in the opensource tool ECMC, which uses the weighted model-counting tool GPMC [50].2 To assess the scalability and practicality of ECMC, we conduct experimental evaluations using random Clifford+T circuits which closely resemble quantum chemistry applications [59] and various quantum algorithms from the MQT benchmark [43], which includes important quantum algorithms such as QAOA, Wstate, and VQE among others. We compare the results of our method against that of the state-of-the-art circuit equivalence checker QCEC [8], showing that in several cases the WMC approach used by our ECMC tool is competitive.

In summary, this paper provides a many-to-many reduction of (universal) quantum circuit equivalence to weighted model counting (WMC). As a consequence, we contribute additional new benchmarks for the WMC competition: basically, each pair of universal quantum circuits can be reduced to a sequence of weighted CNF encodings that need to be solved to (dis)prove equivalence. This opens up numerous possibilities and challenges to better adapt model counters for this new application area in quantum computing.

1 A similar "jump" in hardness was noted for quantum circuit simulation in [54].

2 While the theorem presented in [52] already supported universal circuits, the provided tool implementation in [52] is limited to (non-universal) Clifford circuits.

#### **2 General Background**

We only provide the necessary background. For a more complete description see the full version of this paper [35].

*Quantum Computing.* We fix n as the number of qubits in the circuit(s) under consideration and write [m] for the set {1,...,m}. Qubits are numbered as [n]. We represent an n-qubit quantum state |ϕ- ∈ C2n as its *density matrix* |ϕϕ| ∈ C2n × C2n , where ϕ| represents the conjugate transpose |ϕ-† of |ϕ-[38].

A quantum gate G on n qubits can be expressed by a 2n ×2n complex matrix UG which is unitary, i.e. UG is invertible and satisfies U† G = U−1 G . If a quantum state is represented by a density matrix |ϕϕ|, then the density matrix after applying G is given by *conjugation* of |ϕϕ|, i.e. UG |ϕϕ|U† G. For an n-qubit quantum system, applying a single-qubit gate U on the j-th qubit is represented by Uj = I⊗j−1 ⊗ U ⊗ I⊗n−j , (1)

$$U\_j = I^{\otimes j-1} \otimes U \otimes I^{\otimes n-j},\tag{1}$$

where I is the single-qubit identity matrix and ⊗ denotes the Kronecker product. A circuit in our text is simply a list of n-qubit unitaries, i.e., C = (G0,...,Gm−1) where C can in turn be understood as unitary itself UC = UGm−1 · UGm−2 ···UG0 . We will sometimes refer to a gate or circuit as its unitary, and vice versa, because it is clear from context which is meant.

The gates

$$H = \frac{1}{\sqrt{2}} \begin{bmatrix} 1 & 1 \\ 1 & -1 \end{bmatrix}, \quad S = \begin{bmatrix} 1 & 0 \\ 0 & i \end{bmatrix}, \quad CZ = \begin{bmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & -1 \end{bmatrix}$$

form the so-called Clifford (generating) set.

Though non-universal and classically simulatable [1], Clifford circuits, i.e., circuits composed of Clifford gates only, are expressive enough to describe entanglement, teleportation and superdense coding, and are used in quantum errorcorrecting codes [9,48,49] and in measurement-based quantum computation [46]. Nonetheless, even equivalence checking of Clifford circuits is in P [52]. By extending the Clifford gate set with any non-Clifford gate, such as the T = √ S, Toffoli or arbitrary rotation gates RX, RY , RY , we immediately obtain a universal gate set, in the sense that arbitrary unitaries can be approximated [14,30,31].

In this work, we express matrices not in the standard basis but in the Pauli basis. We define the 2 × 2 *Pauli matrices* X, Y, Z, together with identity, as: 0 −1 ] , σ[10] ≡ X ≡ [ 0 1 1 0 ] , σ[11] ≡ Y ≡ [ 0 −ı˙ ı˙ 0 ]

$$\sigma[00] \equiv I \equiv \begin{bmatrix} \begin{smallmatrix} 1 \ 0 \end{smallmatrix} \end{smallmatrix} \mid, \ \sigma[01] \equiv Z \equiv \begin{bmatrix} \begin{smallmatrix} 1 \ 0 \end{smallmatrix} \end{smallmatrix} \mid, \ \sigma[10] \equiv X \equiv \begin{bmatrix} \begin{smallmatrix} 0 \ 1 \end{smallmatrix} \end{smallmatrix} \mid, \ \sigma[11] \equiv Y \equiv \begin{bmatrix} \begin{smallmatrix} 0 \ -i \end{smallmatrix} \end{smallmatrix} \mid$$

For n qubits, we define the set of "Pauli strings" Pˆn ≜ {P1 ⊗ P2 ⊗ ... ⊗ Pn | Pj ∈ {I, X, Y, Z}}. Inheriting the properties of Pauli matrices, Pauli strings are unitary, involutory and Hermitian. It is well-known that the scaled Pauli strings { √ 1 2 n · P | P ∈ Pˆn} form an orthonormal basis for 2n × 2n complex matrices [27]. Hence, we can decompose any 2n × 2n complex matrix M as M = P ∈Pˆn γP · P where the *Pauli coefficient* γP = 1 2n Tr(P† · M).

*In general, the coefficients* γP *are complex numbers, but for Hermitian matrices, they are real* [18,35]*. Example 1.* The matrix M = [ 1 4+i 4−i −5 ] is Hermitian. We calculate the coefficients:

$$\frac{1}{2^{\mathbb{Z}}}\operatorname{Tr}(I^{\dagger}M) = -2, \quad \frac{1}{2^{\mathbb{T}}}\operatorname{Tr}(Z^{\dagger}M) = 3, \quad \frac{1}{2^{\mathbb{T}}}\operatorname{Tr}(X^{\dagger}M) = 4, \quad \frac{1}{2^{\mathbb{T}}}\operatorname{Tr}(Y^{\dagger}M) = -1$$

It is straightforward to verify that these are M's Pauli *real* coefficients:

$$\begin{aligned} \text{is straightforward to verify that these are } M \text{'s Pauli real coefficients:}\\ -2I + 4X - 1Y + 3Z &= -2 \cdot \begin{bmatrix} \begin{smallmatrix} 1 \ 0 \end{smallmatrix} \end{smallmatrix} + 4 \cdot \begin{bmatrix} \begin{smallmatrix} 0 \ 1 \end{smallmatrix} \end{smallmatrix} - 1 \cdot \begin{bmatrix} \begin{smallmatrix} 0 \ -i \end{smallmatrix} \end{smallmatrix} + 3 \cdot \begin{bmatrix} \begin{smallmatrix} 1 \ 0 \end{smallmatrix} \end{bmatrix} = \begin{bmatrix} \begin{smallmatrix} 1 \ 4 \ -i \end{smallmatrix} \end{bmatrix}. \end{aligned}$$

*Weighted Model Counting (WMC).* In this work, we will encode the Pauli coefficients of specific matrices as weighted model counting: a sum of weights over all satisfying assignments of a boolean formula. We here formally describe WMC.

For boolean variables x, y ∈ B = {0, 1}, we define a literal as e.g. x and x and write conjunctions of literals (cubes) as products, e.g., xy = x ∧ y. A clause is a disjunction of literals, e.g., x ∨ y. A formula in conjunctive normal form (CNF) is a conjunction of clauses.

Let F : Bx → B be a propositional formula over boolean variables x ∈ Bn. We assign weights to literals using a weight function W : {x, x | x ∈ x} → R. Given an assignment α ∈ Bx, let W(α) = x∈x W(x = α(x)). We define *weighted model counting* [7,10,19,21] as follows.

$$MC\_W(F) \triangleq \sum\_{\alpha \in \mathbb{B}^{\vec{x}}} F(\alpha) \cdot W(\alpha)$$

*Example 2.* An example, consider a formula F =b∧c over x=(a, b, c). There exist two satisfying assignments: α1 = abc and α2 = abc. Suppose a weight function W is defined as follows: W(a) = −2, W(a) = 3, W(b) = 1/2, W(b) = 2, while c remains unbiased, i.e., W(c) =W(c) = 1. The weighted model counting for F with respect to W is computed as follows. MCW (F) = F(abc) · W(abc) + F(abc) · W(abc) = (−2 · 1 2 · 1) + (3 · 1 2 · 1) = 1 2 .

## **3 Equivalence Checking Circuits in the Pauli Basis**

In this section, we introduce (exact) equivalence checking [2,4,8,22,52,55,56,61] in Definition 1, the task we set out to solve. In this work, we will only consider circuits which consist of gates, and do not contain measurements (this is without loss of generality since measurements be deferred to the end of the circuit [38]). **Definition 1.** *Given two* n*-qubit circuits* U *and* V *where* n∈N+*,* U *is equivalent*

*to* V *, written* U ≡ V *, if there exists a complex number* c *(the global phase [38]) such that for all input states* |ψ-*, we have* U|ψ- = cV |ψ-*.*

At first sight, one might think that Definition 1 requires iterating over all quantum states. However, although the n-qubit quantum state space is continuous, it is a complex vector space of dimension 2n, so it suffices to only consider 2n basis vectors for proving U and V equivalent. In fact, the novice approach to equivalence checking is to decompose U and V in the standard basis; that is, to find U and V each by writing each of their individual gates in the standard basis and determining the full unitaries U and V by matrix multiplication, and finally checking whether the matrix entries of U equal those of V , modulo a uniform constant c. One could also perform such an approach when the individual gates in U and V are specified in a different basis, such as the Pauli basis (see Sect. 2), but this would have no a priori advantage over the use of the standard basis. Instead, we will use the following folklore result (for proof see e.g. [52]). **Theorem 1.** *Let* U, V *be two circuits on* n ∈ N+ *qubits. Then* U *is equivalent to*

V *if and only if the following condition holds (for notation* Pj *see Eq. 1): For all* j ∈ [n] *and* P ∈ {X, Z}*, we have* UPjU† = V PjV †*.*

The main advantage of using Theorem 1 instead of directly computing the (matrix entries of the) unitaries U and V is that for Clifford gates G, G it is computationally easy to update the Pauli coefficients of GPjG† to those of (GG )Pj (GG )† = G G PjG† G†. This feature forms the basis for efficient simulation of Clifford circuits and has lead to efficient Clifford circuit equivalence checking [52]. Here, we will include T gates, Toffoli, and Pauli rotation gates, enabling equivalence checking of universal quantum computing (lifting the hardness of equivalence checking to quantum analogs of NP, see Sect. 1). Another advantage of Theorem 1 is that, since U is a unitary, UPjU† is Hermitian, so that its Pauli coefficients are real numbers as noted in Sect. 2, relieving us from the need to use complex numbers.

*Example 3.* Choose V = S1 and U = T1T1. In order to determine whether U ≡ V , we compute the Pauli coefficients of UXU†,UZU†,V XV † and V ZV † as follows using Table 1. By Theorem 1, this implies that U and V are equivalent, which we verify by writing their unitaries in the standard basis as follows.

U = S = [ 1 0 0 i ] , V = T · T = 1 0 0 √i · 1 0 0 √i = [ 1 0 0 i ]

Finally, we remark that UXU†= 1 2 (✚X✚+Y +Y −✚X✚)=Y represents both constructive (Y terms add up) as well as destructive interference (X terms cancel).

We will finish this section by explaining the intuition behind Theorem 1, by rephrasing its proof from [52]. The first step in the proof is to realize that Definition 1 is equivalent to the following in density matrix representation. **Lemma 1.** *Given two* n*-qubit circuits* U *and* V *where* n ∈ N+*,* U *is equivalent*

*to* V *iff for all* n*-qubit quantum states* |ϕ-*, we have* U |ϕϕ|U† = V |ϕϕ| V †*.*

Recall that for any unitary U, with |ψ- = U|ϕ-, the corresponding operation on the density matrix |ϕϕ| is conjugation, i.e., |ψψ| = U|ϕϕ|U†. Density matrices are 2n × 2n Hermitian matrices and can thus be expressed as a (realweighted) linear combination of Pauli strings. For this reason, we observe that if UPU† = VPV † for each Pauli string P, i.e. U and V coincide on all Pauli strings by conjugation, then U and V must also coincide on all density matrices by conjugation, and thus they are equivalent by Lemma 1.

The final step in proving Theorem 1 is to realize that for a unitary matrix, the conjugation action is completely determined by fixing its conjugation action on only all Xj and Zj for j ∈[n]. This insight relies on two parts: First, each Pauli string can be written as the product of Xj and Zj modulo a factor ∈{±1, ±i}. Second, for a unitary M, we have M†M = I, which implies that instead of first multiplying Xj s and Zj s to construct a Pauli string, followed by conjugation, one can first conjugate and subsequently multiply to arrive at the same result.3 For example, MXjM† · MZjM† = MXj IZjM† = MXjZjM†.

We observe that in Table 1, the last two non-Clifford gates yield a linear combination of Pauli strings [34] for each Pauli string (matrix). This potentially causes an explosion of the number of Pauli strings when conjugating multiple non-Clifford gates. To handle this, we will exploit the strength of model counters in Sect. 4 by representing Pauli strings Pˆ as satisfying assignments which are weighted by the coefficient γPˆ, as explained next in Sect. 4.

# **4 Encoding Quantum Circuit Equivalence in SAT**

The previous section Sect. 3, centered around Theorem 1, explained that equivalence checking can be done by conjugating Pauli strings with unitaries, and that the required calculations for this approach are the same as in simulation of quantum circuits using a density matrix representation of the quantum state. In this section, we show how we reduce equivalence checking of universal quantum circuits to weighted model counting, which is formalized in Corollary 1 below. Our approach is based on the O(n + m)-length encoding for quantum circuit simulation provided in [34]. Finally, our encoding in this work extends [34] with Toffoli gates. For the rest of the paper, we use P for an unweighted Pauli string and we use **P** for a summation of weighted Pauli strings, e.g. √ 1 2X + √ 1 2Y .

3 The conjugation map P -→ UPU† is a group isomorphism.

**Table 1.** Lookup table for conjugating Pauli gates by Clifford+T+R*X* gates. The subscripts "c" and "t" stand for "control" and "target". Adapted from [34].

To simplify notation, we will solve a rephrased version of the equivalence checking problem from Definition 1 in Sect. 3: to check whether a unitary A is equivalent to the identity unitary I, which leaves every input unchanged. By choosing A ≜ V †U, we see that U ≡V precisely if A≡I. If U and V consist of gates U = (U0, U1,...,Um−1) and V = (V0, V1,...,V−1) for m, ∈ N+, then a circuit for A is given as the m+ gates A= (U0, U1,...,Um−1, V † −1, V † −2,...,V † 0 ). Following Theorem 1, our task will be as follows: Given a circuit A = G0,...,Gm−1 ∈ {Hj , Sj ,CZjk, Tj , Toffolijkl, RX(θ)j , ···| j, k, l ∈ [n]} m, we need to obtain **P**m = A**P**0A† from an initial **P**0 ∈ {+Xi, +Zi | i ∈ [n]}, showing that **P**m = **P**0. Since **P**0 is a Pauli string and thus Hermitian, so is **P**m. Our approach is to construct a boolean formula whose weighted model counts represent the terms in the Pauli decomposition of **P**m.

#### **4.1 Encoding Pauli Coefficients as Weighted Model Counts**

We first explain the encoding for circuit simulation from [34], where we encode the real-weighted sum of Pauli operators **P** and the update rules of the circuit A as weighted boolean formulas. We start with the simplest case—a Pauli string, then consider how to encode a single summand, i.e., a single weighted Pauli operator, and in the end extend this to a weighted sum of Pauli operators. i∈[n] σ[ai, bi] with ai, bi ∈ {0, 1}, the corresponding

Given a Pauli string P = encoding is denoted as FP , which is the boolean formula which only has {x1 ← a1, ··· , xn←an, z1←b1, ··· , zn←bn} as satisfying assignment, for example FZ⊗X = Fσ[01]⊗σ[10] = x1x2z1z2. When it comes to weighted Pauli string, although the weights are never imaginary in case of a Hermitian matrix, they can still have a ± sign. A weighted Pauli operator can be therefore encoded by 2n + 1 boolean variables: two bits xi, zi for each of the n Pauli matrices and one sign bit r, such that **P** = (−1)rσ[x1, z1] ⊗ ... ⊗ σ[xn, zn]. For example, consider boolean formula F**P** = rx1z1x2z2 where **P** = −Z ⊗ Y . Its one satisfying assignment is {r←1, x1←0, z1←1, x2←1, z2←1}≡−Z ⊗Y . We later introduce weights W(r)=−1 and W(r)=1 to interpret the sign. So for a formula F(x1, z1,...,xn, zn, r), we let the satisfying assignment represent a set (linear combination) of Pauli strings. The base case is the formula F**P**0 = FP for a Pauli string P ∈ {Xj , Zj | j ∈ [n]}. Next, we need to encode how sums of Pauli operators evolve when conjugating with the gates of the circuit, one by one. For this, our encoding duplicates the variables for all m gates (each time step) as follows (which is similar to encodings for bounded model checking [6]).

$$\vec{w}^{t} = \{x\_j^t, z\_j^t, r^t \mid j \in [n]\} \text{ for } t \in \{0, 1, \ldots, m\} \text{ and } \vec{v}^{t} = \bigcup\_{i \in [t] \cup \{0\}} \vec{w}^{i}. \tag{2}$$

For example, **P**0 = X1 is encoded as r0x0 1z0 1x0 2z0 2 ...x0 nz0 n. Also, the satisfying assignments of a boolean formula FA(vm) projected to variables wt represent the sum of Pauli operators after conjugating the initial t gates G0, G1,...,Gt−1 of the circuit A, written:

$$F\_A(\vec{v}^m)[\vec{w}^t] = \sum\_{\alpha \in \{0, 1\}^{\vec{v}^m}} F\_A(\alpha) \cdot (-1)^{\alpha(r^t)} \cdot \bigotimes\_{j \in [n]} \sigma[\alpha(x\_j^t), \alpha(z\_j^t)]$$

The next question is how to encode gate semantics, i.e., define a constraint to get **P**1 by conjugating gate G0 to **P**0, etc. Note that since **P**0 ∈ {Xj , Zj | j ∈ [n]} consists of a sum of only one Pauli operator. For Clifford circuits C, there will only be a single satisfying assignment α for all time steps t ∈ [m], since e.g. HXH† = Z (and not e.g. Z + Y ). Non-Clifford gates, like T or Toffoli, will add satisfying assignments representing summands with different weights (e.g. sums of accumulated weights of 1/ √2 for the T gate as discussed above). To encode these weights, we introduce new variables ut , but only at time steps t with a T gate (i.e., Gt = T).

When a gate Tj is performed and there is a satisfying assignment with xt j =1, it means that we are conjugating a T gate on the j-th qubit set to ±X or ±Y and the result should be either TXT† = √ 1 2 (X + Y ) or TYT† = √ 1 2 (Y − X) (modulo sign). To achieve this the encoding should let zt+1 unconstrained and set ut⇔xt j . Accordingly, we set the weights W(ut ) = √ 1 2 and W(ut ) = 1. Table 2 illustrates how the boolean variables wt and wt+1 relate for a T gate (derived by computing TPT† for Pauli gate P).

The encoding of gate semantics can be derived similarly. For example the boolean constraint for Ht j follows from Table 1 and is given by , wt+1) ≜ rt+1 ⇔ rt ⊕ xt j ∧ zt+1 j ∧ xt+1

$$F\_{H\_j^t}(\vec{w}^t, \vec{w}^{t+1}) \triangleq r^{t+1} \Leftrightarrow r^t \oplus x\_j^t z\_j^t \land z\_j^{t+1} \Leftrightarrow x\_j^t \land x\_j^{t+1} \Leftrightarrow z\_j^t$$

Here we omit additional constraints at+1 ⇔ at for all unconstrained time-stept + 1 variables a, i.e., for a = xt+1 l , zt+1 l with l =j. Similarly, by abbreviating FGt (wt , wt+1) as Gt , the encoding for other Clifford+T gates are as follows: j ≜ rt+1 ⇔ rt ⊕ xt j ∧ zt+1

$$\begin{split} &G^{t}\_{j} \triangleq \begin{aligned} &r^{t+1}, \ldots, r^{t+1} \Leftrightarrow \stackrel{\scriptstyle \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \! \!$$

**Table 2.** Boolean variables under the action of conjugating one T gate. Here we omit the sign (−1)*r*t for all P and sign (−1)*r*t+1 for all TPT†.

To this end, we can inductively define boolean constraints for each time step as F**P**t (vt ) = F**P**0 (w 0) ∧ i∈[t−1]∪{0} Gi (wi , wi+1) for t ⊓ 1, where Gi denotes the gate at time step i and F**P**0 (v0) encodes **P**0.

*Example 4.* Reconsider the circuit U=T ·T from Example 3. Starting with **P**0=X, the formulas are F**P**0 = x0 z0 r0, F**P**1 = F**P**0 ∧ FT 0 , i.e.

$$\begin{aligned} F\_{\mathbf{P}^0} \wedge F\_{T\_1^0} &= x\_1^0 \overline{z\_1^0} \overline{r^0} \wedge x\_1^1 \Leftrightarrow x\_1^0 \wedge x\_1^0 \vee (z\_1^1 \Leftrightarrow z\_1^0) \wedge \overline{z\_1^1}, \\ r^1 &\Leftrightarrow r^0 \oplus x\_1^0 z\_1^0 \neg z\_1^1 \wedge u^0 \Leftrightarrow x\_1^0, \end{aligned}$$

and similarly F**P**2 = F**P**1 ∧ FT 1 .

Formalizing the explanation above as induction over the gates proves Proposition 1, relating weighted model counting the Pauli coefficients (see Sect. 2).

**Proposition 1 (WMC computes the Pauli coefficients).** *Let* CA = (G0, ...,Gm−1) *be an* n*-qubit circuit,* A = G0 ··· Gm−1 *the corresponding unitary and* **P**0 *a Pauli string, so that the encoding of* **P**m ≜ A**P**0A† *is given by* F**P**m ≜ F**P**0 ∧ m−1 i=0 FGi *with according weight function* W*. For any* **P**0 ∈ {+Xj , +Zj | j ∈ [n]} *and* P ∈ Pˆn*, the weighted model count of* F**P**m ∧ FP *equals the Pauli coefficient* γP *of* **P**m*. That is,* MCW (F**P**m ∧ FP ) = 1 n · Tr(P† · A**P**0A†) *for all* P ∈ Pˆn*.*

We emphasize the necessity for using negative weights. For example, in Example 3, we have **P**2 =U**P**0U† = 1 (✚X✚+Y +Y −✚X✚)=Y for **P**0 =X, where the terms X and −X cancel each other out, while the Y terms add up. *This is why weighted model counting with negative weights is required; to reason about such constructive and destructive interference, ubiquitous to quantum computing.*

*Example 5.* Following Example 4, we have the satisfying assignments for F**P**0 , F**P**1 and F**P**2 as:

$$\begin{split}SAT(F\_{\mathbf{P}^{0}}) &= \{x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}\}, \\ SAT(F\_{\mathbf{P}^{1}}) &= \{x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}x\_{1}^{1}\overline{z\_{1}^{1}r\_{1}^{1}}\ u^{0}, \ x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}x\_{1}^{1}z\_{1}^{1}\overline{r\_{1}^{1}}\ u^{0}\}, \\SAT(F\_{\mathbf{P}^{2}}) &= \{x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}x\_{1}^{1}\overline{z\_{1}^{1}r\_{1}^{1}}x\_{1}^{2}\overline{z\_{1}^{2}r\_{1}^{2}}\ u^{0}u^{1}, \ x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}x\_{1}^{1}\overline{z\_{1}^{1}r\_{1}^{1}}x\_{1}^{2}z\_{1}^{2}\overline{r\_{1}^{2}}u^{0}u^{1}, \\ &\qquad\qquad x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}x\_{1}^{1}z\_{1}^{1}\overline{r\_{1}^{1}}x\_{1}^{2}z\_{1}^{2}\overline{r\_{1}^{2}}u^{0}u^{1}, \ x\_{1}^{0}\overline{z\_{1}^{0}r\_{1}^{0}}x\_{1}^{1}z\_{1}^{1}\overline{r\_{1}^{1}}x\_{1}^{2}\overline{z\_{1}^{2}}r\_{1}^{2}u^{1}u^{1}\}, \end{split}$$

with the weight function W(r2 1)=−1, W(r2 1)=1, W(u0)=W(u1)= √ 1 2 and W(u0)= W(u1)=1. Each of the satisfying assignments corresponds to a term in the Pauli decomposition of **P**2, which we recall from Example 3 to be

$$\mathbf{P}^2 = \frac{1}{2}X + \frac{1}{2}Y + \frac{1}{2}Y - \frac{1}{2}X = \left(\frac{1}{2} - \frac{1}{2}\right)X + \left(\frac{1}{2} + \frac{1}{2}\right)Y = Y. \tag{3}$$

For example, the term −1 2X is encoded by x0 1z0 1r0 1 x1 1z1 1r1 1 x2 1z2 1r2 1 u0u1 because it contains x2 1z2 1 (corresponding to X) and its weight is W(r2 1)· W(u0)· W(u1) = (−1) · √ 1 2 · √ 1 2 = −1 2 . We verify that the constructive interference of the Y terms in (3) (i.e. they add up) results in an aggregate Pauli coefficient γY of **P**2 of 1:

$$MC\_W(F\_{\mathbf{P}^2} \wedge F\_Y) = \frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} + \frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} = 1 = \frac{1}{2} \text{Tr}(Y \cdot \mathbf{P}^2).$$

Similarly, we verify that destructive interference of the X terms in (3) (i.e. they cancel) results in the coefficient γX being 0:

$$MC\_W(F\_{\mathbf{P}^2} \wedge F\_X) = \frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} - \frac{1}{\sqrt{2}} \cdot \frac{1}{\sqrt{2}} = 0 = \frac{1}{2} \text{Tr}(X \cdot \mathbf{P}^2). \tag{7}$$

**Toffoli Gate.** Similar to the way gate encodings of other non-Clifford gates were derived, we can encode the Toffoli gate. To this end, we brute forced the Toffoli gate behavior in the Pauli domain. To keep things readable, we will only present a lookup table in the Pauli basis in Table 3, like Table 1. The corresponding boolean constraint can easily be derived. To subsequently obtain a minimal (weighted) CNF formula, we applied the Quine-McCluskey algorithm [33,44].

**Table 3.** An partial lookup table for the Toffoli gate for in/output Pauli operators P and Q. The extended version of this paper [35] includes the full table.

#### **4.2 WMC-Based Algorithm for Equivalence Checking**

The previous subsection explains how to encode the Pauli coefficients of AP A†, where A is a unitary and P a Pauli string, in a boolean formula together with a weight function. We here connect this encoding to Theorem 1, which expresses that determining whether a unitary A is equivalent to the identity circuit can be done by checking if AP A† ? = P for Pauli strings P ∈ {Xj , Zj | j ∈ [n]}. We use the following lemma, which expresses that for any unitary A and Pauli string P, the P-Pauli coefficient of AP A† can only become 1 if AP A† equals P.

**Lemma 2.** *Let* A *be a unitary and* P ∈ Pˆn *be a Pauli string. Then* AP A† = P *if and only if* 1 2n Tr(AP A† · P) = 1*. Proof.* If APjA† = Pj , then Tr(APjA† · Pj ) = Tr(Pj · Pj ) = Tr(I⊗n) = 2n. For the

converse direction, we observe that Tr(APjA† ·Pj ) is the Frobenius inner product U, V - ≜ Tr(U†V ) for U ≜ APjA† and V ≜ Pj . It now follows from the Cauchy-Schwarz inequality |U, V -|2 ⊔ U, U-·V,V that

$$\begin{aligned} |\operatorname{Tr}(AP\_jA^\dagger \cdot P\_j)|^2 &\stackrel{\text{\tiny\$}}{\operatorname{Tr}}((AP\_jA^\dagger)^\dagger \cdot AP\_jA^\dagger) \cdot \operatorname{Tr}(P\_j^\dagger \cdot P\_j) \\ &= \operatorname{Tr}(AP\_jA^\dagger \cdot AP\_jA^\dagger) \cdot \operatorname{Tr}(P\_j^\dagger \cdot P\_j) \\ &= \operatorname{Tr}(AP\_j \cdot P\_jA^\dagger) \cdot \operatorname{Tr}(I^{\otimes n}) \\ &= \operatorname{Tr}(AA^\dagger) \cdot \operatorname{Tr}(I^{\otimes n}) \qquad \left(\begin{array}{c} A \text{ and } P\_j \text{ are unitary} \\\ \end{array}\right) \\ &= \operatorname{Tr}(I^{\otimes n}) \cdot \operatorname{Tr}(I^{\otimes n}) = 2^n \cdot 2^n = 4^n \qquad \left(\begin{array}{c} A \text{ is unitary} \end{array}\right) \end{aligned}$$

and therefore |Tr(APjA† · Pj )| ⊔ 2n. Since Tr(APjA† · Pj ) = 2n by assumption, the Cauchy-Schwarz inequality is tight, which only happens if U = APjA† and V = Pj are linearly dependent. Thus, there exists a complex number λ such that APjA† =λPj . Substituting this expression in Tr(APjA† ·Pj ) yields Tr(λPj ·Pj )= λ · Tr(I⊗n) = λ2n, hence λ = 1 and APjA† = Pj .

Combining Lemma 2 and Proposition 1 with Theorem 1 yields Corollary 1 below, which in turn implies correctness of Algorithm 1 which reduces equivalence checking to WMC.

**Corollary 1.** *Let* A *be an* n*-qubit circuit with* m *gates and* P ∈{Xj , Zj | j ∈ [n]}*, which are encoded by* FA *and* FP *respectively, with according weight function* W*. We have* A ≡ I *if and only if* MCW (FP (w 0) ∧ FA (vt ) ∧ FP (wm)) = 1 *for all* P ∈ {Xj , Zj | j ∈ [n]}*, where* wt+1 *are boolean variables encoding the quantum state in circuit* A *after the* t*-th gate of* A *(*0 ⊔ t ⊔ m − 1*) and* vt = t∈[m]∪{0} wt *as defined in Eq.* (2)*.*

*Example 6.* Consider A = V †U where =U = (T,T) and V = (S) as in Example 3. We show how to reduce the equivalence check A ? ≡ I to weighted model counting. First, we encode the check AXA† ? =X using F1 ≜ FAXA*†* ∧ FX:

$$\begin{array}{ll} P^0 & \overbrace{\left[\begin{array}{c} \Box \\ U \end{array}\right]}^{P^1} \cdot \left[\begin{array}{c} P^2 \\ \overline{U} \end{array}\right] \cdot \left[\begin{array}{c} S^3 \\ \overline{V} \end{array}\right] & & F\_1 & = \underbrace{x\_1^0 \overline{z\_1^0} \overline{r^0}}\_{F\_{AXA}} \wedge T\_1^0 \wedge T\_1^1 \wedge S\_1^{\dagger,2} & \wedge \underbrace{x\_1^3 \overline{z\_1^3}}\_{F\_X} \end{array}$$

**Algorithm 1.** Quantum circuit equivalence checking algorithm based on WMC. Given an n-qubit circuit A = (G0, G1,...,Gm−1), the algorithm decides whether A is equivalent to the identity circuit.

The satisfying assignments of F1 are

SAT(F1) = {x1 1z1 1r1 1 x2 1z2 1r2 1 x3 1z3 1r3 1 u0u1, x1 1z1 1r1 1 x2 1z2 1r2 1 x3 1z3 1r3 1 u0u1}. so MCW (F1) = σ∈SAT(F1) W(σ(r3 1))W(σ(u0))W(σ(u1)) = √ 1 2 · √ 1 2 + √ 1 2 · √ 1 2 = 1 .

Now we turn to the check AZA† ? = Z, obtaining the formula F2 ≜ FAZA*†* ∧FZ, where FAZA*†* is the same formula from F1 and FZ = x3 1z3 1. The satisfying assignments of F2 are SAT(F2) = {x0 1z0 1r0 1x1 1z1 1r1 1x2 1z2 1r2 1x3 1z3 1r3 1u0u1}, and MCW (F2) = W(r3 1)W(u0)W(u1) = 1. Since both weighted model counts evaluate to 1, we conclude that A ≡ I.

#### **5 Implementation: The ECMC Tool**

We implemented our method in an open-source tool called ECMC, available at https://github.com/System-Verification-Lab/Quokka-Sharp. ECMC takes two quantum circuits in QASM format [13] as input. It encodes these circuits to a sequence of 2n weighted conjunctive normal form (CNF) formulas as explained in Sect. 4, and then uses the weighted model counter GPMC [50] to solve these constraints in parallel, terminating as soon as one returns a negative result. Here we set the number of parallel cores to be 16 as it is shown to be the optimal number of cores for our task.

We choose GPMC as it supports the negative weights in our encoding and performs the best among solvers with that capability in the model counting competition 2023 [21]. To demonstrate the effectiveness of our method, we conducted a set of broad experiments as discussed in the following.

We performed equivalence checking of quantum circuits comparing our method against the state-of-the-art tool QCEC [8], which runs different algorithms and heuristics based on ZX calculus and decision diagrams (shorted as DD) in portfolio with 16 parallel threads [60]. Similar to ECMC, QCEC also terminates earlier when one thread returns "non-equivalent". Since the ZX-calculus based method is still incomplete for universal quantum circuits, in the sense

**Fig. 1.** Equivalence check of typical random Clifford+T circuits against their optimized circuits (equivalent cases, Fig 1 & Fig 2) and optimized circuits with one random gate missing (non-equivalent cases, Fig 3 & Fig 4). (Both vertical axes are on a logarithmic scale.)

that it is only capable of proving equivalence, we use this tool under two settings: one is the default setting which uses DD and ZX calculus in portfolio; the other is to exclusively enable DD [8]. We use two families of circuits: (i) random Clifford+T circuits, which mimic hard problems arising in quantum chemistry [59] and quantum many-body physics [17]; (ii) all benchmarks from the public benchmark suite MQT Bench [43], which includes many important quantum algorithms like QAOA, VQE, QNN, Grover, etc. All experiments have been conducted on a 3.5 GHz M2 Machine with MacOS 13 and 16 GB RAM. We set the time limit to be 5 min (300 s) and include the time to read a QASM file, construct the weighted CNF and perform the model counting in all reported runtimes.

*Results.* First, to show the scalability of both methods on checking equivalence, we consider random circuits that resemble typical oracle implementations—random quantum circuits with varying qubits and depths, which comprise the CX, H, S, and T gates with appearing ratio 10%, 35%, 35%, 20% [41]. We use a ZX-calculus tool PyZX [28] to generate optimized circuits, to construct equivalent, yet very different, counterparts. To construct non-equivalent instances, we inject an error by removing one random gate from the corresponding optimized circuits. So by

construction, we know the correct answer for all equivalence checking instances in advance. The resulting runtimes can be seen in Fig. 1.

In addition to random circuits, to test structural quantum circuits, we empirically evaluated our method on the MQTBench benchmark set [43]. We also generate the optimized circuits of the circuits from MQT-bench using PyZX [28]. To generate non-equivalent instances, three kinds of errors are injected into the optimized circuits: one with a random gate removed, one where a random CNOT gate is flipped, switching control and target qubits, and one where the phase of the angle of a random rotation gate is shifted. For the last error, since many optimizations on rotation gates involve phase shifts in the rotation angles, we consider two sizes of phase shift: one with the angle of a random rotation gate

**Table 5.** Results of verifying non-equivalence of circuits from MQT bench against optimized circuits with flipped CNOT gate (Flipped) and one missing gate (1 Gate Missing). For cases within time limit, we give runtime (sec), while > 300 represents a timeout (5 min).

added by 10−4, one with the angle added by 10−7. We note that this experimental setup is stronger than the one used in [41], where only two errors are considered: bit flip and phase shift without giving the shifting scale. We present a representative subset of equivalence checking results in Table 4. The complete results can be found in the extended version of this paper [35]. The first three columns list the number of qubits n and gates |G| in original circuits, and the number of gates |G | in optimized circuits. Then we give the runtime of the weighted model counting tool ECMC, the decision diagram-based QCEC (DD) and the default setting of QCEC respectively. For the non-equivalent cases, we show the flipped-CNOT and one-gate-missing error in Table 5. The first three columns are the same as Table 4 and then the performance of all three tools on CNOT flipped error and one-gate-missing error respectively. Finally, Table 6 shows the performance of phase shift errors, where Shift-10−4 (resp. Shift-10−4) denotes adding 10−4 (resp. 10−7) to the phase of a random rotation gate.

*Discussion.* For random circuits, Fig. 1 shows that the runtime of ECMC exhibits a clear correlation with the size of the circuits. While QCEC and QCEC (DD) are very fast for small size circuits, for non-equivalent cases, both of them are less scalable and reach time limit much earlier than ECMC. For the equivalent cases, QCEC benefits from ZX calculus and outperforms the other two methods. We suspect that QCEC (DD) shows poor performance when solving random circuits because these circuits don't contain the structure found in quantum algorithms, which decision diagrams can typically exploit.

When considering structural quantum circuits, the results vary between equivalent and non-equivalent instances. For equivalent instances, QCEC (DD) significantly surpasses ECMC on Grover, QFT and QNN, primarily due to the decision diagram-based method's proficiency in handling circuits featuring repeated structures and oracles. While for those circuits featuring a large number of rotation gates with various rotation angles, like graphstate and wstate, ECMC demonstrates clear advantages. Moreover, the default QCEC is much faster than QCEC (DD) on all cases while it reports "no information" for many cases as ZX calculus method and decision diagram method give different answers.

For non-equivalent instances, since ECMC can terminate when a single out of 2n WMC calls returns a negative result, it shows better performance than checking equivalence. For example, in the case of QPE, where both tools face time constraints when checking equivalent instances, ECMC can efficiently demonstrate non-equivalence and resolve the majority of cases within the time limit, while both QCEC and QCEC (DD) still get timeout in most instances.

In all instances, ECMC outperforms both QCEC and QCEC (DD) on graph state and wstate, each featuring many rotation gates. When dealing with rotation gates, decision diagrams might suffer from numerical instability [39,41], as can be clearly observed in Table 6 for the instances with errors in the phase shift, where both QCEC and QCEC (DD) get wrong results for many benchmarks. In contrast, the WMC approach—also numerical in nature—iteratively computes a sum of products, which we think avoids numerical instability. Table 6 also demonstrates this point as ECMC yields the correct answer for most benchmarks with 10−4 and 10−7-size error. In contrast, the default QCEC gives no answer for a large amount of cases.

#### **6 Related Work**

Bauer et al. [3] verify quantum programs by encoding the verification problem in SMT, using an undecidable theory of nonlinear real arithmetic with trigonometric expressions. An SMT theory for quantum computing was proposed in [11]. Berent et al. [4] realize a Clifford circuit simulator and equivalence checker based on a SAT encoding. The equivalence checker was superseded by the deterministic polynomial-time algorithm proposed and implemented in [52]. Using weighted model counting, universal quantum circuit simulation is realized in [34], which we extend by providing encodings for the CZ and Toffoli gates and which we apply to circuit equivalence checking according to the approach of [52]. Amy [2] uses path integrals to check equivalence of circuits, which is complete for Clifford circuits and can prove equivalence of Clifford+T and Clifford+R circuits.

Yu and Palsberg [62] use an abstract interpretation to simulate quantum circuits. Abstraqt [5] improves upon this by using the stabilizer basis. SAT solvers have proven successful in quantum compilation [53], e.g., for reversible simulation of circuits [58] and optimizing space requirements of quantum circuits [36,45].

The ZX calculus [12] offers a diagrammatic approach to manipulate and analyze quantum circuits. A circuit is almost trivially expressible as a diagram, but the diagram language is more powerful and circuit extraction is consequently #Pcomplete [15]. It has proven enormously successful in applications from equivalence checking [41,42], to circuit optimization [28] and simulation [29].

Decision diagrams [37] have been used for simulating quantum circuits, checking their equivalence [8] and synthesis [64]. Jimenez et al. use bisimulation for circuit reduction, reducing simulation time compared to DDs in some cases [26].

# **7 Conclusions**

We have shown circuit equivalence checking reduces to weighted model counting by considering quantum states in the Pauli basis, which allows for an efficient reduction of the equivalence checking problem to weighted model counting. We extended a linear-length encoding with the three-qubit Toffoli gate, so that most common non-Clifford gates are supported (previously the T, phase shift and rotation gates were already supported).

Given two n-qubit quantum circuits, their equivalence (up to global phase) can be decided by 2n calls to a weighted model counter, each with an encoding that is linear in the circuit size. Our open source implementation demonstrates that this technique is competitive to state-of-the-art methods based on a combination of decision diagrams and ZX calculus. This result demonstrates the strength of classical reasoning tools can transfer to the realm of quantum computing, despite the general 'quantum-hardness' of these problems. In future work, we plan to extract diagnostics for non-equivalent circuits from the satisfying assignments of the model counter.

# **References**

14216, pp. 199–216. Springer, Cham (2023). https://doi.org/10.1007/978-3-031- 45332-8 10

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.

# **Author Index**

#### **A**

Acclavio, Matteo II-216 Amrollahi, Daneshvar I-154 Arrial, Victor II-338 Avigad, Jeremy I-3 Ayala-Rincón, Mauricio II-317

#### **B**

Baader, Franz II-279 Balbiani, Philippe II-78 Barragán, Andrés Felipe González II-317 Barrett, Clark I-458 Bártek, Filip I-194 Berg, Jeremias I-396 Bhayat, Ahmed I-75 Biere, Armin I-284 Bonsangue, Marcello II-401 Bozec, Tanguy II-157 Bromberger, Martin I-133 Brown, Chad E.  I-396

#### **N**

Nalon, Cláudia II-3, II-97 Niederhauser, Johannes I-86 Nordström, Jakob I-396

#### **O**

Oertel, Andy I-396 Olivetti, Nicola II-78

#### **P**

Papacchini, Fabio II-3 Pattinson, Dirk II-97 Peltier, Nicolas II-157 Perrault, C. Raymond I-53 Petitjean, Quentin II-157 Platzer, André II-196

Poidomani, Lia M. I-265 Pommellet, Adrien I-366 Prebet, Enguerrand II-196

#### **R**

Rawson, Michael I-115 Rebola-Pardo, Adrian I-325 Ritter, Eike II-61 Rooduijn, Jan II-257 Ruess, Harald II-137

#### **S**

Scatton, Simon I-366 Schmid, Ulrich II-114 Schöpf, Jonas II-298 Schürmann, Carsten II-61 Seidl, Martina I-315, I-325 Shillito, Ian II-43 Sighireanu, Mihaela II-157 Silva, Alexandra II-257 Smallbone, Nicholas I-214 Stan, Daniel I-366 Suda, Martin I-75, I-194, I-214 Summers, Alexander J. I-419 Sutcliffe, Geoff I-30, I-53 Suttner, Christian I-53

#### **T**

Tan, Yong Kiam I-396 Tesi, Matteo II-176 Tinelli, Cesare I-458 Tsiskaridze, Nestan I-458

#### **V**

van Ditmarsch, Hans II-114 Vartanyan, Grigory II-360 Voronkov, Andrei I-21, I-115, I-154

#### **W**

Wagner, Eva Maria I-154 Waldmann, Uwe I-244 Weidenbach, Christoph I-133 Wernhard, Christoph I-172

#### **Y**

Yu, Emily I-284