问题标签 [sat-solvers]

我一直在尝试使用 minisat API 解决 SAT 实例，但由于某种原因，minisat 在打印结果时非常慢。我很确定我在 API 调用中做错了，因为我自己实现了 sat 求解器，并且 minisat 在我正在检查的实例上不应该那么慢（我自己实现的求解器在 4 秒内输出）

下面是我写的代码。

PS我已经尝试删除松弛变量它仍然很慢

minisat 中是否有任何 API 调用来提取 unsat 核心或任何其他方法。

我想为求解器的每次调用提取 unsat 核心，然后处理 unsat 核心。

我有两个逻辑输出，我知道它们在逻辑上是等效的（使用 SAT 求解器证明）。现在我从两个信号中选择相同的位。我可以说既然完整的信号是等效的，那么子信号也将是等效的吗？

例如。N 位信号 - Signal-1 和 Signal-2 这两者在逻辑上是等效的。现在我从 Signal-1 中提取 0:1，从 Signal-2 中提取 0:1，现在我想知道这两个新信号的等价性。我可以肯定地说这些将是等效的吗？

我认为它们是等效的，如果我遗漏了什么，请告诉我，或者在任何情况下都可能有所不同。

我和我的朋友从标题收到问题来解决。

我们发现了很好用的 SAT Solver Cryptominisat。

我们还发现了一篇关于将 VTML 转换为 Sat Article的长文章。我们将从 python 生成规则/限制。

我们实际上发现了将整个图转换为布尔规则的障碍。我们也

根据文章，我手动编写了 cnf 子句。2开头是Y，

1 是 X X1,1 -> 111

我知道上述两种算法都属于迭代解决方案以找到 MAXSAT 问题的最佳解决方案，但我想知道为什么从可满足方面开始同时为 MAXSAT 找到解决方案比从不可满足方面搜索更好？

同样在这里，可满足方面意味着放宽所有可能的软条款，直到我们达到 UNSAT 和不可满足方面意味着从不放宽条款开始增加数量，直到我们达到 SAT

我对 MaxSat 有一个想法，并且已经使用 MSU3 以及使用 minisat API 的顺序编码实现了一个简单的 Maxsat 求解器

我想知道是否有办法加快这个求解器的速度。

我附带了这篇论文： https ://www.researchgate.net/publication/264936663_Incremental_Cardinality_Constraints_for_MaxSAT

这谈到了增量弱化及其使用累加器编码的实现

有没有办法通过顺序编码来实现增量弱化？

这会大大加快速度吗？

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

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

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

提前感谢您的回复:)

我的代码：

我的输出：

z3.Bool() 和 z3.FreshBool() 函数有什么区别？当我使用 Bool() 时，我在 python 上的 z3 中的代码失败（当求解器不应该返回 unsat 时），但是当我使用 FreshBool() 时工作​​正常（观察到所需的行为）。

我不能在这里提供代码的详细信息，因为它是我大学提供的课程中正在进行的作业的一部分。尽管如此，如果这些信息还不够，我可以尝试在不相关的代码中重新创建，为您提供更好的示例来处理。谢谢

我正在尝试使用 SAT Solver 解决扫雷问题。

到目前为止，我了解了游戏的一般逻辑、SAT Solver 的工作原理以及如何实现它。

但是，我不知道如何将我的布尔公式转换为 CNF，以便使用 SAT Solver 解决它。

假设我有以下 5x5 板：

2 XXXX XXXXXX
XXXXX
XXXXXX
XXXXXX

在单元格 1,1 中有值 2，这意味着周围的相邻单元格有 2 个地雷。整个单元格 1,1 有 3 个邻居（单元格 1,2；单元格 2,1；单元格 2,2）。我将调用相邻单元格：1,2 和 3。

这意味着我有以下布尔可能性：

如果(a or b) and (c or not d)是一个 CNF，那么 SAT Solver 的语法是：{{1,2},{3,-4}} 其中变量是整数，布尔假值是负整数，真值是正整数。

但是，我不知道如何将扫雷字段的布尔可能性转换为 CNF。

我对有 3 个邻居和 2 个地雷的单元格 1,1 的猜测：

所以我的 SAT Solver 公式根据语法将是： {{1,2,-3},{1,-2,3},{-1,2,3}}

有人可以确认或更正我的 SAT Solver 公式吗？

谢谢你。

编辑：

经过一番讨论，我想出了以下伪代码想法/方法：

• 任何形式的任何评论都将受到高度赞赏和帮助。

• 此外，一旦我检查并遍历每个单元格，这种方法会解决游戏吗？

谢谢你。