## Exercise ‹13›:

Train schedules
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:
1. The train conductors are Bryan, Eugene, Greg, Herman, Luke, Nathan, and Thomas.
2. The scheduled days are June 10, 11, 12, 13, 14, 15, and 16.
3. The departure stations are Buttonwillow, Coulterville, Daly City, Farley, Jackman, Kent, and Manson.
4. The arrival stations are Paradise, Quimby, Ripley, Urbandale, Vinalhaven, Yreka, and Zwingle.
5. Each train conductor has a different scheduled day, a different departure station and a different arrival station.
6. The conductor working on June 15 is either the person arriving at Paradise or the conductor departing from Daly City (but not both).
7. 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.
8. Nathan is either the person working on June 15 or the conductor arriving at Urbandale (but not both).
9. The person arriving at Quimby will leave 2 days after the conductor arriving at Zwingle.
10. Neither the conductor working on June 14 nor the person arriving at Vinalhaven is Nathan.
11. The conductor departing from Manson will leave sometime after the person departing from Kent.
12. The person departing from Jackman will leave 3 days after the person departing from Farley.
13. Greg won’t arrive at Yreka.
14. The conductor arriving at Urbandale will leave 4 days after the conductor departing from Daly City.
15. Luke will leave 1 day before the conductor arriving at Vinalhaven.
16. Eugene is either the person arriving at Paradise or the person departing from Daly City (but not both).
17. 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.
18. 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.
19. 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.
Authors: Nil Mamano / Documentation:
 reduction { // Write here your reduction to SAT... } reconstruction { // Write here your solution reconstruction... } To be able to submit you need to either log in, register, or become a guest.