谈论CSP/SAT时什么是条款？

Question

这里有一个问题：

考虑了运动联盟调度问题下面的规则和定义：

• N（偶数）队，每两队赛季中打对方一次。
• 本季持续（N-1）周。
• 每个球队在本赛季的每周都会打一场比赛。
• 每周有N/2个周期或时段;每个插槽都预定一场比赛。

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

• 为了模拟两个不同的团队在给定的插槽中彼此对战，将每个插槽划分为两个子插槽。每周，我们有N个子时隙。采用这样的惯例，即两个连续的子球队 - 一个奇数子插槽和一个偶数子插槽 - 实际上是相互作用的。
• 可变Xijk分配真当且仅当球队我扮演的子槽法官在周K
• 可变Yijk指定真当且仅当球队我扮演球队法官在周K

有一个问题是： 给这个条款这表明恰好有一个团队在每个子插槽中播放。有多少条款？

我的问题： 这里的“从句”究竟是什么意思？我发布了这个问题，希望有人能告诉我问题想问什么，我不是在寻找一个直接的解决方案。

如果有人能帮忙，谢谢。

Answer 1

在CNF SAT的术语，“条款”是文字的有限析取，其中，文字是一个变量或它的否定

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

大多数现代布尔SAT解决方案接受CNF公式作为它们的输入。

Answer 2

您正在寻找SAT的介绍。 Don Knuth在今年早些时候在JKU做了一次演讲，这是对该主题的一个很好的介绍。在讲座中，他还给出了TAOCP中SAT章节预览版的链接。查找讲座这里的记录：

• 第1部分：http://www.youtube.com/watch?v=8DVu2-CC--8
• 第2部分：http://www.youtube.com/watch?v=ve-qyxlWOJQ
• 3部分：http://www.youtube.com/watch?v=5MiqBwieRxI

讲座（和书章）覆盖的基本术语SAT解决方案，如何使用CNF子句编码各种问题以及SAT解算器如何工作。