问题标签 [sat-solvers]

我有伪布尔问题，我需要用 sat4j 解决它。

有人能帮我吗？

这是我的问题：

• 我有一个名为：a,b,c,d,e,f 的变量列表

• 我有一个由以下表示的值列表：#1、#2、#3 .....

• h(a,#1) 表示将 #1 分配给 a

我有一些示例约束：

如此多的约束，例如上面的示例。最后，我想要一个将哪个值分配给哪个值的结果。

我怎样才能用 sat4J 解决它？我应该如何表示约束？

如何使用 Prolog 将 CNF 子句转换为 Horn 形式？我正在尝试创建一个以 CNF 作为输入的 SAT Solver，需要将其转换为 Horn 形式。

我正在尝试从这个 git repo - https://github.com/fbacchus/MaxHS设置 MaxHS SAT 求解器。

我收到一条错误消息，显示“/usr/bin/ld: 找不到 -lcplex”。谁能指导我什么是 lcplex 库以及如何解决这个问题？我的控制台看起来像这样..

当使用 MiniSat 作为 C++ 库时，每个新变量都可以创建为决策变量或非决策变量。

我对此的粗略理解是，当求解器决定在分支过程中接下来使用哪个变量时，不考虑非决策变量。但是，在我的项目中，当非决策变量位于蕴涵左侧而不是等价关系时，我遇到了麻烦，因为求解器返回 SAT，即使公式实际上是 UNSAT。

进一步的实验表明，这只发生在非决策变量位于超过 2 个变量的公式中时（我猜 2 变量公式路径是求解器中的一种特殊情况，因此它的行为不同）。

我正在编写一个 SAT 求解器，并开始实施 DPLL 算法。我了解该算法及其工作原理，我还实现了它的一个变体，但困扰我的是接下来的事情。

这是什么意思，这Φ是一组一致的文字？我理解不一致意味着假，这意味着一致意味着不假。true那么，如果当前的分配没有证伪问题，为什么我们可以返回呢？

我实现我的 SAT 求解器的方式是，每当遇到使所有子句都为真的赋值时，我返回那个赋值，算法就完成了。但是由于对于给定的赋值，所有子句都必须为真才能成为问题的解决方案，我不明白，true如果赋值刚好满足问题，怎么能返回（我假设我弄错了在这里，但是既然如果Φ是一致的，那么就意味着它不是假的，但它仍然可以是不可判定的？）。

我正在尝试使用 z3-solver 解决这个
问题，但问题是它给了我错误
的值我试图>>用LShR值更改替换它，但它们都不是正确
的但是我知道值w应该是0x41414141十六进制
我也尝试过设置w为0x41414141，它说它是unsat

SAT解决方案是否有一个名称，其中部分公式是静态的（形成命题“理论”）并用作测试相对较小句子的可满足性的静态上下文。

许多这样的测试需要用不同的句子执行，因此每次重新评估每个小公式与静态部分的连接是次优的。

与增量 SAT 相比，可满足的句子不会附加到理论中，而是在测试后丢弃。

有没有适合这种情况的工具？

我需要一个 SAT 求解器，它不仅可以将 CNF 文件作为输入，还可以将包含命题子句的普通 txt 文件（仅使用and or and not编写）作为输入。

我找不到任何东西。你能指出一个吗？

每次我在同一个问题上运行 minisat 时，我都想得到不同的解决方案。我可以通过使用 minisat 的“rnd-seed”参数来做到这一点。它只是随机化变量选择，所以每次我都能得到不同的解决方案。即使此参数在我的机器（Ubuntu16）上完美运行，它也不适用于在 Ubuntu 机器上运行的 gcloud（谷歌云）。

我想我遗漏了一小部分，但我不知道那是什么。

注意：我不想将解决方案的谈判提供给 minisat 以获得不同的解决方案。我实际上需要随机化变量选择。

编辑：让我解释一下为什么我需要随机解决方案。我解决了很多 SAT 问题，通常这些 SAT 问题看起来很像。所以，如果我不能随机变量选择，我大部分时间都会得到非常相似的解决方案，这是我不想要的。因此，我实际上并没有在同样的问题上运行 minisat。

Edit-2：@sascha 想让我解释一下“有效”和“无效”的含义。当我在我的电脑上运行一个 cnf 文件时，每次我得到不同的解决方案。但是，当我在 gcloud 机器上运行相同的 cnf 文件时，我总是得到相同的解决方案。

我正在尝试用琐碎的方式分析相移故障分析，并遇到了一个非线性方程组来求解。我读过关于 sat-solvers 和 Gaussian 消元的文章，但不幸的是，我在互联网上找到的文章都没有显示如何处理具有大量变量的非线性方程组（这里 trivium 给出了 288 个变量）。所以我现在几乎被困在如何解决这些变量上。