Abstract
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.
Abstract (translated)
确定具有不同约束类型的综合性布尔满足问题是否满足条件,也就是混合约束,是一个备受研究的具有重要应用的问题。在这里,我们研究了一种在量子计算中提出的混合布尔约束的应用。该问题与边色图形的约束完美匹配有关。虽然通用的混合约束求解器可以功能强大,但我们表明,将约束匹配问题直接编码为混合约束的 scaling 较差,并且仍然需要特殊技巧。我们提出了基于 graph 理论的 Tutte 定理和优化技巧的新编码方案。实证结果表明,我们的编码,在与先进的 SAT 求解器兼容的语言中,在约束匹配基准问题上 scales significantly better than 几种竞争方法。我们的研究确定了在应用功能强大的通用约束求解器时,设计问题特定的编码的必要性。
URL
https://arxiv.org/abs/2301.09833
