这是个问题：
对于体育联盟调度问题，请考虑以下规则和定义：
- N（偶数）球队，每两支球队在赛季中正好比赛一次。
- 季节持续（N-1）周。
- 每支球队在赛季的每一周都打一场比赛。
- 每周有 N/2 个时段或老虎机;每个老虎机都安排了一场比赛。
（一） （25分）将体育联盟调度问题编码为布尔满足性问题。提示：
- 为了模拟两个不同的团队在给定插槽中相互比赛，请将每个插槽划分为两个子插槽。每周，我们都有 N 个子槽。采用这样的惯例，即两个连续子插槽的团队 - 一个奇数子插槽，然后是一个偶数子插槽 - 实际上相互比赛。
- 变量 Xijk 被分配 True iff 球队 i 在第 k 周的子插槽 j 中比赛
- 变量 Yijk 被分配 True iff 团队 i 在第 k 周玩团队 j
有一个问题：给出条款，说明每个子插槽中只有一个球队参加比赛。有多少个条款？
我的问题：这里的"条款"到底是什么意思？我发布这个问题是希望有人能告诉我这个问题想问什么，我不是在寻求直接的解决方案。
如果有人可以帮忙，谢谢。
就 CNF SAT 而言，"子句"是文字的有限析取，其中文字是变量或其否定
阅读维基百科上的条款以获取更详细的描述。
大多数现代布尔 SAT 求解器都接受 CNF 公式作为输入。
您正在寻找对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 求解器的工作原理。