问题标签 [sat-solvers]

这是我的程序，当图中存在循环时返回 SAT，当没有循环时返回 UNSAT：

我想在没有周期（ UNSAT ）时获取模型。我意识到我应该使用命令 (get-unsat-core) 并将选项设置为 (set-option :produce-unsat-cores true) ：

我收到此错误：

DPLL SAT 求解器通常应用Phase Saving启发式算法。这个想法是记住每个变量的最后一次赋值并在分支中 首先使用它。

为了试验分支极性和相位节省的效果，我尝试了几个 SAT 求解器并修改了相位设置。都是Windows 64 位端口，以单线程模式运行。我总是使用中等复杂度的相同示例输入（5619 个变量，11261 个子句，在解决方案中，所有变量的 4% 为真，96% 为假）。

下面列出了生成的运行时间：

这可能只是（坏）运气，但差异非常大。在我的例子中， MiniSat的表现优于所有现代求解器，这让我感到特别惊讶。

我的问题：

对这些差异有任何解释吗？
极性和相位节省的最佳实践？

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

I'm working on a CDCL SAT-Solver. I don't know how to implement non-chronological backtracking. Is this even possible with recursion or is it only possible in a iterative approach.

Actually what i have done jet is implemented a DPLL Solver which works with recursion. The great differnece from DPLL and CDCL ist that the backracking in the tree is not chronological. Is it even possible to implement something like this with recursion. In my opionion i have two choices in the node of the binary-decision-tree if one of to path leads i a conlict:

1. I try the other path -> but then it would be the same like the DPLL, means a chronological backtracking
2. I return: But then i will never come back to this node.

So am i missing here something. Could it be that the only option is to implement it iterativly?

我正在尝试在我的程序生成的一堆 cnf 编码上运行 SAT 求解器。我已经通过自制软件在我的笔记本电脑（MacOS）上安装了 minisat，我可以在终端上运行 minisat：

$ minisat INPUT_FILE.cnf OUTPUT_FILE.txt

但是因为我有数百种编码，所以我使用subprocess. 编码是在for循环内生成的。该循环还包含子进程命令，理想情况下，SAT 求解器 (minisat) 在每个循环上运行每个文件。

cnf 编码生成良好，我可以在终端上单独运行它们，但是当我尝试运行使用 subprocess 命令时，它会抛出一个错误说：

FileNotFoundError: [Errno 2] No such file or directory: 'minisat': 'minisat'

这是我的代码（它只是我的代码的一部分，我省略了不相关的部分）：

编辑：在此处提到的其他几个解决方案中，建议添加，但这会在打印时shell=True抛出minisat: command not founderr

Z3 输入格式是SMT-LIB 2.0标准定义的格式的扩展。输入表达式需要以前缀形式编写。例如rise4fun，

x + (y * 2) = 20需要以“ (= (+ x (* 2 y)) 20))的形式给出输入。

Z3 支持JAVA API。例如，让我们考虑以下评估和检查可满足性表达式的代码：x+y = 500和x + (y * 2) = 20。

问题是如果外部用户想给求解器提供输入，他不能以“x+y = 500, x + (y * 2) = 20”的一般公式的形式给出。输入需要解析，然后应该使用 JAVA API 以前缀形式手动编写（注意上面代码中的BoolExpr t2），以将最终表达式提供给 Solver。

是否有任何解析器/库/API（最好是 JAVA 或任何其他语言）使用算术运算符（+、-、<、>、=）、命题逻辑连接器（And、OR）、量词（ForAll、存在）然后向 Z3 Solvers 提供输入？

请建议和帮助。

我正在尝试使用 Z3py 优化基于最小化的集合覆盖问题（SCP41）的一个实例。

结果如下：

使用

（1）我知道Z3支持优化（https://rise4fun.com/Z3/tutorial/optimization）。很多时候我在 SCP41 和其他实例中达到了最佳状态，但也有一些没有。

(2) 我知道，如果我在没有优化模块的情况下使用Z3py API，我将不得不执行@Leonardo de Moura在（整数变量的最小值和最大值）中描述的典型顺序搜索。它永远不会给我结果。

我的方法

（3）我试图通过实现类似于它在（Z3 是否支持优化问题）中解释@Philippe 的二进制搜索来改进顺序搜索方法，当我运行我的算法时它会等待并且我没有得到任何结果。

我知道二进制搜索应该更快并且在这种情况下工作？我也知道实例 SCP41 很大，产生了许多限制，它变得非常具有组合性，这是我的完整代码（代码大实例），这是我的二进制搜索：

而且，这是我在初始测试中使用的另一个实例（代码短实例），它在任何情况下都运行良好。

什么是不正确的二分搜索或 Z3 的某些概念未正确应用？

问候，亚历克斯

Given a set of possible values for each variable and two equations, I wrote the below code to get the exact variable values. But Z3 is giving Unsat results.

I have created 7 instances and combined them to make a single one. And passed the instance to the z3 solver. But getting unsat result as a response but clearly it can be seen there exists a valid solution. Below is the code I have written:

一般来说，一阶逻辑是Undecidable。但是，一阶逻辑的一些片段，如 Monadic 逻辑、BSR 片段、分离片段是可判定的。

存在解决 SAT/SMT 求解器的工具，如 Z3。是否有任何工具/语言可以检查 FOL 公式的可满足性？

我知道，给定 N 中最多 k 个工具，我可以通过将其更改为 N 中最多 (nk) 来得到 N 中的至少 K。

但我似乎无法理解这是怎么回事。我可能会遗漏一些非常微不足道的东西

例如，如果 K=2 和 N=6，如何至少 2 out of 6 等于最多 4 out of 6

任何帮助，将不胜感激