广义布尔可满足性 III：实现
人工智能
2011-09-13 v1
摘要
这是描述 ZAP 的三篇系列论文中的第三篇。ZAP 是一个可满足性引擎，它在大幅推广现有工具的同时，保留了现代高性能求解器的性能特征。ZAP 的基本思想在于，传递给此类引擎的许多问题包含丰富的内部结构，而这些结构被所使用的布尔表示所掩盖；我们的目标是定义一种表示法，使该结构显而易见并能被利用以提升计算性能。第一篇论文综述了（有意或无意地）利用问题结构来提升可满足性引擎性能的现有工作，第二篇论文则表明该结构可以理解为在任何特定布尔理论中对单个子句起作用的置换群。作为本系列的总结，我们讨论了实现我们思想所需的技术，并报告了它们在多种问题实例上的性能表现。
引用
@article{arxiv.1109.2142,
title = {Generalizing Boolean Satisfiability III: Implementation},
author = {H. E. Dixon and M. L. Ginsberg and D. Hofer and E. M. Luks and A. J. Parkes},
journal= {arXiv preprint arXiv:1109.2142},
year = {2011}
}