mrcpsp2smt

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.

Versions

• 25/07/2016: Version 2.0.01
  See: Bofill, M., Coll, J., Suy, J., & Villaret, M. (2016, November). Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT. In IEEE 28th International Conference on (Tools with Artificial Intelligence (ICTAI), pp. 239-246). IEEE.
• 25/05/2017: Version 3.0.1
  See: Bofill, M., Coll, J., Suy, J., & Villaret, M. Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems. In 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)
• 27/08/2020: Version 4.0.1
  See: Bofill, M., Coll, J., Suy, J., & Villaret, M. SMT encodings for Resource-Constrained Project Scheduling Problems. Computers & Industrial Engineering, 149. 2020

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

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]imae.udg.edu.

Results

• Bofill, M., Coll, J., Suy, J., & Villaret, M. (2016, November). Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT. In IEEE 28th International Conference on (Tools with Artificial Intelligence (ICTAI), pp. 239-246). IEEE.

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

  The executions are done on the j30 set from PSPLIB and MMLIB50 from MMLIB.

• Bofill, M., Coll, J., Suy, J., & Villaret, M. Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems. To appear in 26th International Joint Conference on Artificial Intelligence (IJCAI 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 for the MRCPSP are done on the j30 set from PSPLIB and MMLIB50 from MMLIB. Also, we have solved the RCPSP datasets j30, j60, j90 and j120 with this tool.

• Bofill, M., Coll, J., Suy, J., & Villaret, M. SMT encodings for Resource-Constrained Project Scheduling Problems. Computers & Industrial Engineering, 149. 2020

  Here you can get the detailed results of this work, obtained on a 8GB Intel© Xeon© E3-1220v2 machine at 3.10 GHz.

  The executions for the MRCPSP are done on the j30 set from PSPLIB and MMLIB50 from MMLIB. Also, we have solved the RCPSP datasets j30, j60, j90, j120, Pack and Pack_d with this tool.