问题标签 [sat]

我看到很多关于这个问题的相互矛盾的信息。一些网站说它是 NP 完全的，而另一些网站则说它是共同 NP 完全的。我能找到的唯一真正一致的信息是这绝对是 NP 难的。它是哪一个？为什么？

也许有点超出本网站的范围，但我想这里有足够多的人会知道这一点，所以我试了一下。

假设我有一组 3-CNF 子句

每个变量范围超过{0,1}

S 有多少令人满意的作业？一般来说，对于 S 有多少令人满意的分配是 S 的大小是 k？

这是一个关于什么是 3-disjunctive 从句的令人满意的分配的问题，就像它是关于计数的问题一样。例如，当我只有 时，有 2 ³ = 8 个可能的分配：

但其中哪一项是令人满意的任务？

Minisat 是一个约束编程/满足工具，有一个版本的 Minisat 可以在浏览器中运行http://www.msoos.org/2013/09/minisat-in-your-browser/

如何用 Minisat 表达调度问题？是否有更高级别的语言可以编译为 Minisat 让我表达它？

我的意思是解决考试时间表等问题。http://docs.jboss.org/drools/release/6.1.0.Final/optaplanner-docs/html_single/#examination

一般问题

我已经多次注意到push-pop已经弹出的范围似乎会影响check-sat后续范围中的 a 所需的时间。

也就是说，假设一个程序具有多个（可能是任意嵌套的）push-pop 作用域，每个作用域都包含一个 check-sat 命令。此外，假设第二个 check-sat 需要 10 秒，而第一个只需要 0.1 秒。

注释完第一个 push-pop 范围后，第二个 check-sat 只需要 1s。这是为什么？

• AFAIK，如果使用推弹范围，Z3 会切换到增量求解器。他们为什么会这样表现有（概念上的）原因吗？

• 曾经有人告诉我，Z3 按重要性为符号分配属性，这会影响证明搜索（在证明搜索期间，符号的重要性也会发生变化）。这可能是原因吗？是否可以重置重要性（在范围之间）？

• 这可能是一个错误吗？我发现这篇文章Leonardo 提到了一个似乎相关的错误（不过，他的回答来自 2012 年）。

具体实例

不幸的是，我只有相当长的（自动生成的）SMTLib 文件来说明该行为，您可以在此 gist中找到其中一个文件。它使用量词和未解释的函数，但既不使用mbqi数组也不使用位向量。该示例由 148 个嵌套的 push-pop 作用域和 89 个 check-sat 组成，Z3 4.3.2 大约需要 8s 来处理它。最后一次检查（以 为前缀echo）耗时最长。

我随机评论了几个 push-pop 作用域（一次一个，永远不会是最后一个，确保你没有评论符号声明），并且在大多数情况下，整体运行时间下降到不到 1 秒。也就是说，最后一次检查坐的速度要快得多。

为了提供更多详细信息，我将运行 Z3 与所有范围（慢，8 秒）与运行 Z3 进行比较，其中标记的范围[XXX]已被注释（快速，0.3 秒）。结果可以在这个差异中看到（左慢，右快）。

diff 表明所有检查-sat 的行为都相同（我通过回显“unsat”来伪造评论过的一个），从中我得出结论，评论范围会影响证明搜索，但不会影响其最终结果。

我还试图从获得的统计数据的差异中找出一些意义，但我对如何正确解释统计数据知之甚少。以下是我能理解的一些统计数据：

• grobner（383 vs 36）和nonlinear-horner（342 vs 25），所以看起来较慢的运行执行更多与算术相关的操作。注释范围确实即将进行非线性算术（许多其他算法也是如此），但是注释范围中的特定证明应该是“微不足道的”，它本质上表明x != 0对于x已0 < x明确假设的一个。

• memory（40 vs 7），我解释为表明Z3在程序的慢版本中探索了更大的搜索空间

• quant-instantiations（43k vs 51k），这让我感到惊讶，因为明显更快的运行仍然触发了更多的量词实例化。

我想解决以下关于 3SAT 的问题。“TWICE-3SAT 输入：如何证明它是 NP-hard 并且有多个可满足的作业”

是否有任何算法具有良好的性能（除了天真）找到最接近公式的任意良好估值（我们知道）的新的、不同的公式估值？

铁

((p & q & x) | r) <-> (a & b & c & d & e) 正确估值 p,q,x = 1, r = 0, a..e = 1. fe a 的变化到 0 对我们不利——它强制改变 p,q,x = 0。“r”的变化对我们来说更好——我们不必从 r 改变任何东西。我们可以假设“最接近”意味着根据汉明度量最接近。

该算法对于我的程序探索从时间逻辑公式生成的状态空间非常有用（对于具有 > 15 个变量的所有解决方案，许多可能的估值，仅使用 BFS 算法进行部分搜索）的图太大。

我正在努力想出一个更好的解决方案来声明 CBMC（C 有界模型检查器）中的“恰好一次”属性。我的意思是一行中的一个元素位置应该具有值 1（或任何可以检查为布尔值 true 的正数），其余的必须全为零。

对于 M = 4

对于比这更大的 M，这是一个巨大的问题。可以说 M = 8 我必须做类似的事情：

检查一次的违规很容易，但说明它看起来很重要。我可能还有一个选择：将二维数组问题表述为一维位向量问题，然后进行一些智能异或。但我目前不确定。

