SMT/SAT Encoder for Exact Solving of the RCPSP/t

This repository is part of the Research Project (2022) of TU Delft. The implementations were written for a bachelor thesis on "SAT-based optimisation for the resource-constrained project scheduling problem with time-dependent resource capacities and requests" by Jelle Pleunes, supervised by Emir Demirović.

Encoder for the Resource-Constrained Project Scheduling Problem with Time-Dependent Resource Capacities and Requests. Encodes a problem instance into SMT or SAT using the C API provided by Yices 2 (SMT2 language), or into MaxSAT (WCNF file format). For the SMT and SAT approaches this program optimises by calling the Yices solver. For the MaxSAT approach this program writes the encoding to a file. This encoded instance can then be solved using a MaxSAT solver, after which this program can convert the model from the solver back to a solution vector for the RCPSP/t.

Test Data

Test instances that can be parsed by this implementation can be downloaded from http://www.om-db.wi.tum.de/psplib/newinstances.html. These instances were generated by S. Hartmann (2013) (see references below).

Building

The following are prerequisites:

• An installation of the Yices 2 SMT solver: can be installed by following "Quick Installation" from https://github.com/SRI-CSL/yices2. Another option is to use Apt, as explained on the GitHub page. The Makefile and CMakeLists.txt of this project expect that the Yices library is installed in the default location /usr/local/.
• The GMP library version 4.1 or newer (this was already required for Yices).
• For using the Makefile: g++ supporting the C++17 standard.

Building can be done by running make (clean with make clean), or by using CMake.

References

The SMT encoding (input into Yices 2 SMT solver through the provided C API) is wholly based on a paper by M. Bofill et al. (2020):
M. Bofill et al. "SMT encodings for Resource-Constrained Project Scheduling Problems". In: Computers & Industrial Engineering 149 (2020). doi: https://doi.org/10.1016/j.cie.2020.106777.

This encoder program was tested on (and the parser was designed for) instances that were generated as part of a paper by S. Hartmann (2013):
S. Hartmann. "Project scheduling with resource capacities and requests varying with time: a case study". In: Flexible Services and Manufacturing Journal 25 (2013), pp. 74-93. URL: https://doi.org/10.1007/s10696-012-9141-8.

The encoding of Pseudo-Boolean constraints into SAT follows the approach from a paper by I. Abío et al. (2012):
I. Abío et al. "A New Look at BDDs for Pseudo-Boolean Constraints". In: Journal of Artificial Intelligence Research 45 (2012), pp. 443–480.

The SAT (CNF) encoding for precedence constraints is inspired by a paper by A. Horbach (2010):
A. Horbach. "A Boolean satisfiability approach to the resource-constrained project scheduling problem". In: Annals of Operations Research 181 (2010), pp. 89-107. URL: https://doi.org/10.1007/s10479-010-0693-2.