在SAT求解中利用动态命题逻辑结构
计算机科学中的逻辑
2011-06-08 v1 离散数学
摘要
32位hwb问题（简称hwb-n32）源于对计算隐藏加权比特函数的两个电路进行等价性检查。自2002年以来，该问题在每一次SAT竞赛中仍无法求解。本文聚焦于解决诸如hwb-n32之类的问题。一般而言，现代求解器只能检测XOR、AND、OR和ITE门。其他非子句公式（命题逻辑结构）无法被检测。为解决hwb-n32问题，我们动态提取了一些特殊的命题逻辑结构，然后使用基于DPLL的求解器的一个变体来求解由提取的结构信息简化后的子问题。利用动态提取技术，我们高效地解决了hwb-n32问题，其中一些甚至在3000秒内被求解。
引用
@article{arxiv.1106.1370,
title = {Exploiting Dynamically Propositional Logic Structures in SAT},
author = {Jingchao Chen},
journal= {arXiv preprint arXiv:1106.1370},
year = {2011}
}
备注
6 pages