rcpspt2smt

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

Versions

• 25/05/2017: Version 1.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. To appear 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 rcpspt2smt.tar.gz

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.

Results

• 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 RCPSP/t are done on the j30 and j120 sets from PSPLIB.

• 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 RCPSP/t are done on the j30 and j120 sets from PSPLIB.