What is mrcpsp2smt?

mrcpsp2smt is a system for solving the Multi-mode Resource-Constrained Project Scheduling Problem (MRCPSP) using Satisfiability Modulo Theories (SMT). It uses an SMT solver (Yices 2) as its core solving engine.

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

The input of mrcpsp2smt are files in .mm format (see PSPLIB). In can also solve instances of MMLIB, but since the file format is slightly different, it has to be specified with the argument -mmlib. Also the single mode RCPSP can be solved, with files in .rcp format.


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 mrcpsp2smt.tar.gz

  4. For usage, see the help:
    mrcpsp2smt -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]


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