What is mrcpspmax2smt?

mrcpspax2smt is a system for solving the Multi-mode Resource-Constrained Project Scheduling Problem with Minimum and Maximum Time Lags (MRCPSP/max) using Satisfiability Modulo Theories (SMT). It uses an SMT solver (Yices 2) as its core solving engine.

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

The input of mrcpspmax2smt are files in .sch format (see PSP/max library).


Install instructions

  1. Unpack the downloaded file
  2. Download Yices 2 with GMP dynamically linked (2.4.2) 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 mrcpspmax2smt.tar.gz

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


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