What is a clause when talking about CSP/SAT?

Question

Here is the question:

Consider the following rules and definitions for a sports league scheduling problem:

• N (even) teams, and every two teams play each other exactly once during season.
• The season lasts (N-1) weeks.
• Every team plays one game in each week of the season.
• There are N/2 periods or slots per week; every slot is scheduled for one game.

(a) (25 pts.) Encode the Sports League Scheduling problem as a Boolean satisfiability problem. Hints:

• In order to model that two different teams play each other in a given slot, divide each slot in two subslots. For each week, we have N subslots. Adopt the convention that two teams that play consecutive sublots — an odd numbered subslot followed by an even subslot — in fact play each other.
• Variable Xijk is assigned True iff team i plays in subslot j in week k
• Variable Yijk is assigned True iff team i plays team j in week k

There is one question: Give the clauses that state that exactly one team plays in each subslot. How many clauses are there?

My question: what does "clauses" here actually mean? I post this question in the hope that somebody could tell me what the question is trying to ask, I am not looking for a direct solution.

Thanks if anybody could help.

Answer 1

You are looking for an introduction to SAT. Don Knuth gave a lecture at JKU earlier this year, that is a nice introduction to the topic. In the lecture he also gives away the link to the preview version of the SAT chapter in TAOCP. Find the recording of the lecture here:

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

The lecture (and the book chapter) cover the basic terminology of SAT solving, how to encode a wide range of problems using CNF clauses and how SAT solvers work.

Answer 2

In terms of CNF SAT, "clause" is a finite disjunction of literals, in which a literal is a variable or its negation

Read Clause on Wikipedia for more detailed description.

Most of the modern Boolean SAT solvers accept CNF formula as their input.