Solving Quantum-Inspired Perfect Matching Problems via Tutte-Theorem-Based Hybrid Boolean Constraints

1 Introduction

Constraint-satisfaction problems (CSPs) [Brailsford et al., 1999] play a fundamental role in mathematics, physics, and computer science. The Boolean SATisfiability problem (SAT) [Biere et al., 2009] is a special class of CSPs, where each variable takes value from {True, False}. Solving SAT efficiently is of utmost significance in computer science, both theoretically and practically [Vardi, 2014]. Though most effort of the SAT community has been put into solving conjunctive-normal-form (CNF) constraints, Boolean satisfiability that also allows hybrid (non-CNF) constraints is used in numerous applications in various areas, e.g., XOR constraints in cryptography [Bogdanov et al., 2011], pseudoBoolean constraints in discrete optimization [Costa et al., 2009; Dinur et al., 2005; Kyrillidis et al., 2020], and more. The combination of different types of constraints enhances the expressive power of Boolean formulas [Feldman et al., 2005].

Extensive research has been done for general-purpose hybrid Boolean constraints solving by a variety of techniques. Given the remarkable success of modern CNF-SAT solvers [Gong and Zhou, 2017; E´en and S¨orensson, 2003; Liang, 2018; Froleyks et al., 2021], a natural approach is to encode hybrid constraints into CNF. Numerous types of encodings with different properties have been developed [Prestwich, 2009]. Some high-level logic-modeling languages such as Answer Set Programming (ASP) [Lifschitz, 2019; Gebser et al., 2019] are also based on CNF encoding. A different technique for hybrid constraints is to handle certain types of constraints natively by devising specialized solvers, such as CNF + XOR [Soos et al., 2009] and pseudoBoolean solvers [Devriendt et al., 2021; Martins et al., 2014]. In addition, there also exist attempts for handling different types of hybrid constraints uniformly [Kyrillidis et al., 2020; Kyrillidis et al., 2021a; Kyrillidis et al., 2021b; Kyrillidis et al., 2022].

In this paper, we study a new application of hybrid constraints that arises in quantum computing, through quantuminspired graph theoretical problems related to perfect matching with vertex color constraints. Solving this problem efficiently provides essential insights into how to design quantum experiments [Jooya et al., 2016; Duncan et al., 2020; Krenn et al., 2022] and advance the realization of large-scale quantum computers [Pan et al., 2012] (see Section 4). Extant algorithmic work on this problem is far from developed, providing no scalable tool to the quantum-computing community. Tackling this problem by solving hybrid constraints is promising for several reasons. First, modern constraint solvers have been well-developed to solve large-scale instances. Second, additional properties of graph instances such as symmetry can be easily integrated as extra constraints, which can be difficult for pure graph theoretical algorithms.

Applying general-purpose hybrid-constraint techniques to the problem above is, however, not trivial. A straightforward encoding of our constrained-matching problem leads to a blow-up of the length of the formula, as also observed in [Cervera-Lierta et al., 2021]. A more advanced encoding based on exact-one constraints yields a considerably long quantified Boolean formula (QBF) with poor scalability. To address those issues, as the main technical contribution of this work, we propose an encoding for the constrained-matching problem based on Tutte's Theorem in graph theory [Anderson, 1971]. Tutte-Berge formula, as a generalized result of Tutte's Theorem, as well as related decompositions, are widely used in computer science and graph theory [Schrijver and others, 2003]. The efficiency of our encoding originates from the short proof of the non-existence of perfect matchings that this encoding offers.

In the experiment section, we evaluated our approach by solving novel benchmark problems that represent important tasks in quantum computing. For a comprehensive comparison, we also implemented a number of competing methods. We demonstrate that our Tutte encoding does not scale well without further optimizations and suitable languages. Specifically, expressing our encodings in high-level languages, such as Answer Set Programming (ASP) or pseudo-Boolean programming (PB), is more convenient. The resulting performance is, however, less than satisfactory. We discover that in conjunctive normal form (CNF) with additional optimizations and advanced SAT solvers, our encodings exponentially outperform other constraint-based and graph theoretical methods, significantly increasing the scalability of the state-ofthe-art. Our implementations provide helpful tools for testing quantum properties efficiently. We conclude that in spite of the progress in general-purpose hybrid constraint solving, specialized encoding techniques are still required to obtain a scalable approach for specific problems.

2 Preliminaries

