标签: sat-solvers

在SAT(布尔可满足性问题)求解器上阅读哪些好文档.我无法通过Google找到好的资料.我发现的文件要么是鸟瞰图,要么太高级或损坏的PDF文件......

您建议哪些论文/文档了解现代实用SAT求解器中的算法？

我需要使用sat解算器来检查布尔表达式的可满足性.

我有像这样的复杂布尔表达式

是否有任何自动cnf文件转换器,以便我可以直接给坐在求解器？

我读了cnf格式文件..但是如何在.cnf文件中表达这个表达式？当paranthesis里面有一个连词以及如何表达时,我会感到困惑 - >和< - >？请帮我

我是 Z3 的新手，正在尝试制作一个求解器，将每个可满足的解决方案返回到布尔公式。从其他 SO 帖子中记下笔记，我已经编写了我希望能起作用的代码，但事实并非如此。问题似乎是，通过添加以前的解决方案，我删除了一些变量，但它们又在后面的解决方案中返回了？

目前我只是想解决a或b或c。

如果我解释得不好，请告诉我，我会尽力进一步解释。

预先感谢您的回复:)

我的代码：

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

while (s.check() == sat):
        print(s.check())
        print(s)
        print(s.model())
        print(s.model().decls())
        print("\n")
        s.add(Or([ f() != s.model()[f] for f in s.model().decls() if f.arity() == 0])) 

我的输出：

sat
[Or(a, b, c)]
[c = False, b = False, a = True]
[c, b, a]


sat
[Or(a, b, c), Or(c != False, b != False, a != True)]
[b = True, …

我目前正在使用 ocaml 4.06.0 并且我正在尝试使用 Z3 sat 求解器。我正在使用 opam 的 oasis 来编译文件（它成功地构建了所有内容）。但是，当我运行生成的本机代码时，出现以下错误：error while loading shared libraries: libz3.so. 我尝试重新安装 z3 软件包，但错误仍然存​​在。谁能帮我解决这个问题，因为我不知道还能尝试什么？