tt: Timetabling System based on Scarab and Sat4j

Overview

Requirements

  • Java version 1.7.* or higher.
  • Scala version 2.11.*

How to use it

  1. Download the latest version.
  2. Edit file "tt" for your environment.
  3. Exec the following
$ ./tt

DSL

About I/O

  • parse
    • parse *.tim files.
  • dump
    • dump information of current pectt instance.

Abount Constraints

  • defineVars
    • define necessary 0-1 variables
  • h1, h3, h5, m1, s1, s2, s3
    • define each hard and soft constraint
  • defineHard
    • define all hard constraints
  • defineSoft
    • define all soft constraints
  • naTime(e, t)
    • prohibit event 'e' assigned to time 't'
  • naRoom(e, r)
    • prohibit event 'e' assigned to room 'r'
  • commit
    • set commit point of constraints
  • rollback
    • rollback constraints to the last commit point

Abount Solving

  • solve
    • compute solution
  • showSolution
    • print current solution
  • validate
    • validate current solution
  • optimize
    • compute optimum solution according to soft constraints

Example

  • 'tt' is an interactive timetabling system for post-enrollment timetabling.
[soh@asakusa:tt]$ ./tt
Welcome to Scala version 2.11.5 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_11).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import pectt.dsl._
import pectt.dsl._

scala> parse("./example/easy01.tim")
#Rooms: 5
#Events:  100
#Students:  80
#Ave.EventsPerDay:  2.2222222222222223
#Density: 0.4444444444444444

scala> defineVars

scala> defineHard

scala> solve
res3: Boolean = true

scala> showSolution
|    | 000 | 001 | 002 | 003 | 004 |
|-
| 00 |     |     |     |     | 000 |
| 01 |     |     |     |     |     |
| 02 |     |     |     |     |     |
| 03 |     |     |     |     | 003 |
| 04 |     |     |     |     | 005 |
| 05 |     |     |     |     | 007 |
| 06 |     |     |     |     | 011 |
| 07 |     |     |     |     | 014 |
| 08 |     |     |     |     | 016 |
|-
| 09 |     |     |     |     | 017 |
| 10 |     |     |     |     | 018 |
| 11 |     |     |     |     | 022 |
| 12 |     |     |     |     | 023 |
| 13 |     |     |     |     | 025 |
| 14 |     |     |     |     | 029 |
| 15 |     |     |     |     | 032 |
| 16 |     |     |     |     | 035 |
| 17 |     |     |     |     | 036 |
|-
| 18 |     |     |     |     | 039 |
| 19 |     |     |     |     | 043 |
| 20 |     |     |     |     | 046 |
| 21 |     |     |     |     | 047 |
| 22 |     |     |     |     | 048 |
| 23 |     |     |     |     | 052 |
| 24 |     |     |     |     | 053 |
| 25 | 031 |     |     |     | 054 |
| 26 |     |     |     |     | 056 |
|-
| 27 |     |     |     |     | 059 |
| 28 |     | 002 |     |     | 061 |
| 29 | 020 | 004 |     |     | 062 |
| 30 | 001 | 009 |     |     | 063 |
| 31 | 028 | 041 |     |     | 066 |
| 32 | 057 | 042 |     |     | 070 |
| 33 | 015 | 045 | 012 |     | 071 |
| 34 | 030 | 049 | 008 | 006 | 073 |
| 35 | 044 | 038 | 024 | 010 | 075 |
|-
| 36 | 021 | 064 | 026 | 013 | 076 |
| 37 | 065 | 050 | 033 | 019 | 079 |
| 38 | 051 | 078 | 058 | 027 | 087 |
| 39 | 077 | 080 | 034 | 060 | 089 |
| 40 | 072 | 074 | 040 | 037 | 090 |
| 41 | 091 | 081 | 069 | 055 | 092 |
| 42 | 082 | 083 | 084 | 067 | 094 |
| 43 | 093 | 085 | 088 | 068 | 096 |
| 44 | 097 | 099 | 086 | 095 | 098 |

scala> validate
Hard Violation: 0
Soft Violation: 232
   3 events in a row: 36
   1 event in a day : 100
   event on end slot: 96

scala> defineSoft

scala> optimize(4)
RUN-FIRST,easy01,5,100,80,2.22,0.44,232
RUN4,easy01,5,100,80,2.22,0.44,3
RUN3,easy01,5,100,80,2.22,0.44,3
RUN2,easy01,5,100,80,2.22,0.44,3
RUN1,easy01,5,100,80,2.22,0.44,2
RUN0,easy01,5,100,80,2.22,0.44,1

scala> validate
Hard Violation: 0
Soft Violation: 0
   3 events in a row: 0
   1 event in a day : 0
   event on end slot: 0

scala>

Download

Note

  • This software is distributed under the BSD License. See LICENSE file.
  • hss-<version>.jar includes Sat4j package.
    • We really appreciate the developers of Sat4j!

tt as PECTT Solver

  • There is a launcher class for solving PECTT.
  • It can invoked as follows
./ttSolver <option> example/easy01.tim
  • The following options are available.
-h                   : show this help
-opt                 : compute optimum solution
-one                 : add one room support constraints
-all                 : delete room constraints for events that can be held in all rooms

Benchmarks

Links

Scarab SAT-based CP System
Sat4j SAT solver in Java, which Scarab adopts!

Author: Takehide Soh

Created: 2015-03-10 火 10:45

Emacs 24.3.1 (Org mode 8.2.8)

Validate