|
|
2 回复 | 直到 11 年前
|
1
8
这个 Davis-Putnam-Logemann-Loveland page on Wikipedia 有一个很好的概述。 那你就可以看迷你报纸了 "An Extensible SAT-solver" . 你也应该阅读 "GRASP - A New Search Algorithm for Satisfiability" 了解minisat中使用的冲突驱动学习算法。 我可以很容易地使用这些资源在Python中编写SAT解算器。我的 sat.py 代码是可用的(目前是lgpl 2.1),但它是最近的,所以可能仍然包含bug。它缺乏一些来自minitat设计的优化;如果您想要原始速度,请使用minitat代码;-) 更新:我还做了一个OCAML版本, sat.ml ,这样可以更容易地看到类型。 |
|
|
2
0
一本好书是:Uwe Sch_《宁》;Jacobo Tor_n——满足性问题 |
推荐文章
|
|
Okonjo Mitchel · CS50凯撒:分段故障问题 4 年前 |
|
|
Baraa · 而我在java中得到无限的while循环 4 年前 |
|
|
deficiencyOn · 用DP求解“背包” 8 年前 |
|
|
Robbie · 使用嵌套的if-else语句理解Do-While循环 8 年前 |
|
|
Andrei · 查找两个数组中的差异[重复] 8 年前 |
|
|
Shkarik · 为什么我在Scala中的二进制搜索实现如此缓慢? 8 年前 |