Note: this problem has been taken from
Puzzle Baron’s Logic Puzzles.
Solve the following exercise by means of a reduction to
SAT:
 A group of train conductors has just received their individual
assignments for next week’s schedule. Using only the clues provided,
match each conductor to his train, scheduled day, and departure/arrival
stations:
 The train conductors are Bryan, Eugene, Greg, Herman, Luke, Nathan, and Thomas.
 The scheduled days are June 10, 11, 12, 13, 14, 15, and 16.
 The departure stations are Buttonwillow, Coulterville, Daly City, Farley, Jackman, Kent, and Manson.
 The arrival stations are Paradise, Quimby, Ripley, Urbandale, Vinalhaven, Yreka, and Zwingle.
 Each train conductor has a different scheduled day, a different departure station and a different arrival station.
 The conductor working on June 15 is either the person arriving at Paradise or the conductor departing from Daly City (but not both).
 Of the person departing from Coulterville and Thomas, that are two distinct persons, one will arrive at Paradise and the other is scheduled to leave on June 14.
 Nathan is either the person working on June 15 or the conductor arriving at Urbandale (but not both).
 The person arriving at Quimby will leave 2 days after the conductor arriving at Zwingle.
 Neither the conductor working on June 14 nor the person arriving at Vinalhaven is Nathan.
 The conductor departing from Manson will leave sometime after the person departing from Kent.
 The person departing from Jackman will leave 3 days after the person departing from Farley.
 Greg won’t arrive at Yreka.
 The conductor arriving at Urbandale will leave 4 days after the conductor departing from Daly City.
 Luke will leave 1 day before the conductor arriving at Vinalhaven.
 Eugene is either the person arriving at Paradise or the person departing from Daly City (but not both).
 Of the conductor departing from Buttonwillow and the conductor arriving at Ripley, that are two distinct conductors, one is scheduled to leave on June 11 and the other is scheduled to leave on June 14.
 Of the conductor arriving at Yreka and the person working on June 10, that are two distinct people, one will depart from Farley and the other is Luke.
 The person departing from Kent will leave 2 days before Bryan.
The input of the exercise and the output with the solution (when the input is
solvable) are as follows:
 This problem has no parameters, and therefore, there is no real input.
Nevertheless, in order to ease the reduction, some input variables are
defined with the identifiers for the days, conductors, and departure/arrival
stations:
INPUT VARIABLES FOR ... 
DAYS CONDUCTORS DEPARTURES ARRIVALS  ID VALUE
+
June10 Bryan Buttonwillow Paradise  0
June11 Eugene Coulterville Quimby  1
June12 Greg DalyCity Ripley  2
June13 Herman Farley Urbandale  3
June14 Luke Jackman Vinalhaven  4
June15 Nathan Kent Yreka  5
June16 Thomas Manson Zwingle  6
Note that, for convenience, all the identifiers are numbers in $\{0,\ldots,6\}$,
and that conductor and station names have been sorted alphabetically.

schedules: array [7] of struct {
conductor: int
departure: int
arrival: int
}
The output consists of an array with $7$ elements, one for each day:
at index $i$ (starting at $0$) there is the data for June $10+i$.
The data for a day consists of the conductor, the departure station, and
the arrival station identifiers. Thus, for instance, if the element of
schedules at index $3$ is a struct containing the identifier $5$
as conductor, the departure station $3$, and the arrival station $2$,
it means that in June $13$, Nathan is assigned to go from Farley to Ripley.
Note: this problem can be solved in asymptotic constant time without reducing to SAT.