This section includes a background in hybrid Boolean SAT and definitions in graph theory which are needed for defining the quantum-inspired problem related to perfect matching.

Definition 1. (Boolean satisfiability and hybrid constraints) Let x = (x1, ..., xn) be a sequence of n Boolean variables. A Boolean constraint f(x) is a mapping from a Boolean vector {True,False}n to {True, False}. A formula f = c1∧c2∧· · ·∧cm is the conjunction of Boolean constraints {ci}i=1,··· ,n. There can be multiple types of constraints, e.g.:

• Disjunctive Constraints, e.g., (x1 ∨ x2 ∨ x3).
• Cardinality constraint, e.g., x1 + x2 + x3 ≥ 2, where False and True are interpreted as 0 and 1 respectively. If the constraint is in the form of ∑x∈X x = k, then it can be written as Exact-k(X).
• Pseudo-Boolean (linear) constraints, e.g., 3x1 - 4x2 + 5x3 ≥ 0.
• XOR constraints, e.g., x1 ⊕x2 ⊕x3.

A set of constraints is satisfiable if there exists a Boolean assignment (solution) that evaluates all constraints to True.

Next, we introduce concepts that relate to the quantuminspired graph theoretical problem.

Definition 2. (Bicolored Graphs [Gu et al., 2019a; Vardi and Zhang, 2022]) In this paper, a "graph" refers to an undirected, non-simple 1 graphs. A bicolored graph G is a tuple (V,E, d), where V is the set of vertices with |V |, E is the set of bicolored edges, and d is the number of colors. For each edge e ∈ E that connects u and v, there are two colors ceu , cev ∈ {1, · · · , d} that are associated with u and v, respectively, i.e., e = {(u, ceu ), (v, cev )}. If ceu = cev , we call the edge e monochromatic, otherwise e is bicolored. See Figure 1 (left) as an example.

1 Self-loops are prohibited but multiple edges between the same pair of vertices are allowed.

Definition 3. (Vertex coloring) A vertex coloring of graph G = (V,E, d) is a mapping c from vertices to colors, i.e., c : V → {1, · · · , d}. Alternatively one can write c ∈ {1, · · · , d}V . For a coloring c and a color i ∈ {1, · · · , d}, we use count(c, i) to denote the number of appearances of color i in c.

Definition 4. (Perfect matchings and their inherited vertex colorings) [Krenn et al., 2019] A perfect matching P of a graph G is a subset of edges, i.e., P ⊆ E, such that for each vertex v ∈ V , exactly one edge in P is adjacent to v. For a perfect matching P of a bicolored graph G, its inherited vertex coloring, denoted by cP : V → {1, · · · , d} is defined as follows: for each vertex v, let e be the unique edge that is adjacent to v, then cP (v) = cev . See Figure 1 for examples.

3 Quantum-Inspired Perfect-Matching-Related Problems

In this section, we introduce the graph-theoretical problem that relates to vertex-color-constrained perfect matching, inspired by quantum computing. Roughly speaking, the problem asks whether for each vertex coloring in a set of "legal" vertex colorings, a bicolored graph has at least one perfect matching with this inherited vertex coloring.

Problem 1. (Perfect matchings exist for all legal vertex colorings, abbrv. FORALL-PMVC) Consider a bicolored graph G and a set of C ⊆ {1, · · · , d}V "legal" vertex colorings. Does G satisfy that, for each vertex coloring c ∈ C, G has at least one perfect matching with inherited vertex coloring c?

The hardness of FORALL-PMVC depends heavily on the set of legal vertex colorings C. C can be defined by enumerating all members of the set or by constraints. Below, we list several legal sets of vertex colorings with interest in quantum computing [Gu et al., 2019a; Vardi and Zhang, 2022].

• GHZ State: the legal colorings are monochromatic, i.e., C = {(1, 1, · · · , 1), (2, 2 · · · , 2), · · · , (d, d, · · · , d)}, denoted as GHZ(|V |, d) = 1/√d · ∑di=1 |i⟩⊕|V | .
• W State: the graph has two colors (d = 2). C = {c ∈ {1, · · · , d}V |count(c, 1) = 1}, i.e, there must be exactly one vertex with color 1 and |V | - 1 vertices with color 2, denoted as W(|V |) = 1/√|V | · ˆ S(|2⟩⊕(|V |-1) |1⟩⊕1 )

