I was able to write a SAT solver in Python quite easily using those resources. My sat.py code is available (LGPL 2.1 currently), but it's quite recent so may still contain bugs. It lacks a few optimisations from the minisat design; if you want raw speed use the minisat code ;-)
Update: I've also made an OCaml version, sat.ml, which might make it easier to see the types.
发布评论
评论（2）
维基百科上的Davis-Putnam-Logemann-Loveland 页面提供了很好的概述。
那么您应该能够遵循 minisat 论文“An Extensible SAT-solver”。
您还应该阅读 “GRASP - 一种新的可满足性搜索算法” 了解 minisat 中使用的冲突驱动学习算法。
我能够使用这些资源轻松地用 Python 编写 SAT 求解器。我的 sat.py 代码可用（当前为 LGPL 2.1），但它是最近的，因此可能仍然包含错误。它缺乏小型卫星设计的一些优化；如果您想要原始速度，请使用 minisat 代码；-)
更新：我还制作了 OCaml 版本，sat.ml，这可能会更容易查看类型。
The Davis-Putnam-Logemann-Loveland page on Wikipedia has a good overview.
Then you should be able to follow the minisat paper "An Extensible SAT-solver".
You should also read "GRASP - A New Search Algorithm for Satisfiability" to understand the conflict-driven learning algorithm used in minisat.
I was able to write a SAT solver in Python quite easily using those resources. My sat.py code is available (LGPL 2.1 currently), but it's quite recent so may still contain bugs. It lacks a few optimisations from the minisat design; if you want raw speed use the minisat code ;-)
Update: I've also made an OCaml version, sat.ml, which might make it easier to see the types.
一本好书是：Uwe Schöning； Jacobo Torán - 可满足性问题
A good Book is: Uwe Schöning; Jacobo Torán - The Satisfiability Problem