What is rcpsp2smt?

The rcpsp2smt is a system for solving the Resource-Constrained Project Scheduling Problem (RCPSP) using Satisfiability Modulo Theories (SMT). It uses an SMT solver (Yices 1) as its core solving engine. It supports four different encodings with a large number of variants for each, as well as many formulations of propagators and redundancy constraints.

rcpsp2smt also solves Resource-Constrained Project Scheduling Problems with minimum and maximum time lags (RCPSP/max).

The rcpsp2smt system is written in C++ and uses the API's of Yices 1. We only provide a GNU/Linux executable.

The input of rcpsp2smt are files in .rcp, .sch and .sm formats (see PSPLIB). The output is the makespan of the RCPSP or RCPSP/max.


Install instructions

  1. Unpack the rcpsp2smt.zip file
  2. Download the SMT solver Yices 1 with GMP dynamically linked Yices (read its terms of use) and add the path to the LD_LIBRARY_PATH enviroment variable
  3. Add to the PATH enviroment variable the folder where you uncompressed rcpsp2smt.zip

  4. For usage, see the help:
    rcpsp2smt -h



Miquel Bofill, Miquel Palahí, Josep Suy,
and Mateu Villaret  
Departament d'Informàtica, Matemàtica Aplicada i Estadística
Universitat de Girona
E-17003 Girona, Spain
Carlos Ansótegui
Departament d'Informàtica i Enginyeria Industrial
Universitat de Lleida
E-25003 Lleida, Spain
Contact: suy@ima.udg.edu