On the Scalability of Constraint Solving for Static/Off-Line Real-Time Scheduling

Raul Gorcitz (1) , Emilien Kofman (2, 3) , Thomas Carle (4) , Dumitru Potop-Butucaru (2) , Robert de Simone (2)

1 CNES - Centre National d'Études Spatiales [Toulouse]
2 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
3 LEAT - Laboratoire d'Electronique, Antennes et Télécommunications
4 Brown University

Recent papers have reported on successful application of constraint solving techniques to off-line real-time scheduling problems, with realistic size and complexity. Success allegedly came for two reasons: major recent advances in solvers efficiency and use of optimized, problem-specific constraint representations. Our current objective is to assess further the range of applicability and the scalability of such constraint solving techniques based on a more general and agnostic evaluation campaign. For this, we have considered a large number of synthetic scheduling problems and a few real-life ones, and attempted to solve them using 3 state-of-the-art solvers, namely CPLEX, Yices2, and MiniZinc/G12. Our findings were that, for all problems considered, constraint solving does scale to a certain limit, then diverges rapidly. This limit greatly depends on the specificity of the scheduling problem type. All experimental data (synthetic task systems, SMT/ILP models) are provided so as to allow experimental reproducibility.

Mots clés: real-time scheduling; satisfiability modulo theories; constraint solving; repeatable

Domaines: Systèmes embarqués

Raul Gorcitz, Emilien Kofman, Thomas Carle, Dumitru Potop-Butucaru, Robert de Simone. On the Scalability of Constraint Solving for Static/Off-Line Real-Time Scheduling. 13th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2015, Madrid, Spain. pp.16, ⟨10.1007/978-3-319-22975-1_8⟩. ⟨hal-01250010⟩