• Dicke State: a generalization of W State. C = {c ∈ {1, · · · , d}V |count(c, 1) = k} (d = 2), denoted as Dicke(|V |, k) = 1/√(|V | k ) · ˆ S(|2⟩⊕(|V |-k) |1⟩⊕k ).

Complete bicolored graphs trivially satisfy the FORALLPMVC condition for an arbitrary legal coloring set. Nevertheless, graphs with interest in quantum computing are those satisfying the FORALL-PMVC condition with as few edges as possible. In Figure 2, we show examples of such graphs.

The problem of checking the existence of perfect matching is well-known to be polynomial, via the Blossom algorithm [Edmonds, 1965]. We now show that if the size of legal colorings, i.e., |C|, is polynomially bounded, then FORALLPMVC is tractable. The idea is that one can enumerate all legal colorings and verify the existence of perfect matching individually, as formalized in the following proposition.

Definition 5. (Induced graph w.r.t. a vertex coloring) Given a bicolored graph G = (V, E, d) and a vertex coloring c, let Gc = (V,Ec, d) be the subgraph where Ec is a subset of E, defined as follows:

In other words., in Gc, we keep only the edges whose colors agree with the vertex coloring c.

Proposition 1. A bicolored graph G has a perfect matching with inherited vertex coloring c iff Gc has a perfect matching.

With Proposition 1, we can design a polynomial algorithm for FORALL-PMVC with polynomially many legal colorings, as shown in Algorithm 1. We assume Blossom(G) is an algorithm that returns True iff. G has a perfect matching.

Algorithm 1: Enum-Blossom: An EnumerationBased Algorithm for FORALL-PMVC

Input : Bicolored graph G, set of legal colorings C. Output: Whether G satisfies the FORALL-PMVC condition w.r.t. C.

1 for c ∈ C do

• 2 Let Gc be the induced graph of Gw.r.t. c.
• 3 if Blossom(GC)==False then return False;
• 4 return True

Algorithm 1 runs in O(|C| · |E| · |V |2 ). Therefore it provides an efficient algorithm for the FORALL-PMVC problem for GHZ State (|C| = d) and W State (|C| = |V |). The challenging part of FORALL-PMVC is when |C| is exponential, such that it is infeasible to enumerate C. As an example, Dicke(n, n/2) has ( n n/2) = Θ(2n /√n) legal colorings.

The lower bound of the computational complexity of FORALL-PMVC for exponentially many legal colorings remains open, though in [Vardi and Zhang, 2022] the complexity of a related problem is addressed for some special cases. It is not obvious how to reduce a well-known NP-hard or W[1]- hard problem to FORALL-PMVC.

Open Question 1. Is FORALL-PMVC of Dicke State NPhard?

OpenQuestion 2. Is FORALL-PMVC of Dicke(n, k) fixedparameter tractable (FPT) or W[1]-hard w.r.t. k? 2

As for the upper bound, the problem is in co-NP, provided that checking if a coloring c is in C is in PTIME.

Proposition 2. FORALL-PMVC is in co-NP.

Proof. If a graph does not satisfy the condition of FORALLPMVC, then a witness can be obtained as a legal coloring c ∈ C such that Gc has no perfect matching. Such a witness c can be verified in polynomial time by the Blossom Algorithm.

If one views a coloring c as a witness, then the algorithm for checking the witness can be relatively sophisticated, such as the Blossom Algorithm. There exists, however, a more powerful form of witness that allows a simpler checking algorithm, which leads to our approach for solving FORALLPMVC, as shown in Section 5.

4 QuantumMotivation and Impact of FORALL-PMVC

4.1 Perfect Matchings and QuantumCircuits

The motivation of PMVC from the perspective of quantumexperiment design was originally introduced in [Vardi and Zhang, 2022], which we recall here to make this paper selfcontained. An example of a (simplified) quantum optical circuit is shown in Figure 3 (left). A non-linear crystal (shaded box in Figure 3) can emit a pair of entangled photons simultaneously if activated by a laser-pump power. Each photon has a mode, encoded by an integer index. Photons emitted by crystals travel on optical paths. A receiver, which detects the arrival of a photon and identifies photon mode, is placed at the end of each optical path. Each crystal is associated with two optical paths [Gu et al., 2019b].

A coincidence of a quantum optical circuit happens when each receiver detects exactly one photon, due to the activation of some crystals. The quantum state of a coincidence is the mode of photons caught by all receivers in the coincidence. The quantum state of an optical circuit is the superposition [Ballentine, 2014] of the quantum states of all coincidences.

