谈论 CSP/SAT 时的子句是什么？答案

【问题标题】：What is a clause when talking about CSP/SAT?谈论 CSP/SAT 时的子句是什么？
【发布时间】：2013-10-21 23:46:40
【问题描述】：

问题来了：

考虑以下有关体育联赛日程安排问题的规则和定义：

(a) (25 分) 将体育联赛调度问题编码为布尔可满足性问题。提示：

为了模拟两个不同的球队在一个给定的位置上互相比赛，将每个位置划分为两个子位置。对于每周，我们有 N 个子插槽。采用这样的惯例，即两支球队在连续子时段（奇数子时段后接偶数子时段）实际上是互相比赛。
变量 Xijk 被赋值为真 iff 团队 i 在第 k 周的子槽 j 中比赛
如果团队 i 在第 k 周与团队 j 比赛，则变量 Yijk 被分配为真

有一个问题：给出说明每个子槽中只有一支球队参加比赛的条款。有多少条子句？

我的问题：这里的“条款”实际上是什么意思？我发布这个问题是希望有人能告诉我这个问题想问什么，我不是在寻找直接的解决方案。

如果有人可以提供帮助，谢谢。

【问题讨论】：

【解决方案1】：

在 CNF SAT 中，“从句”是文字的有限析取，其中文字是变量或其否定

阅读Clause on Wikipedia了解更详细的说明。

大多数现代布尔 SAT 求解器都接受 CNF 公式作为输入。

【讨论】：

【解决方案2】：

您正在寻找 SAT 的介绍。 Don Knuth 今年早些时候在 JKU 做了一次演讲，很好地介绍了这个话题。在讲座中，他还提供了指向 TAOCP 中 SAT 章节预览版的链接。在这里找到讲座的录音：

讲座（和书籍章节）涵盖了 SAT 求解的基本术语、如何使用 CNF 子句对各种问题进行编码以及 SAT 求解器的工作原理。

【讨论】：