问题标签 [sat]

这是一个非常简单的cnf实例，如(x1 or x2 or x3)&(x1 or x2)&(x2 or x3)，公式绝对可以满足，解x1 = x2 = x3 = 1，就够了。那么，我的问题是求解器如何使用 DPLL 或其他程序生成分配？谢谢。

这是我的第一个问题的连续性（Flow Shop to Boolean satisfiability [Polynomial-time reduction]）。

因为出了点问题，我没有成功知道到底在哪里。再次向 StackOverFlow 高手求助 :)

总结一下我现在所拥有的：

• 我有看起来像这样的输入文件：

谁代表：3 个工作，2 个车间（机器），以及每个车间（机器）上每个工作的持续时间。我想为这些问题找到最佳的 C_max 值。

因此，例如，它应该在输出中给出这个结果（对于paint.exe xD 感到抱歉）：

因此，为了阅读这些文件，我创建了 2 个结构：资源和问题，它们看起来像这样：

读数没问题，我的结构内的输入文件中有所有信息。

我想将这个最优问题（找到最佳解决方案）转换为决策问题（这是一个可能的解决方案吗？）为此，我的目标是将 JobShop/FlowShop 问题转换为 SAT 问题。

• 我的目标如下：我将 C_max 的值设置为固定值，我创建了一个 SAT 问题，我将减小 C_max 直到 SAT 求解器说问题没有解决方案。具有解决方案的最后一个值将是最佳值。

感谢@Jens Schauder，我有了一个解决方案的开始。我的布尔变量是这样的：s_1_2_3 with the meaning resource one gets used at machine 2 starting from time 3.

因此，如果我有 J 个工作、M 个商店并且我将 C_max 设置为 C 值，那么我肯定会有：J * M * C布尔变量。

问题：现在我的SAT问题是错误的。给出的解决方案不好。

以下是我现在的限制：（V 表示“或”，另一个：“和”）

这意味着我的工作只能在 1 家商店工作一段时间 k

这意味着商店 j 在时间 k 内只能处理一项工作。

这意味着如果作业的持续时间超过 1，则它必须是连续的。因此，如果一个变量为真，则在任务持续时间结束之前的另一个变量也必须为真。

我不确定我对问题的表述是否正确，或者/或者我是否忘记了约束。

现在，我还介意 Job Shop（Flow Shop 基本上是相同的，每个商店的工作必须以相同的顺序排列）

抱歉这个非常大的问题，但是对于这种问题，最好有所有的细节来知道它是关于什么的。

编辑

我将添加上面3个约束的源代码，可能里面有问题，我没有看到什么......

约束 n°1：

约束 n°2：

约束 n°3：

现在我正在写关于解决 SAT 的文章，但我被困在了一个点上。我希望你能帮助我。

我想描述一些解决 SAT 问题的方法。现在我有三种不同的方法：

1. 蛮力
2. 随机（天真）
3. DPLL（具有不同的启发式）
4. ? 失踪 ？
5. ...

我的问题是唯一有效的算法是 DPLL（以及其他一些与 DPLL 略有不同的算法）。因此我没有什么可以比较 DPLL 的。

我的问题：如果您能告诉我一些不基于 DPLL (DP) 的算法，我可以将其与之进行比较，那就太好了。

以下是我发现的一些，但无法确定它们是否是一个不错的选择，或者是否有更好的选择：

• 莫尼恩-斯佩肯迈尔
• Dantsin、Goerdt、Hirsch 和 Schöning
• Paturi-Pudlák-Zane-算法
• 霍夫迈斯特、舍宁、舒勒和渡边

谢谢你的帮助。

我发现根据 SATLIB SAT 实例，许多可满足的问题实际上是不可满足的，因为它们都包含一个或多个对它们有确切反条款的子句。例如下面的SATLIB cnf 子句的下载链接，包含 20 个变量、91 个子句 - 1000 个实例，都可以满足