The optical circuit in Figure 3 (left) has 7 nonlinear crystals. A coincidence happens only when crystals in {I,II}, or {I,III}, or {IV,VI} or {V,VII} are activated simultaneously.

2 In [Gaspers et al., 2012], it is proven that deciding whether an uncolored graph has a Tutte set of exactly k vertices is W[1]-hard.

In [Gu et al., 2019b], a coincidence of an optical circuit is shown to be equivalent to a perfect matching under vertexcolor constraints in an undirected graph G with bi-colored edges, as described below.

1. Each optical path corresponds to a vertex in G.
2. Each crystal corresponds to an edge in G. This edge connects two vertices corresponding to two optical paths to which the crystal can emit photons.
3. The modes of photons emitted by crystals correspond to edge colors. Since a crystal can emit two photons with different modes, edges in G are bi-colored.
4. A coincidence of an optical circuit corresponds to a perfect matching P in G. The set of edges in P indicates activated crystals. The quantum state of the coincidence corresponds to the inherited vertex coloring of P .
5. Each crystal has an amplitude as a complex number, corresponding to the edge weight in the graph. The amplitude of a coincidence is the product of the amplitudes of all activated crystals. The weight of a perfect matching is the product of the weights of all its edges.

4.2 Impact of FORALL-PMVC

It is shown in a series of work [Gu et al., 2019a; Gu et al., 2019b] that designing quantum circuits can be done by constructing a graph with bi-colored edges. The ultimate goal of this line of research is to automatically construct bi-colored graphs by combinatorial approaches for arbitrary quantum states, aiming to contribute to the development of large-scale and reliable quantum computers.

The graphs proposed originally in [Gu et al., 2019b] allow complex edge weights, representing the amplitude and phase of the optical components. A quantum state of an optical circuit (resp., graph) can be viewed as a superposition of coincidences (resp., PMs) with predefined "legal" quantum states. An optical circuit (resp., a graph) exhibits a quantum state if 1) the total amplitude (resp., weight) of all coincidences (resp., PMs) of each legal state is 1, and 2) all coincidences (resp., PMs) with an "illegal" state have total amplitude (resp., weight) 0 [Krenn et al., 2017].

The original graph construction problem displays a continuous nature, while in this paper (FORALL-PMVC) as well as [Vardi and Zhang, 2022] (EXISTS-PMVC) we study two simplified, discrete problems, which can be viewed as focusing on the case where edge weights are real and positive. The simplified, discrete setting is not only important in graph theory but also of interest in quantum experiments. Graphs with real, positive edge weights correspond to circuits with optical components with zero-phase. Such a circuit is efficient to set up. Although the existence of graphs with real, positive weights of GHZ states has been studied [Krenn et al., 2019], the simplified setting still remains open and challenging for many other quantum states, e.g., Dicke State. A key feature of our approach is its generality in terms of algorithmically accepting arbitrary user-defined quantum states. In the future, we aim to extend our approach to allow complex weights.

FORALL-PMVC and EXISTS-PMVC test two conditions of whether a graph can be a candidate for displaying a quantum state, under the real-positive-weight-assumption. The algorithms for solving those two decision problems can be applied as building blocks for further developing the actual graph constructors. For instance, a search-based graph constructor can use those algorithms as oracles for quickly pruning unwanted structures in the space of all bi-colored graphs.

5 Boolean Encodings for FORALL-PMVC

In this section we introduce our hybrid-constraint-based approach for FORALL-PMVC. We show that a natural and straightforward Exact-One encoding yields a non-scalable QBF approach. Rather, we exploit the powerful witness of the non-existence of perfect matching provided by Tutte's Theorem to design a novel encoding. We further propose optimization techniques for our Tutte's Theorem-based encoding to enhance the performance.

5.1 The Exact-One Encoding for PMand QBF Encoding for FORALL-PMVC

From the definition of perfect matching, it is natural to use ExactOne constraints to encode perfect-matching-related problems. For each e ∈ E, we introduce a variable edgee, which is True iff e is in the perfect matching:

PM is satisfiable iff the graph has a perfect matching. The variables {edgee}e∈E in PM are existentially quantified. As FORALL-PMVC requires that for each legal coloring the graph has a perfect matching, one can add a universally quantified layer corresponding to vertex colorings. For each vertex v and color i, we define a variable vciv , which is True iff. vertex v has color i. Then FORALL-PMVC can be expressed in the following ∀-∃ quantified Boolean formula (QBF):

