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:

How to use the tt2bm translator:
$ ./bin/tt2bm {-gen options, BENCHMARK}
{a, b} means you have to make a choice between a and b

Time-tabling generation

Here is an example of generation of a random time-tabling instance:
$ ./bin/tt2bm -gen 2 2 1 2 4 2 1 3 1 2 20 50 1 30 60 1 3 2 2 20 20 0 > test.xml

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:

In order to display the generated instance, use:
$ cat test.xml <?xml version="1.0" encoding="UTF-8" standalone="no"?> <!DOCTYPE instance SYSTEM "random generator"> <instance name="rdm_0"> <descriptor> <days value="2"/> <periods_per_day value="2"/> <daily_lectures min="1" max="2"/> </descriptor> <courses> <course id="c0" teacher="t2" lectures="2" min_days="2" students="25" double_lectures="yes"/> <course id="c1" teacher="t2" lectures="1" min_days="1" students="27" double_lectures="yes"/> <course id="c2" teacher="t2" lectures="2" min_days="1" students="33" double_lectures="no"/> <course id="c3" teacher="t1" lectures="2" min_days="1" students="49" double_lectures="no"/> </courses> <rooms> <room id="r0" size="31" building="1"/> </rooms> <curricula> <curriculum id="q0"> <course ref="c0"/> <course ref="c3"/> </curriculum> <curriculum id="q1"> <course ref="c2"/> <course ref="c0"/> </curriculum> <curriculum id="q2"> <course ref="c3"/> <course ref="c2"/> </curriculum> </curricula> <constraints> <constraint type="period" course="c0"> <timeslot day="0" period="0"/> <timeslot day="1" period="1"/> </constraint> </constraints> </instance>

Translation of a time-table into a CNF merging instance

In order to translate the time-tabling instance (stored in file test.xml), use:
$ ./bin/tt2bm test.xml > merging.cnfs
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:

p cnf #var m

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.

c ...

are comment lines

Then

w v wei

indicates that variable v has weight wei

Then one can find a number of lines of the form

... 0

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

s wei
... 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