问题标签 [satisfiability]

我知道布尔可满足性是 NP-Complete 的，但它是布尔表达式的最小化/简化，我的意思是采用符号形式的给定表达式并以符号形式产生等效但简化的表达式，NP-Complete？我不确定从可满足性到最小化是否有减少，但我觉得可能有。有人有确切消息么？

如果我有一个像这样的公式：

（FA = 全部 / E = 存在）

skolemisation 的规则说：

1. 如果 E 在 FA 之外，则替换为常数或
2. 如果 E 在 FA 内部，则用新函数替换包含 FA 外部的所有变量作为参数。

那么在这种情况下我该怎么办？我可以只删除 Exists 量词还是用常数替换它？

谢谢！

只是一个好奇的问题。还记得在课堂小组作业中，教授会将人们分成一定数量的小组（n）吗？

我的一些教授会从每个学生那里拿出n一份想共事和n不想共事的人的名单，然后神奇地将n学生与他们喜欢并避免与之共事的人配对他们不喜欢的人。

对我来说，这个算法听起来很像一个背包问题，但我想我会问你解决这类问题的方法是什么。

编辑：找到一篇 ACM 文章，描述的内容与我的问题完全一样。阅读第二段的似曾相识。

我对 CSP 比较陌生，我试图根据变量之间施加的 ==、>、< 和 != 约束从它们各自的域中找到所有变量的值。我查看了 Choco 和 Jacop，但我找不到更多关于解决这类问题的信息。你能指出我可以找到这个例子的实现的地方吗？我已经使用 Prolog 解决了这个问题，但我想使用 OOP 来完成它。

谢谢你。

我有兴趣了解已知为多项式（或更实际地，O(N^2)）的布尔可满足性问题的特殊情况。这些案例还应该有有效的算法来实际生成所有令人满意的实例，其中高效我的意思是需要 O(N #SAT) 来生成所有实例的序列。第二个条件可能暗示第一个条件，但我不清楚。

简单的例子：1SAT :)

简单的例子：带有“链”子句的 2SAT，因此用子句连接变量的图是一条线。

有更多的地方吗？谢谢。

我有以下问题：

我有两个必须成为逻辑等价的命题公式。只有其中一个包含一个“变量”，因为该变量可以被任何命题公式替换。现在的问题是，我需要找到变量的实际替换，以便逻辑等价变为真。例子：

(a ^ ~b) 或 x = a

这里，x 表示变量。通过将 x 替换为 a ^ b 可以使这个逻辑等价成立，因此它变为：

(a ^ ~b) 或 (a ^ b) = a

所以这就是问题所在。我需要一种算法，该算法将“具有一个变量 x 的方程”作为输入，并给出变量 x 的输出值，以使方程成为逻辑等价。

永远只有一个变量。（实际上我可能会遇到多个变量的问题，但我想先解决简单的情况）。有问题的公式可以有任何形式（它们不在 CNF 或 DNF 中）。此外，公式实际上可以为 FALSE 或 TRUE，并且在某些情况下，没有解决方案（例如，对于“a 或 x = false”，没有解决方案）或多个解决方案（例如，对于“a and x = false”） “任何错误的命题都是有效的答案）。

我所拥有的只是一个画面推理器，它告诉我一个公式是否可以满足。所以我可以测试一个解决方案。但我的问题是给我一个解决方案。

SAT 是 NP-complete 的证明是一个建设性的证明，因此应该可以将其作为程序来实现。有人做过吗？

我正在寻找一个程序（编译器），它将程序（返回真或假）作为输入并输出 SAT 公式。

因此，例如，编译器可以将以下程序（以 pythonic 语法显示，但任何语言都可以）作为输入，并输出 SAT 公式。将 SAT 公式提供给 SAT 求解器将给出参数“证书”的解。在这种情况下，解将是 [False, True, True, True, False]，表示 {-3, -2, 5} 是一个解。

显然，输出的 SAT 公式会有其他辅助变量，因此编译器必须指出哪些变量对应于证书。

这样的编译器是否已经存在？它们中的任何一个都是开源的吗？

在对包含子句数据库的 SAT 实例进行预处理期间，需要为每个变量分配一个单词。散列函数为每个变量返回一个仅由 0 组成的 32 位字，除了 16 个最高有效位 (MSB) 中的一位和 16 个最低有效位 (LSB) 中的一位，这取决于设置为 1多变的。子句的签名是其所有变量的散列函数值的按位或。

如何实现这个哈希函数？

问题

我正在研究 SAT 优化问题的一个特殊子集。对于那些不熟悉 SAT 和相关主题的人，这里是相关的 Wikipedia 文章。

没有非，它是合取范式。这很容易解决。但是，我试图最小化真实分配的数量，以使整个陈述成为真实。我找不到解决这个问题的方法。

可能的解决方案

我想出了以下方法来解决它：

1. 转换为有向图并搜索最小生成树，仅跨越顶点的子集。有 Edmond 的算法，但它给出了完整图的 MST，而不是顶点的子集。
   • 也许有一个版本的 Edmond 算法可以解决顶点子集的问题？
   • 也许有一种方法可以从可以用其他算法解决的原始问题构建图形？
2. 使用 SAT 求解器、LIP 求解器或穷举搜索。我对这些解决方案不感兴趣，因为我正试图将这个问题用作讲座材料。

问题

你有什么想法/意见吗？你能想出其他可行的方法吗？

我正在尝试使用 Z3 SMT Solver 证明以下内容：((x*x) + x) = ((~x * ~x) + ~x). 这是正确的，因为 c 编程语言中的溢出语义。

现在我编写了以下 smt-lib 代码：

z3 的输出是：

现在我的问题是：为什么结果“不满意”？我的代码中的简化命令表明可以获得有效的分配，以便 myfun1 和 myfun2 具有相同的结果。

我的代码有问题还是z3中的错误？

请任何人都可以帮助我。谢谢