mrcpspmax2smt

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).

Versions

• 21/06/2017: Version 1.0.01
  See: Bofill, M., Coll, J., Suy, J., & Villaret, M. (2017). An Efficient SMT Approach to Solve MRCPSP/max Instances with Tight Constraints on Resources. To appear in 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017)

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

For usage, see the help:
mrcpspmax2smt -h

Results

• Bofill, M., Coll, J., Suy, J., & Villaret, M. (2017). An Efficient SMT Approach to Solve MRCPSP/max Instances with Tight Constraints on Resources. To appear in 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017)

Here you can get the best results obtained by our system, with a timeout of 600 seconds, on a 8GB Intel© Xeon© E3-1220v2 machine at 3.10 GHz.

The executions are done on the mm30, mm50 and mm100 sets from PSP/max library, and the following datasets that were created for this paper:

• mm30_1
• mm50_1
• mm100_1
• mm30_2
• mm50_2
• mm100_2