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

Question

问题是:

考虑体育联赛安排问题的以下规则和定义:

• N(偶数)支球队，每两支球队在赛季中恰好交手一次。
• 这个季节持续 (N-1) 周。
• 每支球队在赛季的每个星期都打一场比赛。
• 每周有 N/2 个时段或时段；每个时段都安排了一场比赛。

(a)(25 分)将体育联盟调度问题编码为 bool 可满足性问题。提示:

• 为了模拟两个不同的球队在给定时段内相互比赛，将每个时段分成两个子时段。对于每周，我们有 N 个子槽。采用这样的惯例，即两支参加连续子赛的队伍——一个奇数子赛后面跟着一个偶数子赛——实际上是在互相比赛。
• 变量 Xijk 被分配为真当且仅当第 i 队在第 k 周的子时段 j 中比赛
• 变量 Yijk 被分配为真当且仅当第 i 队在第 k 周对阵第 j 队

有一个问题:给出说明在每个子槽中恰好有一支球队比赛的条款。有多少个子句？

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

如果有人能提供帮助，谢谢。

Answer 1

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

阅读Clause on Wikipedia以获得更详细的描述。

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