Scheduling Benchmarks.
These are benchmark files for three types of scheduling problems: courses, classes and exams.
The name of the benchmark file (e.g., courses_flat_0.2_2016_7.cnf) is made of five elements:
1. type: t \in {courses, classes, exams}
2. flat or not: whether the objective has coefficients larger than 1 (if 'flat' mode, then e.g., 2x
becomes x + x)
3. strength: s \in {0.12, 0.16, 0.2} - the value of the objective is forced to be less or equal to s *
(theoretical upper-bound).
4. year
5. month
There are six formats in the set:
cnf - conjunctive normal form. We used minisatp (with flag -cs) to translate the objective to cnf.
opb - optimisation pseudo-Boolean
smt2 - satisfiability modulo theories, v2.
wcnf - weighted cnf. This can be used by weighted max-sat solvers.
mod - used by cplex.
mzn - A format called 'minizinc', which is a standard de-facto for csp solvers.
The benchmarks reflect scheduling problems of 8 semester programs. If the benchmarks is suffixed with "_s" it means that it is a much easier problem, based on a single semester.
Details: Ofer Strichman ofers@ie.technion.ac.il