一族用于将伪布尔约束转换为 SAT 的编码方法

Amir Aavani

一族用于将伪布尔约束转换为 SAT 的编码方法

计算机科学中的逻辑 2015-03-19 v3 数据结构与算法

作者: Amir Aavani

摘要

伪布尔 (PB) 约束是关于布尔变量的线性算术约束。PB 约束在表达 NP 完全问题时方便且被广泛使用。我们引入了一种新的、两步式的方法，用于将 PB 约束转换为命题 CNF 公式。第一步涉及将每个 PB 约束重写为 PB-Mod 约束的合取。其优点是 PB-Mod 约束更容易转换为 CNF。在第二步中，我们将上一步得到的每个 PB-Mod 约束转换为 CNF。生成的 CNF 公式规模较小，并且单元传播能够推导出使用其他常用转换方法得到的 CNF 公式所无法推导出的事实。我们还刻画了那些可以预期 SAT 求解器在生成的 CNF 上表现良好的约束类型。我们表明，对于许多约束，所提出的编码方法具有良好的性能。

关键词

伪布尔约束 SAT 编码 CNF 转换 PB-Mod 约束单元传播 SAT 求解器

引用

@article{arxiv.1104.1479,
  title  = {A Family of Encodings for Translating Pseudo-Boolean Constraints into SAT},
  author = {Amir Aavani},
  journal= {arXiv preprint arXiv:1104.1479},
  year   = {2015}
}

备注

Used as the reference for SAT-2013 submission

一族用于将伪布尔约束转换为 SAT 的编码方法

摘要

关键词

引用

备注

相关论文