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.

翻译：判定具有不同类型约束（即混合约束）的布尔约束满足问题的可满足性是一个研究充分且具有重要应用的问题。本文研究了量子计算中产生的一类新型混合布尔约束应用，该问题涉及边着色图中的约束完美匹配。尽管通用混合约束求解器功能强大，但研究表明将约束匹配问题直接编码为混合约束的扩展性较差，仍需采用特殊技术。我们提出了一种基于图论中Tutte定理的新型编码方案及优化技术。实验结果表明，在配备先进SAT求解器的合适语言框架下，我们的编码在约束匹配基准测试中的扩展性显著优于多种竞争方法。本研究揭示了在应用强大通用约束求解器时，设计特定问题编码的必要性。