问题标签 [satisfiability]

我是 SMT 求解的新手，我正在写信询问一些建议和指示，以了解difficult constraintSMT 求解器真正需要解决的问题，例如 Z3。

我试图调整位向量的长度，例如通过以下方式：

虽然直觉上这可能会导致相当大的搜索空间，但事实证明它Z3仍然做得很好并且可以迅速解决它。

我知道一些加密哈希函数或数学公式（例如，Collat​​z 猜想）可能会使约束求解变得非常困难。但这似乎很极端。另一方面，例如假设我有以下约束：

如何让约束求解器更难求解？有什么通用的方法吗？我的印象是，不知何故，约束变成了“非线性”，那就很难了。但我仍然不清楚它是如何工作的。

==================================

感谢您提供所有友好的注释和有见地的帖子。我非常感激！

因此，根据@usr 的建议，这里有一些试探性的测试：

（从 Math StackExchange 复制并进行了一些修改，如果这不是正确的地方，请告诉我）

一些背景：我正在考虑使用 SAT 求解器来证明素数的可行性，尤其是梅森素数，通过证明不存在布尔数组 d[1],d[2],...,d[b']可以表示素数的一个除数（即UNSAT）。

给定一个布尔列表 d[1],d[2],...,d[b]，其中 d 是一个以 10 为底的正整数 D 的以 2 为底的表示形式，是否存在一个计算结果为 True 的布尔谓词当且仅当 2^b−1≡0(mod D)？

（假设1<D<N，因此，b′<b。还假设 b 是素数。）

任何帮助是极大的赞赏。

我有一个学校项目，我必须使用 SAT Solver 找到游戏“Lights Out”（https://en.wikipedia.org/wiki/Lights_Out_(game)）的解决方案，但我在尝试设置连接词时遇到了麻烦游戏的正常形式。

游戏由 5 x 5 的灯光网格组成。按下任何一个灯都会切换它和四个相邻的灯。谜题的目标是关掉所有的灯。

到目前为止我是如何尝试的：

对于 3x3 网格（开始），我设置了 9 个术语（每个按钮），因此：

C11 : 位置 1,1 的按钮变亮 C12 : 位置 1,2 的按钮变亮 C13 : 位置 1,3 的按钮变亮。[...]

由于 1,1 处的按钮熄灭 1,2 和 2,1 位置处的按钮

我做了 C11 => C12 和 C21 1,2 处的按钮熄灭了位置 1,1 和 1,3 和 2,2 我做了 C12 => C11 和 C13 和 C22

并继续另一个：

然后我只是将这些转换为 CNF 以获得 sat 求解器所需的子句，但似乎我做错了..

谁能帮我把这个游戏写成 CNF 形式？

非常感谢 ！

如果您需要更好地理解它，这里是游戏：

https://www.geogebra.org/m/JexnDJpt#material/KArehWn8

我有 7 个杯子，里面有一些水。我需要对这些杯子进行编程以获得不同量的水。完成此操作后，我需要测量水量最多的杯子，然后取出一些量（比如 2 个单位的水）。

c实现：

这将给出一个答案c7 = 3.8

我试图在 z3 中实现这一点，并将值分配给 c1....c7

当我得到模型值时，它应该将 c7_1 设为 3.8

是否可以在 z3 中定义它？当我在 if 条件（在 ite 中）中使用不同条件的 and 时，它给了我一个错误。不能这样定义吗？有什么办法吗？

提前致谢

[问题描述][1]

我正在尝试使用 Z3 工具，很容易得到他的第一部分但是对于第二部分来说有点困难。

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

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

我正在使用 Z3 尝试一些基本的 FOL 公式可满足性问题。我无法理解为什么下面的代码片段会返回 Unsat。请帮忙。

如果可能的话，如果有人尝试使用带有量词的 FOL 给出“Sat”并且通过一些小的微小更改给出“Unsat”作为输出的示例，将非常有帮助

除了rise4fun教程页面上提供的之外，是否有一些简单的FOL公式代码片段可供学习。

我正在尝试制作 z3（我正在使用 z3py）来检查公式是否可以满足，如果可以满足则简化它。

我最初使用的是 Z3 的ctx-solver-simplify. 然而，由于我反复打很多电话，使用这种策略结果非常昂贵。因此，我尝试使用ctx-simplify仅执行局部简化的 Z3，但无论是否可满足，它仍应返回。

但是，我遇到了一些情况，它产生了简化，但不能令人满意。例如考虑以下内容：

使用ctx-solver-simplifyreturn unsatisifiable whilectx-simplify返回一个目标列表（如下所示），因此是可满足的（这显然是不正确的）。

谁能向我解释为什么会发生这种情况以及我是否正确使用了这些策略？谢谢！

根据维基百科，最大可满足性问题 (MAX-SAT) 是确定给定布尔公式的最大子句数的问题，该问题可以通过将真值分配给公式。它是布尔可满足性问题的推广，它询问是否存在使所有子句为真的真值赋值。

我不明白关于 MAX-SAT 如何是 SAT 的概括的第二句话。根据维基百科，SAT 询问给定布尔公式的变量是否可以一致地被值 TRUE 或 FALSE 替换，从而使公式计算为 TRUE。

我之所以问这个问题是因为论文“可满足性和最大可满足性问题的半定优化方法”，我想尝试半定优化技术来解决我手头的一些 SAT 问题。

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

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

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

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

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

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

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

这会大大加快速度吗？