Jul*_*les 3 computer-science sat-solvers
在SAT(布尔可满足性问题)求解器上阅读哪些好文档.我无法通过Google找到好的资料.我发现的文件要么是鸟瞰图,要么太高级或损坏的PDF文件......
您建议哪些论文/文档了解现代实用SAT求解器中的算法？
维基百科上的Davis-Putnam-Logemann-Loveland页面有一个很好的概述.
然后你应该能够遵循minisat论文"可扩展的SAT解算器".
您还应该阅读"GRASP - 一种新的可满足性搜索算法"来理解minisat中使用的冲突驱动学习算法.
我能够使用这些资源很容易地在Python中编写SAT求解器.我的sat.py代码是可用的(目前是LGPL 2.1),但它是最近的,所以可能仍然包含错误.它缺乏一些minisat设计的优化; 如果你想要原始速度使用minisat代码;-)
更新:我还制作了一个OCaml版本,sat.ml,这可能会更容易看到类型.