What is rcpspt2smt?

rcpspt2smt is a system for solving the Resource-Constrained Project Scheduling Problem with Time-Dependent Resource Capacities and Requests(RCPSP/t) using Satisfiability Modulo Theories (SMT). It uses an SMT solver (Yices 2) as its core solving engine.

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

The input of rcpspt2smt are files in .smt format (see PSPLIB).


Install instructions

  1. Unpack the downloaded file
  2. Download Yices 2 with GMP dynamically linked (2.6) Yices (read its terms of use) and add its path to the LD_LIBRARY_PATH enviroment variable
  3. Add to the PATH enviroment variable the folder where you uncompressed rcpspt2smt.tar.gz

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

This software has been designed and developed for research purposes only. Consequently the required execution arguments can substantially differ in the different versions. Should you need any assistance please contact Jordi Coll, jordi.coll[at_symbol]imae.udg.edu.


Miquel Bofill, Jordi Coll, Josep Suy, and Mateu Villaret
Departament d'Informàtica, Matemàtica Aplicada i Estadística
Universitat de Girona
E-17003 Girona, Spain

Contact: jordi.coll@imae.udg.edu