ValidColoring is satisfied if the assignment to the vertex-color variables {vc} represents a valid vertex coloring, i.e. each vertex has exactly one color:

LegalColoring includes the constraints that define the set C of legal coloring. For example, for Dicke(|V |, k), we have

Therefore the QBF formula (1) is satisfiable iff. the graph satisfies the FORALL-PMVC condition. Extant QBF solvers, however, accept only problems in CNF format, which requires encoding the implication and cardinality constraints in (1) to CNF. Even using scalable encoding techniques such as Tseytin encoding [Tseitin, 1983], the length of the CNF-QBF formula increases rapidly as the graph scales, which makes QBF solvers perform poorly, as demonstrated in Section 6.

5.2 A Tutte's Theorem-Based Encoding

We show that it is possible to encode FORALL-PMVC with only existential quantifiers, such that a broader set of solvers, e.g., SAT solvers and hybrid Boolean solvers, can be applied. It is enabled by the witness of the non-existence of perfect matching given by Tutte's Theorem.

Theorem 1. (Tutte's Theorem) Let the number of odd connected components (connected components having an odd number of vertices) of a graph G be #odd(G). For a subset V ′ ⊆ V of vertices, let G[V ′ ] be the induced subgraph of G on V ′ . A graph G has no perfect matching if and only if there exists a set S ⊆ V of vertices such that

We call such a set S a Tutte set.

For example, consider the complete bipartite graph Kn-2,n, where every vertex of the first set containing (n-2) vertices is connected to every vertex of the second set including n vertices. It is easy to see that Kn-2,n has no perfect matching. All (n - 2) vertices in the first set form a unique Tutte set, since removing those n-2 vertices yields n isolated vertices, i.e., n odd connected components.

The idea is, with Tutte's Theorem, we can convert the problem of "finding a legal coloring whose induced graph has no perfect matching" to "finding a legal coloring that allows a Tutte set". If for all legal colorings, there exists no Tutte set, then the graph satisfies the FORALL-PMVC condition. In the following, we introduce the details of our encoding for FORALL-PMVC based on Tutte's Theorem.

For each vertex v, we introduce a variable Tv, which is True iff v is in the Tutte set. For each edge {(u, a), (v, b)} ∈ E, we use a variable eab uv to represent whether this edge remains in the induced subgraph G[V \ S]c w.r.t. a vertex coloring c. Then we have:

One of the technical challenges of encoding Tutte's Theorem is how to count odd connected components of G[V \S]c. For each vertex v and an index i of a connected component, we introduce a variable cciv , which is True iff vertex v is in the i-th connected component. Although there can be up to |V | non-empty connected components in G[V \ S]c (consider |V | isolated vertices), multiple connected components are often empty in practice. For two vertices u and v, if they are connected by an edge that remains in G[V \S]c, then they must be in the same connected component, represented by the following constraints:

ConnectedComponent

It is worth pointing out that ConnectedComponent does not enforce different components to be indexed differently. Nevertheless, TutteCondition below is in favor of using as many indices of connected components as possible.

For each vertex v that is not in the Tutte set, we require v to be in exactly one connected component. If v is in the Tutte set, then it does not belong to any of the connected components, represented by:

For each index i (1 ≤ i ≤ |V |) of connected components, we use a variable Oddi to indicate whether the connected component with index i has an odd number of vertices. The set of variables {Odd}i complies with the following set of XOR constraints:

Finally, we enforce that the number of odd connected components in G[V \ S]c is greater than the size of the Tutte set by a cardinality constraint:

Let TutteEncoding be the union of constraints in RemainingEdges, ConnectedComponent, ValidComponent, Odd and TutteCondition, as well as ValidColoring and QuantumState defined previously. Then we have the following proposition, whose proof is delayed to the appendix.

Proposition 3. (Correctness of Tutte encoding) TutteEncoding is satisfiable iff the bicolored graph does not satisfy the FORALL-PMVC condition.

Our Tutte encoding uses |V |2 +|E|+(d+2)·|V | variables.

Remark 1. The Tutte encoding can be alternatively written in ILP, which allows the Boolean vectors for expressing colorings and indices of connected components to be replaced by a single integer variable. Meanwhile, the constraints for ValidComponent and ValidColoring are no longer necessary in the ILP encoding. The evaluation of Tutte encoding on ILP solvers is left as future work.

5.3 Optimizations of the Tutte Encoding

The Tutte encoding we proposed above can be improved, by exploiting the symmetric nature of Tutte set and the input graph. In the following, we describe optimization techniques that reduce the search space by 1) using fewer variables and 2) eliminating redundant solutions. As will be seen in the experiment section, the optimized Tutte encoding scales exponentially better than the vanilla one proposed above.

