You are organizing a New Year's Eve party. There will be N tables in the room, with M chairs around each table. You need to select a table for each of the guests, who are assigned numbers from 1 to MN, so that two conditions are satisfied. First, some guests like each other and want to sit together; accordingly, you are given a set A of two-element subsets of {1,...,MN}, and, for every {i,j} in A, guests i and j should be assigned the same table. Second, some guests dislike each other and want to sit at different tables; accordingly, you are given a set B of two-element subsets of {1,...,MN}, and, for every {i,j} in B, guests i and j should be assigned different tables. Your program should find such a seating arrangement or determine that it is impossible.
Here is a formalization in the language of ccalc (Version 1.9): new_years.b .
This formalization is absolutely tight in the sense of "Tight logic programs," by E. Erdem and V. Lifschitz (in TPLP, Vol. 3, pp. 499-518, 2003.)
Some other formalizations can be found at http://www.cs.utexas.edu/users/vl/tag/seating_solutions; a discussion on these formalizations can be found at http://www.cs.utexas.edu/users/vl/tag/seating_discussion.