问题标签 [sat-solvers]

我是 z3 SMT 求解器的新手。我需要定义一个关系，而不是一个函数。我的意思是一个可以返回多个值的函数。我查了教程，找不到任何东西。如果您能在这方面帮助我，我将不胜感激。

谢谢你。

我对 sat4j 求解器和研究布尔可满足问题是全新的；我被卡住了。我想制作一个程序来解决布尔公式中的整数变量，例如；

x1 < x2 + x3 用户输入该公式，我的程序满足该公式（返回真），如 x1 = 5 ，x2 = 3，x3 = 4。所以公式返回真，用户得到满足公式的整数值。是可以在 sat4j 中实现它，因为我使用 java 在 eclipse 中工作。

我正在寻找有关如何将数学方程编码为 cnf-sat 形式的想法，以便它们可以通过像 MiniSat 这样的开源 SAT 求解器来求解。

那么，我该如何转换：

3x + 4y - z = 14

-2x - 4z <= -6

x - 3y + z >= 15

成一个命题方程，可以使用 SAT Solvers 求解。

有什么建议，因为我很难过？？

stackoverflow-ers(?),

我正在玩 z3，我正在尝试解决以下限制：

我在这些约束方面遇到了一些麻烦：a）第一个问题是 z3 忽略了“Restriction #2”

，我得到的值如下：

尽管有限制，但 F*B = D。

b）如果我取消注释“限制 #1”

我得到以下结果：

它是椅子 - 键盘界面错误吗？我究竟做错了什么？

在 Z3 上在线运行。

提前致谢！

我正在使用 Z3 的 Python 绑定，并尝试创建一个属性为函数的 Z3 数据类型。例如，我可能会执行以下操作：

这是尝试Foo使用属性创建数据类型my_function，我可以在其中调用my_function x（如果x是 type 的变量Foo）以获取从整数到布尔值的某些函数。

但是，我在第二行遇到以下错误：

是否可以用函数作为属性声明 Z3 数据类型，也许使用不同的语法？

或者这是不允许的事情？z3 中的 post函数声明向我表明 Z3 中不允许使用高阶函数，因此可能不允许向数据类型添加函数，以防止使用这些数据类型创建高阶函数。

假设我有一个带有 variables 的 CNF 表达式(a,b,c,d,e,f,g)。我将如何使用 SAT 求解器来找到(d,e,f)给定的分配{a,b,c,g} = {1,0,0,1}和{a,b,c,g} = {1,1,1,1}？如果这是一个假设，那么调用 sat 求解器来查找分配{d,e,f}将是直截了当的（例如，通过向 CNF 添加单元子句）。但是如果我有多个假设呢？这可能吗？

我有一组任意约束。例如：

我可以将其转换为可以通过 picosat 解决的 SAT 问题（我无法让 minisat 在我的 Mac 上编译），或者转换为可以通过CVC4解决的 SMT 问题。为此，我需要：

1. 将这些方程映射到布尔电路中。
2. 将 Tseitin 变换应用于电路并将其转换为 DIMACS 格式。

我的问题：

1. 我用什么工具来转换电路？
2. 电路的文件格式有哪些，常用的有哪些？
3. 我使用什么工具将电路转换为 DIMACS 格式？

是否有增量 SMT 求解器或某些增量 SMT 求解器的 API，我可以在其中增量添加约束，我可以通过某个标签/名称唯一标识每个约束？

我想唯一标识约束的原因是我以后可以通过指定该标签/名称来删除它们。需要放弃约束是因为我之前的约束与时间无关。我看到在 Z3 中我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。使用基于假设的 Z3 的其他增量方法，我将不得不执行格式为“(check-sat p1 p2 p3)”的 check-sat，即如果我要检查三个断言，那么我将需要三个布尔常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个布尔常量。我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，

我想知道是否有任何增量求解器可以添加或删除由名称唯一标识的约束，或者是否有 API 可以使用另一种方法来处理它。我将不胜感激任何建议或意见。

我正在使用 Z3 Python 界面为我的实验创建公式。然后我将该公式发送到 Z3 求解器。如果我是正确的 Z3 使用它自己的求解器！

如何在 Z3py 中使用不同的 SAT/SMT 求解器？

我在 CBMC（C 有界模型检查器）中使用的方法：运行程序并吐出中间 DIMAC 表示（在文件中），然后将该文件用作其他 SAT 求解器的输入。我可以在 Z3 中做类似的事情吗？谢谢你。

我试图从http://amit.metodi.me/research/bee/编译 bumblebee sat-solver 。我已经安装了 SWI-Prolog 和 MinGW，但是在 cmd 中输入“make-minisat”后，我得到：

看起来 g++ 无法访问 prolog 头文件。有任何想法吗？我在win 10、64位上工作。