Exploiting the Symmetry in Tutte's Theorem

Each vertex in V \ S belongs to a connected component. Given a solution of the Tutte encoding, permuting the indices of connected components also generates a solution. To reduce the solution space, we can leave each vertex with fewer options regarding the index of the connected component. Specifically, for a vertex v with 1 ≤ v ≤ |V |, we only keep variables cc1v , · · · , ccvv . That is, a vertex v must belong to a connected component whose index is smaller or equal to v. |V |(|V |-1) 2 variables are removed from the vanilla Tutte encoding.

Additionally, we add constraints to reduce the number of solutions. In spite of that G[V \ S]c can have up to |V | connected components, the number of non-empty connected components is often much smaller than |V |. Therefore, for the same Tutte set, there is still considerable flexibility in the assignment of connected component indices, which we aim to further reduce. If a vertex v is in the Tutte set or belongs to a connected component with an index smaller than v, we can rule out all solutions that contain non-empty connected components indexed by v, expressed by the following constraints:

Exploiting the Symmetry of the Input Graph

One of the advantages of constraint-based approaches is that the properties of the input can be easily taken into account as extra constraints. Previous work has been done in symmetrybreaking by leveraging graph automorphism when solving combinatorial problems by propositional logic [Aloul et al., 2006]. Since adding all potential symmetry-breaking constraints often leads to an exponential overhead, in this work we apply a lightweight symmetry-breaking strategy. If there exists a set U ⊆ V , such that all vertices are equivalent in graph G, i.e., permuting vertices in U leads to a graph isomorphism to G. Then we want the solution of the Tutte encoding to have the smallest lexicographically representative in U.

For such a set U and an order of vertices in U: (u1, · · · , u|U|), we add the following constraints:

Note that our approach is not the only way of breaking symmetry. There exists a trade-off between the size of constraints and solution-space reduction [Walsh, 2006]. We leave investigating the interaction of different symmetry-breaking techniques on FORALL-PMVC as a future work.

6 Experiment Results

This section evaluates our Tutte encoding on solving FORALL-PMVC problems.

6.1 Implementations andMethods in Comparison

RQ1. How do the optimization techniques in Section 5.3 improve the performance of the Tutte encoding?

• RQ2. Among conjunctive normal form (CNF), pseudoBoolean+XOR (PBXOR), and Answer Set Programming (ASP), which language fits best for the Tutte encoding?

RQ3. How do methods based on Tutte encoding perform on FORALL-PMVC benchmarks?

6.2 Implementations and CompetingMethods

We implemented the Tutte encoding in CNF formulas (TutteCNF), pseudo-Boolean+XOR constraints (TuttePBXOR), and Answer Set Programming (TutteASP). Additionally, we implemented the QBF-based approach in Section 5.1 and Algorithm 1 based on the Blossom Algorithm. Our implementations are based on the following software.

• For solving ASP programs, we use Clingo [Gebser et al., 2019]. Due to the powerful expressiveness of ASP, the implementation of Tutte encoding is less than 30 lines of code, which is considerably more compact than CNF and pseudo-Boolean encoding.
• For solving CNF Tutte encoding, we use two SAT solvers: Kissat [Fleury and Heisinger, 2020], a winner of recent SAT Competitions, and Clasp [Gebser et al., 2007], the underneath SAT solver in Clingo in order for fairly comparing CNF with ASP.
• For solving pseudo-Boolean+XOR encoding, we use LinPB [Yang and Meel, 2021], a recent advanced hybrid Boolean constraint solver with native XOR support.
• We implemented Alg. 1 (Enum-Blossom) with Python package networkx [Hagberg and Conway, 2020].
• For solving QBF formulas, we use DepQBF, a medal winner of QBF evaluations [Lonsing and Biere, 2010].

Besides the vanilla Tutte encoding in Section 5.2, we use Tutte[Language]+Opt to denote the Tutte encoding including constraints in OPT defined in Section 5.3 and with unnecessary variables removed. We use Tutte[Language]+Opt+GS to denote the Tutte encoding including constraints in both OPT and GraphSymmetryBreaking.

