Model-Based Problem Solving for University Timetable Validation and Improvement

1. Asín Achá, R., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research 218(1), 71–91 (2012)

   Article  Google Scholar 

2. Abrial, J.-R.: The B-Book. Assigning Programs to Meanings. Cambridge University Press (November 2005)

   Google Scholar 

3. Banbara, M., Soh, T., Tamura, N., Inoue, K., Schaub, T.: Answer Set Programming as a Modeling Language for Course Timetabling. Theory and Practice of Logic Programming 13(4-5), 783–798 (2013)

   Article  MATH  MathSciNet  Google Scholar 

4. Bendisposto, J., Clark, J., Dobrikov, I., Krner, P., Krings, S., Ladenberger, L., Leuschel, M., Plagge, D.: ProB 2.0 Tutorial. In: Proceedings of the 4th Rodin User and Developer Workshop. TUCS Lecture Notes. TUCS (2013)

   Google Scholar 

5. Carlsson, M., Ottosson, G.: An Open-Ended Finite Domain Constraint Solver. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997)

   Chapter  Google Scholar 

6. Cooper, T.B., Kingston, J.H.: The complexity of timetable construction problems. In: Burke, E.K., Ross, P. (eds.) PATAT 1995. LNCS, vol. 1153, pp. 281–295. Springer, Heidelberg (1996)

   Chapter  Google Scholar 

7. Corne, D., Ross, P., Fang, H.: Evolving Timetables. Practical Handbook of Genetic Algorithms: Applications 1, 219–276 (1995)

   Google Scholar 

8. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

9. Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194–207. Springer, Heidelberg (2012)

   Chapter  Google Scholar 

10. Deris, S., Omatu, S., Ohta, H.: Timetable planning using the constraint-based reasoning. Computers & Operations Research 27(9), 819–840 (2000)

    Article  MATH  Google Scholar 

11. Di Gaspero, L., McCollum, B., Schaerf, A.: The Second International Timetabling Competition (ITC-2007): Curriculum-based Course Timetabling (Track 3). In: Proceedings of the 14th RCRA Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, Rome (2007)

    Google Scholar 

12. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

13. Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: An extensible ASM execution engine. Fundam. Inform. 77(1-2), 71–103 (2007)

    MATH  Google Scholar 

14. Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11, 256–290 (2002)

    Article  Google Scholar 

15. Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. The Journal of Logic Programming 19(20), 503–581 (1994)

    Article  MathSciNet  Google Scholar 

16. Lach, G., Lübbecke, M.E.: Curriculum based course timetabling: new solutions to Udine benchmark instances. Annals of Operations Research 194(1), 255–272 (2010)

    Article  Google Scholar 

17. Leuschel, M., Schneider, D.: Towards B as a High-Level Constraint Modelling Language. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 101–116. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

18. Lewis, R.: A survey of metaheuristic-based techniques for University Timetabling problems. OR Spectrum 30(1), 167–190 (2008)

    Article  MATH  Google Scholar 

19. Métayer, C.: AnimB 0.1.1 (2010), http://wiki.event-b.org/index.php/AnimB

20. Müller, T., Rudová, H.: Real-life Curriculum-based Timetabling. PATAT (June 2012)

    Google Scholar 

21. Müller, T., Rudová, H.: Real-life curriculum-based timetabling with elective courses and course sections. Annals of Operations Research, 1–18 (June 2014)

    Google Scholar 

22. Plagge, D., Leuschel, M.: Validating B, Z and TLA ⁺ using proB and kodkod. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372–386. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

23. Post, G., Di Gaspero, L., Kingston, J.H., McCollum, B.: The Third International Timetabling Competition. Annals of Operations Research (February 2013)

    Google Scholar 

24. Rudová, H., Murray, K.: University Course Timetabling with Soft Constraints. In: Burke, E.K., De Causmaecker, P. (eds.) PATAT 2002. LNCS, vol. 2740, pp. 310–328. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

25. Schimmelpfeng, K., Helber, S.: Application of a real-world university-course timetabling model solved by integer programming. OR Spectrum 29(4), 783–803 (2006)

    Article  Google Scholar 

26. Shapiro, S.C.: The Jobs Puzzle: A Challenge for Logical Expressibility and Automated Reasoning. In: AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning (2011)

    Google Scholar 

27. Torlak, E., Chang, F.S., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326–341. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

28. Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

29. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA⁺ specifications. In: Pierre, L., Kropf, T. (eds.) Proceedings CHARME’99, pp. 54–66. Springer, Heidelberg (1999)

    Google Scholar 

Download references