小 SAT 求解器 强调代码的简单性，而不是性能，至少现在是这样 灵感来自： 运行基准 您可以从这里下载 .cnf 文件 ，提取文件以便 Makefile 可以看到它们（例如，提取 uf20-91.tar.tar.gz）。 gz 进入目录“uf20-91”，确保该目录包含在 SRC 变量中） 去做 看了minisat论文，界面不是很好... 有协程吗？ 尝试找到一种方法来解决所有可能的解决方案，知道我们只会得到第一个 CNF / 基准 介绍 ( ) 进一步阅读 维基百科 http://en.wikipedia.org/wiki/Boolean_satisfiability_problem http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories http://en.wikipedia.org/wiki/DPLL_a