rcpsp2smt

What is rcpsp2smt?

The rcpsp2smt is a system for solving the Resource-Constrained Project Scheduling Problem (RCPSP) using Satisfiability Modulo Theories (SMT). It uses an SMT solver (Yices 1) as its core solving engine. It supports four different encodings with a large number of variants for each, as well as many formulations of propagators and redundancy constraints.

rcpsp2smt also solves Resource-Constrained Project Scheduling Problems with minimum and maximum time lags (RCPSP/max).

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

The input of rcpsp2smt are files in .rcp, .sch and .sm formats (see PSPLIB). The output is the makespan of the RCPSP or RCPSP/max.

Versions

• 1/09/2012: Initial version 1.1.01

Install instructions

1. Unpack the rcpsp2smt.zip file
2. Download the SMT solver Yices 1 with GMP dynamically linked Yices (read its terms of use) and add the path to the LD_LIBRARY_PATH enviroment variable
3. Add to the PATH enviroment variable the folder where you uncompressed rcpsp2smt.zip

For usage, see the help:
rcpsp2smt -h

License

License