All experiments were run on single CPU cores of a Linux cluster at 2.60-GHz and with 16 GB of RAM. We set the time limit for each problem instance to 1000 seconds. The implementations and benchmarks can be found in the GitHub repository: https://github.com/zzwonder/PMVC.

Experiment 1: Proving the Non-existence of PM of Uncolored Graphs. We first evaluate the efficiency of Tutte encoding in identifying the non-existence of PM of uncolored graphs, before solving FORALL-PMVC problems. The benchmarks include complete bipartite graphs Kn-2,n for n ∈ {10, 12, 14, · · · , 70}. All graphs have no perfect matching. The first partition with n - 2 vertices forms the unique Tutte set. We compare the Tutte encoding with the Exact-One encoding in Section 5.1, whose unsatisfiability indicates the non-existence of perfect matching. We also include the Blossom Algorithm in comparison. The running time for each algorithm to prove K48,50 has no perfect matching is shown in Table 1 and the comprehensive results are delayed to the appendix. Each running time is the median of 100 independent executions.

Experiment 2: Verifying graphs that satisfy the Dicke FORALL-PMVC conditions. In this experiment, we use different techniques to verify graphs that satisfy the Dicke state. We generate two types of graphs. First, for n ∈ {6, 8, · · · , 40} we generate graphs that satisfy Dicke(n, n/2) (see Section 3 and Figure 2), where the size of legal coloring grows exponentially as n increases. Second, we fix n = 36 and generate graphs that satisfy Dicke(36, k) with k ∈ {1, 2, · · · , 18}. The Tutte-encoding-based approaches are supposed to output "unsatisfiable", as the formula translates to finding a legal coloring with a Tutte set. The results are shown in Figure 4 and 5. Each running time is the median of 100 independent executions.

Experiment 3: Refuting graphs that violate the Dicke FORALL-PMVC conditions. We evaluate the searching power of different approaches via refuting graphs that violates the Dicke state. Tutte-encoding-based approaches are supposed to output "satisfiable". Graphs in this benchmark are obtained by removing edges from graphs that satisfy the Dicke state. For each (n, k) pair where n ∈ {10, 15, 20, · · · , 80}, and k ∈ {0.1 · n, 0.2 · n, 0.3 · n, 0.4 · n}, we first generate 20 graphs that satisfy Dicke(n, k). Then for each graph, we randomly remove either 40% of blue edges or 2 bicolored edges such that the resulting graph violates the Dicke state. In Enum-Blossom, we shuffled the list of legal colorings for more stable performance. The number of instances that each method solved v.s. the running time is plotted in Figure 6.

6.3 Analysis of Results Answer to RQ1

A significant performance enhancement by optimization techniques in Section 5.3 can be observed in Table 1 and Figure 4-6. For example, verifying Dicke(10, 5) was accelerated by 1200 times from TutteCNF (122.7s) to TutteCNF+Opt (0.1s). On searching tasks (Figure 6), TutteCNF+Opt (741) solved 466 more instances than TutteCNF (275). Adding constraints for graph symmetry exploitation also yields great improvement for the verification of relatively large symmetric graphs. TutteCNF+Opt+GS successfully verifies all Dicke graphs in Experiment 2 within 1000s, while TutteCNF+Opt timed out for verifying Dicke(36, 10) and Dicke(34, 17). We conclude that our optimization techniques are critical for the performance of Tutte encoding.

Answer to RQ2

All experiments agree that CNF is the language leading to the best performance for Tutte encoding, with a significant advantage against PBXOR and ASP. The ASP solver Clingo is deployed with a relatively slow SAT solver Clasp with specialized adaptions, which makes it difficult to replace Clasp with a faster SAT solver, e.g., Kissat. To compare CNF encoding with ASP fairly, in Experiment 2 we also solved the Tutte encoding by Clasp. In Figure 4, TutteCNF+Opt (Clasp) still outperforms TutteASP+Opt+GS and TuttePBXOR+Opt+GS by far. We conclude that while highlevel languages such as ASP and PBXOR can be convenient for modeling the problem, low-level languages such as CNF are necessary for better performance.

Answer to RQ3

Experiment 1 (Table 1). When proving the non-existence of perfect matching in uncolored graphs Kn-2,n, the polynomial Blossom Algorithm is the fastest approach as expected. Among all encoding-based approaches, Exact-One encoding with pseudo-Boolean solver (ExactOne-PB) scales best while ExactOne-CNF is the slowest. This observation aligns with the theoretical results about 1) the polynomial behavior of cutting-plane methods [Chandrasekaran et al., 2016] and 2) the exponential lower bound of resolution-based approaches on perfect matching [Razborov, 2004]. Compared with the Blossom Algorithm and ExactOnePB, approaches based on Tutte encoding take a longer time to solve the problem by searching for the unique Tutte set.

