## The tt2bm translator

### Generation of a time-table and translation into a CNF merging instance

tt2bm is a program which can be used both to generate time-tabling instances, and to turn them into distance-based merging instances. For more details, see the paper:

S. Konieczny, J.-M. Lagniez, P. Marquis, "SAT Encodings for Distance-Based Belief Merging Operators", proceedings of AAAI'17.

In order to compile the tt2bm program, execute "make" in the directory TimeTablingGenTrans (once unzipped, and completed by adding to it the library libxml2). In order to use the tt2bm program, execute the following command line in the directory TimeTablingGenTrans:

{a, b} means you have to make a choice between a and b

- -gen, generate a random time-tabling problem instance (the options are: int days, int periods_per_day, int daily_lectures_min, int daily_lectures_max, int nbCourses, int nbTeacher, int min_lectures, int max_lectures, int min_days, int max_days, int min_students, int max_students, int nbRooms, int min_size_room, int max_size_room, int nbBuilding, int nbCurricula, int min_courses_curr, int max_courses_curr, int probaTimeSlot, int probaRoom, int seed)
- BENCHMARK, the name of the benchmark (respecting the PATAT competition XML format) you want to translate into a merging instance

### Time-tabling generation

The resulting instance is displayed in the standard output, here it is redirected to the file test.xml

The generated instance obeys the following constraint:

- the number of days is set to 2
- the number of periods per day is set to 2
- the number of lectures per day lies in [1,2]
- the number of courses is set to 4
- the number of teachers is set to 2
- each course is scheduled on a number of lectures in [1,3]
- each course is scheduled on a minimal number of days belonging to [1,2]
- the number of students attending each course is in [20,50]
- the number of rooms is set to 1
- the capacity of each room is in [30,60]
- the number of buildings is set to 1
- the number of curricula is set to 3
- the number of courses in each curriculum is 2 (i.e., here it is in [2,2])
- the probability that each time slot is available for a lecture is set to 20%
- the probability that each room is available for a lecture is set to 20%
- seed is the seed used for the random generation

### Translation of a time-table into a CNF merging instance

c ch[c][h]: "course c takes place in time slot h"

c cd[c][d]: "course c takes place in day d"

c cr[c][r]: "course c takes place in room r"

c kh[k][h]: "curriculum k takes place in time slot h". This means that some course c that belongs to curriculum k takes place in h.

c ch[0][0] = 1

c ch[0][1] = 2

c ch[0][2] = 3

c ch[0][3] = 4

c ch[1][0] = 5

c ch[1][1] = 6

c ch[1][2] = 7

c ch[1][3] = 8

c ch[2][0] = 9

c ch[2][1] = 10

c ch[2][2] = 11

c ch[2][3] = 12

c ch[3][0] = 13

c ch[3][1] = 14

c ch[3][2] = 15

c ch[3][3] = 16

c cd[0][0] = 17

c cd[0][1] = 18

c cd[1][0] = 19

c cd[1][1] = 20

c cd[2][0] = 21

c cd[2][1] = 22

c cd[3][0] = 23

c cd[3][1] = 24

c cr[0][0] = 25

c cr[1][0] = 26

c cr[2][0] = 27

c cr[3][0] = 28

c kh[0][0] = 29

c kh[0][1] = 30

c kh[0][2] = 31

c kh[0][3] = 32

c kh[1][0] = 33

c kh[1][1] = 34

c kh[1][2] = 35

c kh[1][3] = 36

c kh[2][0] = 37

c kh[2][1] = 38

c kh[2][2] = 39

c kh[2][3] = 40

For instance, ch[2][2] = 11 means that the fact that the course 2 will take place in the time period 2
holds if and only if variable 11 is set to true.

#### Extended DIMACS format for merging CNF instances

The CNF merging instance which results from the translation is displayed to the standard output (on the example, it is redirected to the file test.cnfs). It respects an extended CNF DIMACS format, and is given by a number of lines, as follows:

indicates that #var is the number of variables of the instance, and m is the number of bases in the instance. m is equal to the number of curricula considered in the corresponding time-tabling instance.

are comment lines

Then

indicates that variable v has weight wei

Then one can find a number of lines of the form

which represent the clauses of the integrity constraint in DIMACS format

Finally for each of the m bases one can find groups of lines of the form

... 0

...

... 0

stating first that the base has weight wei, followed by the clauses of
the base in DIMACS format. When a base has weight wei, it is just as if it was occurring
wei times in the input profile. wei is the median value of the numbers of students attending
the courses composing the corresponding curriculum (on the running example, wei is equal to
49 for the first base, to 33 for the second base, and to 49 for the third base).

The encoding of the time-tabling example as a merging
instance is given in the file merging.cnfs