有人对这个问题有更好的解决方案吗？

我有一些理论/实践问题，我现在不知道如何管理，这里是：

我创建了一个SAT 求解器，它能够在模型存在时找到模型，并在 C 中使用遗传学算法的CNF问题不是这种情况时证明矛盾。

SAT 问题基本上看起来像这样的问题： 我的目标是使用这个求解器在许多不同的 NP 完成问题中找到解决方案。基本上，我将不同的问题转换为 SAT，用我的求解器解决 SAT，然后将解决方案转换为原始问题可接受的解决方案。

我已经成功解决了 N*N 数独和 N-queens 问题，但这是我的新目标：将班级调度问题简化为 SAT，但我不知道如何将班级调度问题形式化以便轻松转换它在SAT之后。

显然，目标是在几个月内生成一张这样的时间表图片：

我发现这个源代码能够解决课程安排问题，但不幸的是没有减少 SAT：/

我还发现了一些关于总体规划的文章（例如http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf）。

但是本文中使用的规划域定义语言对我来说似乎过于笼统，无法代表一个类调度问题。：/

有人知道如何有效地形式化班级调度以将其简化为 SAT，然后将 SAT 解决方案（如果存在 ^^）转换为班级调度吗？

我基本上对任何建议持开放态度，我现在不知道如何表示，如何减少问题，如何将 SAT 解决方案转换为时间表......

后续问题：布尔可满足性的类调度 [多项式时间缩减] 第 2 部分

前几天我问了一个关于如何将大学排课问题转化为布尔可满足性问题的问题。

（类调度到布尔可满足性[多项式时间减少]）

我得到了@Amit 的回答，他非常优雅且易于编码。基本上，他的回答是这样的：他没有考虑课程，而是考虑了时间间隔。

因此，对于第 i 个课程，他只是指出了该课程的所有可能间隔。当每门课程至少有 1 个真实区间并且没有区间重叠时，我们得到了一个解。

当我们只考虑课程而不考虑其他内容时，这种方法非常有效。我通过对区间内的房间进行编码来概括它。

例如，而不是 [8-10] 说课程可以在上午 8 点到 10 点之间进行。

我用 [0.00801 - 0.01001] 表示课程可以在上午 8 点到 10 点之间在房间 1 进行。

我确定您目前正在徘徊“为什么要使用 double ？” 好吧，因为我的问题来了：

为了继续推广这种方法，我还在这个区间内编码了教师的 n°。

我用 [1.00801 - 1.01001] 表示课程可以在上午 8 点到 10 点之间在 1 号房间进行，由 n°1 老师教授。

这是我现在得到的：

像这样 [1.008XX - 1.010XX] 可以与 [2.008YY - 2.010YY] 同时发生，这是真的，如果老师 1 在上午 8 点到 10 点之间在房间 X 教学，那么老师 2 也可以在Y 上午 8 点到 10 点之间，当且仅当房间可用时。

问题是：使用这种方法，我不能保证 XX 和 YY 会不同并且 YY 将可用，因为 [1.008XX - 1.010XX] 不重叠 [2.008XX - 2.010XX]，所以现在，求解器考虑这可能。

而且我仍然不知道如何通过使用这种间隔方法来确保这一点......我需要一种编码 {Interval, room and teacher-id} 的方法，以便：

• 一个老师不能在同一个区间的两个地方。
• 同一房间不能有 2 位教师在同一时间间隔内。
• 当然，至少有 1 个区间为真。

提前感谢您的帮助，最好的问候！

后续问题： Class Scheduling to Boolean satisfiability [Polynomial-time reduction] Final Part

我与您联系是为了了解“如何将流水车间调度问题”转换为布尔可满足性。

我已经为 N*N Sudoku、N-queens 和 Class 调度问题做了这样的简化，但是我对如何将流水车间转换为 SAT 有一些问题。

SAT问题看起来像这样：

目标是：使用不同的布尔变量，找到每个变量的做作，以使“句子”为真。（如果找到解决方案是可能的）。

我用遗传算法创建了自己的求解器，能够找到解决方案并证明什么时候没有解决方案。现在，我尝试解决不同的 NP 问题，比如 Flow Shop。

流水车间调度问题是车间或集团车间的一类调度问题，其中流控制应为每个作业和在一组机器上或使用其他资源的处理启用适当的排序 1,2,...,m遵守给定的处理订单。

尤其是希望以最少的空闲时间和最少的等待时间来维持处理任务的连续流。

流水车间调度是作业车间调度的一种特殊情况，其中对所有作业执行的所有操作都有严格的顺序。

流水车间调度也可以应用于生产设施，就像计算设计一样。

（http://en.wikipedia.org/wiki/Flow_shop_scheduling）

结果是一系列工作将通过每个研讨会，图形结果将如下所示：

因此，为了表示流水车间实例，在输入中我有这样的文件：

这个文件意味着我有 2 个商店和 4 个工作，每台机器上每个工作的所有持续时间。

目标：找到最小化 C_max 的序列，如果您愿意，可以在最后一台机器上找到最后一个作业的结束日期。

我的 Flow-Shop 现在真的很简单，但我不知道如何将它们形式化以便创建一个 CNF 文件来执行我的 SAT 求解器。

如果你们中的一个人有一些想法：文章？一个想法的开始？

这个问题的下一部分：Flow/Job Shop to Boolean satisfiability [Polynomial-time reduction] part 2