布尔可满足性的泛化 I：背景与现有工作综述
人工智能
2011-07-04 v1
摘要
本文是计划中三篇描述ZAP（一个可满足性引擎）论文的第一篇。ZAP在保留现代高性能求解器性能特征的同时，对现有工具进行了实质性的泛化。ZAP的基本思想是：许多传递给此类引擎的问题包含丰富的内部结构，但这些结构被所使用的布尔表示所掩盖；我们的目标是定义一种表示，使这种结构清晰可见并能被轻易利用以提高计算性能。本文是对ZAP背后工作的综述，讨论了先前通过利用所求解问题的结构来提升Davis-Putnam-Logemann-Loveland算法性能的尝试。我们考察了现有思想，包括对布尔语言的扩展以允许基数约束、伪布尔表示、对称性以及一种受限的量化形式。虽然本文旨在作为综述，但我们的研究成果包含在后续两篇文章中：本系列的第二篇论文将描述ZAP的理论结构，第三篇将描述ZAP的实现。
引用
@article{arxiv.1107.0040,
title = {Generalizing Boolean Satisfiability I: Background and Survey of Existing Work},
author = {H. E. Dixon and M. L. Ginsberg and A. J. Parkes},
journal= {arXiv preprint arXiv:1107.0040},
year = {2011}
}