问题标签 [sat]

我有一个有趣的 3SAT 算法，我想实现它，但无法编写相同的代码，因此无法查看它是否真的有效。该算法在此处的 Microsoft Word 文件中定义： DropBox Link for 3SAT algorithm 我不知道该算法是否真的有效，以及它的复杂性如何。不过，我真的很想知道它的复杂性。请帮我解决这个问题，就好像它是在多项式时间内那样我会证明 P = NP！

我可以将具有 SMT-LIBv2 格式并包含 set-logic QF_AUFBV 的输入文件转换为 CNF 吗？如果是这样，我该如何使用 Z3 命令行统一性来做到这一点？

更新：我还需要将变量从 SMT-LIBv2 实例映射到 CNF DIMACS 文件作为注释。用Z3可以吗？

我刚开始使用 Z3 (v4.4.0)，我想尝试其中一个教程示例：

如前所述，第二个示例因“未知”而失败，并且通过增加详细级别（至 3）我想我明白为什么：简化过程存在问题，然后策略失败。为了更好地了解问题（以及更短的输出），我决定删除代码的第一部分以仅测试失败的部分：

但神奇的是，现在我“坐”了。我不确定 Z3 在涉及非线性算术时如何选择它的策略，但问题可能出在 Z3 为第一个公式选择一种对第二个公式无用的策略吗？

提前致谢

当我在 Mac 上编译葡萄糖 SAT 求解器时，在编译葡萄糖 3.0 时出现以下编译时错误。如何避免这些错误？

与固定长度位数组相比，为什么将 16 位有符号整数变量表示为区间（-32768..32767）时性能会显着下降？

检查预处理的 NuSMV/NuXMV 模型可以观察到区间类型转换为枚举。

然而，BDD 的统计数据并未显示任何相关信息。

我想到了一种通过以下方法解决 3SAT 问题的算法：

1）取cnf方程中至少有一个共同变量的所有子句。找到所有这些组合并将它们放入名为“Intersection”的列表中。列表“Intersection”现在包含相交子句组。

2）接下来，我们将特定组“Intersection”中的所有子句转换为 DNF。由于至少有一个共同变量，我认为它不会在指数时间内出现。

3）接下来，我们将所有获得的 DNF 转换为单个 DNF，因为它们在原始方程中都用 AND 门分隔。

4) 如果得到的 DNF 中有一个子句，则方程是可满足的，否则方程是不可满足的。这是因为不相交的子句（没有任何共同变量的子句）不会影响整个方程，最后如果我们与获得的 DNF 进行“与”，它只会将变量相乘并添加到现有的条款（如果有的话）。

我的问题是：

该算法的运行时间是多少，这是否证明了与 P=NP 相关的任何事情，因为我认为该算法非常有效。我之前的算法被其他人失望了，所以这次请花点时间分析算法，因为这是我的努力。

在谈论 SAT 求解器时，例如 minisat，“0-depth”和“CNF assignments”的值是什么意思？这些值通常是各种 SAT 求解器信息输出的一部分。

我正在尝试使用SAT solver. 公式（DIMACS格式）有4,697,898,048 = 2^32 + 402,930,752子句，我能找到的所有 SAT 求解器都遇到了问题：

• (P)lingeling报告“子句太多”（即子句比标题行指定的多，但事实并非如此）
• CryptoMiniSat4 & picosat声称读取标题行时说 402,930,752 个子句太少了 2^32
• Glucose似乎解析了 98,916,961 个子句，然后报告已使用简化将公式求解为 UNSAT，但这不太可能是正确的（公式的初始部分很可能是 SAT）。

有人知道可以处理这么大文件的 SAT 求解器吗？或者是否有类似编译器开关的东西可以回避这种行为？我相信所有求解器都是为64bit linux编译的。（在处理这么大的数字时，我有点菜鸟，抱歉。）

我需要为 ACIS 文件操作制作一个脚本，例如：

我有 1 个从带有 3D 模型的 CAD 软件导出的 SAT 文件，我想用某种语言（php、python 等。甚至 .BAT，如果可以的话）创建一个脚本，打开 SAT 文件删除里面的所有组件我的 3D 模型。我只想要3D模型的外部。

有什么方法可以做到这一点？因为我查看 SAT 文件，它是大量的文本行，也许使用 RFC 和一些棘手的工具我可以做到这一点..

有什么想法吗？

最好的问候，佩德罗·维埃拉

我有一个项目在我的脑海中，我很好奇以前是否做过类似的事情。假设有一组不同类型的约束并且这些约束不能一起满足。

C = {c1, c2, c3, ..., cn}

(c1 and c2 and c3 ... cn) : 不能满足

我的目标是将这个集合分成 k 个集合（可能 k 非常小），以使每组约束都可以单独满足。

基本的解决方案是使用贪婪的方法。将选择一个约束作为第一个约束并标记为第一组。然后，将选择第二个并检查它是否可以用第一个约束解决。如果它们是可解的，那么第二个约束也将在第一组中，否则，它将被标记为第二组。这个过程将以这种方式继续，直到集合中没有任何约束。这样做的另一种方法可能是将约束分为 2 组，并检查这些组是否可以单独解决。如果不是，继续递归除法。这两种方法都受到大小的影响，它们将约束集划分为非常小的集合。

我正在寻找一种将约束集划分为 k 集的有效方法，其中 k 接近最优值（最小 k 值）。这里有 2 个挑战，1）可扩展性问题和 2）事先不知道约束结构。