问题标签 [sat]

我有一个 .cnf 文件，其中包含作为连接范式的数字。

我需要读取它们并将它们存储在数据结构（矩阵或列表）中，以便能够将它们用作索引。（我需要这个来解决 3-SAT 问题。）

如何在 Java 中读取和存储它们？

在一些期刊上，我读到 WSAT（步行 SAT）算法在解决 SAT 问题方面比模拟退火算法具有更好的性能。

所以我的问题是，有人可以解释为什么我们得到这个结果吗？可能是因为 SA 更像是一种通用算法？

编辑： 这可能是我读到的最相关的文件。

我正在使用通过 python 实现的 Z3 SMT 求解器。我有源代码，我希望有一些任何迹象表明该进程正在运行。是否可以使用一些详细的命令或任何东西来了解进程当前正在做什么？我知道它背后的算法，但我想可视化，即使使用 printf，代码中发生了什么。

谢谢！

在我工作的公司，我们可以使用多个 SAT Solver。我们想分析每个 SAT 求解器如何影响 Z3 SMT 求解器的性能。

是否可以从 Z3 调用外部 SAT 求解器？如果不是，应该在哪里修改 Z3 以调用外部求解器？

我刚刚开始使用 Sat4j 库。你能指导我如何计算解析和简化给定 CNF 输入所需的时间吗？

我用过

我希望计算读者解析和 isSatisfiable 所花费的时间。如果可能，请指导我在图像中查找每个处理过的 cnf 文件 的信息 我希望使用 sat4j lib 收集的详细信息的屏幕截图 提前感谢您的时间。

我知道这已被问过几次，但我需要一种快速的方法来处理不同大小的文件（小文件和大文件）。

我需要在 sat(txt) 文件中编辑比例因子。这是第三行的第一个数字：

700 104 1 0 16 Autodesk AutoCAD 19 ASM 221.0.0.1871 NT 24 星期二

2016 年 8 月 16 日 09:02:14

1000 9.9999999999999995e-007 1e-010

我正在尝试使用 minisat 调用程序时尝试一些随机参数system()。我以前从来没有做过这样的事情，不得不承认我很迷茫。

例如我可以这样做：

如何将其随机化为-lubyor-no-luby并将1.5值随机化-rinc？

为了解决 SAT 问题，我决定使用 Microsoft 的 Z3-solver 和 Python 3。目的是采用长模型（最多 500,000 个特征）并找到所有可能的解决方案。为了找到它们，我想将第一个解 S1 添加到初始方程并排除 S1 它等等。我将使用一个while循环来做到这一点。解决 SAT 问题对我来说很重要，因为我想分析特征模型。

但是我在将某物添加到初始方程时遇到了问题。我将分享一个最小的例子：

之后的第一行编码# Successfull...会引发z3types.Z3Exception: model is not available错误。所以我尝试将上面的行简单地添加false到模型中。这工作得很好。

我被困在这里。我相信这个错误很容易解决，但我没有看到解决方案。你们中的一个吗？谢谢！

运行某些实例时，可能需要一段时间，我想在我的台式电脑之间切换，以免炸毁它们。

因此，具有暂停和恢复长时间运行的求解器的功能会很有帮助。

使用 z3 CC_NUM_THREADS=3 配置并行 Z3 时出现问题

我正在尝试为我的 smt2 文件运行带有 CC_NUM_THREADS=3 的 z3 并行版本，弹出以下错误。