SAT v CSP
SAT v CSP
复制标题
DOI：
10.1007/3-540-45349-0_32
复制
发表时间：
2000-09
期刊：
影响因子：
--
通讯作者：
T. Walsh
中科院分区：
文献类型：
--
作者：
T. Walsh
我们对约束满足问题（CSP）和命题可满足性（SAT）之间的映射进行了全面的研究。我们分析了 SAT 问题到 CSP 的四种不同映射，以及其中两种 CSP 到 SAT 问题的映射。对于每个映射，我们比较了在 CSP 上实现弧一致性与 SAT 问题上的单元传播的影响。然后，我们将这些结果扩展到在搜索过程中保持（某种程度）弧一致性的 CSP 算法，如 FC 和 MAC，以及 Davis-Putnam 过程（在每个搜索节点执行单元传播）。由于搜索的分支结构存在差异，显示在 SAT 问题上 CSP 上实现弧一致性相对于单元传播的优势的结果并不一定转化为 MAC 相对于 Davis-Putnam 过程的优势。这些结果提供了对命题可满足性和约束满足之间关系的深入了解。
We perform a comprehensive study of mappings between constraint satisfaction problems (CSPs) and propositional satisfiability (SAT). We analyse four different mappings of SAT problems into CSPs, and two of CSPs into SAT problems. For each mapping, we compare the impact of achieving arc-consistency on the CSP with unit propagation on the SAT problem. We then extend these results to CSP algorithms that maintain (some level of) arc-consistency during search like FC and MAC, and to the Davis-Putnam procedure (which performs unit propagation at each search node). Because of differences in the branching structure of their search, a result showing the dominance of achieving arc-consistency on the CSP over unit propagation on the SAT problem does not necessarily translate to the dominance of MAC over the Davis-Putnam procedure. These results provide insight into the relationship between propositional satisfiability and constraint satisfaction.