论文标题
通过张量产品测试约束满意度问题的难以满足
Testing Unsatisfiability of Constraint Satisfaction Problems via Tensor Products
论文作者
论文摘要
我们研究随机局部搜索方法的设计，以证明约束满意度问题（CSP）的难以满足。对于二进制CSP，已经使用CSP的微观结构设计了此类方法。在这里，我们开发了将微结构分解为图张量的方法。我们展示了如何使用张量分解来有效且并行计算不可满足性的证明。我们还提供了大量的经验证据，表明我们的方法可以改善实践。例如，一个分解产生了一半时间不牺牲质量的证据。与先前的方法相比，另一个分解是在十分之三的速度快二十倍。我们的方法适用于使用众所周知的双重和隐藏变量转换从任意CSP到二进制CSP的任意CSP。
We study the design of stochastic local search methods to prove unsatisfiability of a constraint satisfaction problem (CSP). For a binary CSP, such methods have been designed using the microstructure of the CSP. Here, we develop a method to decompose the microstructure into graph tensors. We show how to use the tensor decomposition to compute a proof of unsatisfiability efficiently and in parallel. We also offer substantial empirical evidence that our approach improves the praxis. For instance, one decomposition yields proofs of unsatisfiability in half the time without sacrificing the quality. Another decomposition is twenty times faster and effective three-tenths of the times compared to the prior method. Our method is applicable to arbitrary CSPs using the well known dual and hidden variable transformations from an arbitrary CSP to a binary CSP.