有第一个文件本身，其中第 7 和第 86 条彼此完全相反，因此这个等式永远不会不满足。我已经在这里发布了一个关于此的问题，但到目前为止没有得到任何答复P = NP 上的旧问题 非常欢迎任何评论，因为我真的很想知道基准问题是否仍然用于比赛，就好像它们一样那么那些比赛真的没用。所以，我的问题是：我在确定这些错误并将它们暴露给公众并征求意见方面是否正确？这些发现还有用吗？我已经发送了几封电子邮件，要求基准问题网站的管理员回复，但 2 个月后仍然没有回复让我感觉很糟糕。

我正在尝试解决包含数千个变量的公式。这些公式的主要部分是线性的，从我的角度来看，z3 正在以令人难以置信的速度咀嚼它们。然而，碰巧很少有约束会引入一些非线性。然后，计算时间从几分钟增长到经过几天的计算后无法获得解决方案。

我认为尝试使用位向量会很有趣，但只是因为那些非线性约束会在此过程中失去一些精度，但这对于我要解决的问题来说不是问题。所以或多或少，我想通过在需要时切换到数字的位表示来使用小的 SAT 问题。我在另一篇文章中看到 int2bv 和 bv2int 被视为未解释，因此似乎无法使用这些函数。但是，我仍然不确定为什么它们没有被解释。是否存在任何理论问题或者是出于性能原因？

我还看到 z3 的最后一个稳定版本可以处理浮点（这里）。然而，从 FP 到 Reals 似乎引入了非线性。因此，仅将浮点用于非线性约束并用实数和整数求解其余部分似乎也是不可能的。我还没有尝试过，但我假设对所有变量使用浮点数不会针对我遇到的问题进行扩展。我想出了非常幼稚的函数，相当于 int2bv 和 bv2int。显然，即使对于非线性的小例子，它也非常慢。这是在 SMT2 中为正整数工作的 8 位向量的实现。

关于解决此问题的最佳方法的任何想法，或者 z3 中是否有任何我错过的东西可以让我的生活更轻松？

我正在寻找一个程序/一个库/一个想法来确定给定交换结构的同时路由和所需连接的列表。

路线必须不相交且同时进行。这是一个电路交换系统，其中实际的电信号将通过继电器传输。

在这张图片中，1-4、5-2 和 4-5 被路由通过，但多端连接（例如 1-1、2、3）也是可能的。

给出了结构的拓扑结构，大约有 200 个节点，但它们不是简单的交叉开关配置。

此外，还有一些额外的限制，因为某些开关只能同时打开或关闭。

最后，软约束是优先选择通过最少开关量的路由，但如果多个输入连接到一个输出，则线路应尽可能靠近输出合并。（这在交叉开关图片中不起作用，但假设输入 4（绿色）和 5（绿色）都应该连接到输出 3（蓝色）。4 和 5 可以在输入附近合并，然后一起路由输出 3，但最好将它们独立路由并尽可能接近 3 合并。

好于

我怀疑这对于约束求解器来说是一个非常简单的问题，但我不知道如何开始（哪个求解器？/如何将问题描述转换为模型？）。

如何根据此处的表定义一个执行值替换的函数？

我整天都在想它，但是为了有效，我仍然被这个问题困住了。欢迎任何建议/答案。谢谢！

具有 k 个一元子句且只有两个子句的 SAT 实例的复杂性是多少？

我想找一篇有这个结果的论文。我找到了一篇问题有点不同的论文。所有变量最多出现两次...

我有兴趣将部分加权最大 SAT 转换为 SAT。我被建议通过 CIRCUIT SAT。

部分加权最大 SAT 由一组硬条款和一组加权软条款组成。我们寻求一个满足所有硬条款并从软条款中获得至少 k 权重的分配。

我如何将其编码为布尔组合电路？

我可以看到如何轻松地对硬子句进行编码。但是我将如何对软子句进行编码，并将权重与它们相关联，并确保通过令人满意的分配获得至少 k 的权重？

谢谢

我的 Java 程序从其数据生成一个大型 CNF 实例。该实例主要包含（在大多数情况下>95%）排他的 2 子句：(!av !b)。目前我使用 Sat4j 的默认求解器。当我启用程序中的所有条件时，求解器将无限期运行。我尝试过一些经验来优化启发式和配置，但没有成功。解决此类情况的适当启发式集是什么？

（一个例子。）