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

arXiv: https://arxiv.org/abs/2301.09833 · HTML: https://mlsanity.com/paper/2301.09833/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 72 references that are in the map.
- First posted on arXiv 24 Jan 2023.

## Builds on (most cited first, 7 of 7)

- [Multi-shot ASP solving with clingo](https://mlsanity.com/paper/1705.09811/) (2017)
- [Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus](https://mlsanity.com/paper/1902.03178/) (2019)
- [FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints](https://mlsanity.com/paper/1912.01032/) (2019)
- [On Continuous Local BDD-Based Search for Hybrid SAT Solving](https://mlsanity.com/paper/2012.07983/) (2020)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Quantum-Inspired Perfect Matching under Vertex-Color Constraints](https://mlsanity.com/paper/2209.13063/) (2022)
- [Design of quantum optical experiments with logic artificial intelligence](https://mlsanity.com/paper/2109.13273/) (2021)

## Built on by (most cited first, 3 of 3)

- [Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs](https://mlsanity.com/paper/2308.15020/) (2023)
- [Analysis of Higher-Order Ising Hamiltonians](https://mlsanity.com/paper/2412.13489/) (2024)
- [Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization](https://mlsanity.com/paper/2506.00674/) (2025)

## Abstract (arXiv)

Determining the satisfiability of Boolean constraint-satisfaction problems with different types of constraints, that is hybrid constraints, is a well-studied problem with important applications. We study here a new application of hybrid Boolean constraints, which arises in quantum computing. The problem relates to constrained perfect matching in edge-colored graphs. While general-purpose hybrid constraint solvers can be powerful, we show that direct encodings of the constrained-matching problem as hybrid constraints scale poorly and special techniques are still needed. We propose a novel encoding based on Tutte's Theorem in graph theory as well as optimization techniques. Empirical results demonstrate that our encoding, in suitable languages with advanced SAT solvers, scales significantly better than a number of competing approaches on constrained-matching benchmarks. Our study identifies the necessity of designing problem-specific encodings when applying powerful general-purpose constraint solvers.