Experiment 2 (Figure 4, 5). For the verification of Dicke FORALL-PMVC conditions, all approaches tend to scale exponentially. The QBF encoding presents the worst scalability, which failed to verify Dicke(10, 5) and Dicke(36, 1) within the time limit. Methods based on Vanilla Tutte encoding (TutteCNF) also do not scale well, which only outperform QBF. With optimization techniques, Tutte encodings in ASP and PBXOR languages (TuttePBXOR+Opt+GS, TutteASP+Opt+GS) were able to achieve better scalability, although the Enum-Blossom algorithm still performs better. Only when equipped with both optimization techniques and state-of-the-art SAT solvers (TutteCNF+Opt, TutteCNF+Opt+GS), does the Tutte encoding display promising potential. For verifying graphs that satisfy Dicke(n, n/2), TutteCNF+Opt+GS can successfully verify graphs with n = 40 and TutteCNF+Opt is able to solve for n = 34 within

1000s, both of which scale exponentially better than EnumBlossom (n = 26) and QBF (n = 8) according to Figure 4. As for verifying Dicke(36, k) (Figure 5), when k is small (k ≤ 2), the set of legal coloring is polynomially bounded and Enum-Blossom is the fastest algorithm. As k increases, optimized CNF Tutte encoding with SAT solvers dominates other approaches by far.

Experiment 3 (Figure 6). On identifying graphs that violate FORALL-PMVC conditions, QBF only solved 8 instances (1280 in total). TuttePBXOR+Opt and EnumBlossom solved 503 and 529 instances respectively. EnumBlossom is able to solve relatively small-size instances quickly (within 0.1s). The optimized Tutte encoding in CNF (TutteCNF+Opt) solved 741 instances, which outperforms Enum-Blossom mainly on large-size problems.

Summary. Not surprisingly, the Blossom Algorithm dominates constraint-based approaches in proving the nonexistence of PM for uncolored graphs. However, when solving FORALL-PMVC tasks with vertex coloring involved, our method displays promising performance, especially when the legal coloring set grows exponentially. The vanilla Tutte encoding does not scale well without optimization techniques and suitable language. With modern CNF-SAT solvers, optimized Tutte encoding scales exponentially better than QBF and a graph theoretical algorithm (Enum-Blossom) on FORALL-PMVC problems. We conclude that while hybridconstraint-based techniques are powerful and expressive, extra effort is necessary for solving FORALL-PMVC efficiently. Our approaches also scale significantly better than previous implementations for similar tasks from the quantumcomputing community. The graph instances used in previous work have less than 15 vertices [Cervera-Lierta et al., 2021].

7 Conclusions and Future Directions

In this paper, we study a new application of hybrid Boolean constraints, named FORALL-PMVC, which arises in quantum computing. We propose a novel encoding based on Tutte's Theorem in graph theory as well as optimization techniques for this encoding. Empirical results demonstrate that in the most suitable encoding language (CNF), our approach based on optimized Tutte encoding scales significantly better than competing approaches on tasks with interest in quantum computing. Our study identifies the necessity of designing problem-specific encodings when applying powerful generalpurpose constraint solvers. Our implementations also provide useful tools for the quantum computing community.

For future directions, we plan to apply constraint-based methods to solve problems beyond graph property checking. For example, the ultimate goal of this line of research [Cervera-Lierta et al., 2021] is to construct a graph w.r.t. a quantum state. Considering an alternative constraintprogramming approach for our problem based on filtering algorithms and All-Different constraints [Bessiere et al., 2010] is another interesting direction. It is also promising to apply our Tutte encoding for solving graph theoretical problems related to Tutte's Theorem algorithmically [Bauer et al., 2007].

Acknowledgements

Work supported in part by NSF grants IIS-1527668, CCF1704883, IIS-1830549, DoD MURI grant N00014-20-12787, Andrew Ladd Graduate Fellowship of Rice Ken Kennedy Institute, and an award from the Maryland Procurement Office. We thank the anonymous reviewers for helping improve the paper.

Contribution Statement

The author list has been sorted alphabetically by last name. Zhiwei Zhang is the corresponding author.