问题标签 [satisfiability]

假设有人找到了一种在 O(n^3) 时间内给定 CNF 布尔表达式创建图的方法，并且这个特殊图的任何生成树都将是 CNF 方程的解。

该场景似乎暗示某人已经找到了 SAT 问题的解决方案，并通过使用仅在 O(n^3) 时间内运行的小工具（减少）将 SAT 问题简化为生成树问题来解决 P=NP。

但是，如果他们的算法创建的图有 n！还是 2^n 个节点和边？

在这种情况下，虽然诸如 DFS 或 BFS 之类的生成树算法可以在节点/边的数量上以线性时间运行，但它不会在布尔表达式的输入数量上以多时间运行。所以这个人不会找到解决 SAT 问题的有效算法，因为运行完整的解决方案需要 n！评估的时间。

这个推理正确吗？

给定一个数组，输出数组中总和为 0 的连续元素。

例如：

对于输入 [2, 3, -3, 4, -4, 5, 6, -6, -5, 10]，

输出为 [3, -3, 4, -4, 5, 6, -6, -5]

我只是找不到最佳解决方案。

澄清1：对于输出子数组中的任何元素，子数组中应该有一个子集与元素相加为零。

例如：对于 -5，子集{[-2, -3], [-1, -4], [-5], ....} 之一应该出现在输出子数组中。

说明2：输出子数组应该是所有连续的元素。

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

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

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

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

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

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

我阅读了许多用于查找 2-SAT 问题的算法，即给定的表达式是否可满足，可以在多项式时间内求解。示例（算法）。
对于Krom 的过程（维基百科），我构建了一个图，从中我可以轻松地验证它在多项式时间内的可满足性。
现在，我想找到这个表达式的解决方案是令人满意的。
我是这样想的（验证它）：首先我取任何形成强连通分量的表达式文字，比如 x，并将值赋值为 0。然后根据算法，存在边（x！-> y）。因此 y 不能为 0。（因为 1 -> 0 为假）并且如果可能，类似地继续。
否则取 x=0，然后只能选择 y=1，然后类似地继续获取任何 1 个可满足的实例。

现在，是否有任何可行的解决方案可以在多项式时间内找到其中任何一个

• 给出表达式可满足的所有可能解。
• 或者这个表达式对于总 k 字面量 = 1 的输入是否可以满足。
• 或者有多少最小数量的文字具有值 1 才能满足表达式。

对于这类问题，我没有得到任何多项式算法。

我对 sat4j 求解器和研究布尔可满足问题是全新的；我被卡住了。我想制作一个程序来解决布尔公式中的整数变量，例如；

x1 < x2 + x3 用户输入该公式，我的程序满足该公式（返回真），如 x1 = 5 ，x2 = 3，x3 = 4。所以公式返回真，用户得到满足公式的整数值。是可以在 sat4j 中实现它，因为我使用 java 在 eclipse 中工作。

这是一个家庭作业问题。我只是在开始之前有一些问题。

我们的问题是：

“从 k 独立集减少到 2−SAT，如下所示。给定一个具有 n 个顶点的图 G 形成 n 个命题，每个顶点一个命题。如果顶点 i 属于独立集，则顶点 i 的每个命题 xi 都设置为真。现在为每条边 (u,v) 写一个子句，说 u 和 v 都不能属于独立集。”

我的问题是，我读到的所有内容都说 2-SAT 不是 NP 完全问题。那么我们怎样才能减少独立集问题呢？

我们知道DPLL算法是回溯+单元传播+纯文字规则。

我有一个例子。有一个例子可以解决以下 DPLL 的可满足性问题。如果将“0”分配给变量先于将“1”分配给变量，使用哪个Unit Clause (UC)或哪个Pure Literal (PL)来解决这个特定示例？

在此示例中，使用其中两个 ( ) 编写PL and UC。为什么选择其中两个？任何想法？

有没有办法在 Z3 中表达假设（我正在使用 Z3Py 库），这样引擎不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样？

例如，假设我有两个参数类型为 Real 的一元函数。我想告诉 Z3 引擎，对于所有输入值，f1(t) 等于 f2(t)。

在 Z3Py 中编码如下所示：
t = Real("t")
假设 1 = ForAll(t, f1(t) = f2(t))。

所呈现代码的问题是我的断言集非常大并且我使用量词（我试图证明实时系统的可满足性）。如果我将上述断言添加到其他断言集中，则检查过程不会终止。

我正在查看以前的试卷，并且遇到了这个让我感到困惑的问题。

问题：

将子句给出的 Not-All-Equal 2-SAT 问题转换{x1, x2}, {x2, x3}, {x3, x4}, {x4, x5}, {x5, x1}为等效的 2-SAT 问题。（提示：2-SAT 问题包含 10 个子句）。

根据我的理解，这是否只是在每个子句中找到每个文字的否定？例如，{x1, x2} = {-x1, -x2}, 并且这是为每个子句完成的？这个对吗？

标题说明了一切。我尝试将 -1 呈现为以下内容：(_ bv-1 32)，并且 z3 抱怨。

如何呈现约束，例如3x - 5y <= 10位向量？出于某种原因，我不想使用线性整数。