Heuristic Augmentation of SAT Solvers for MRCPSP

Heuristic Augmentation of SAT Solvers for MRCPSP

Miguel Teixeira de Mendonça, João (TU Delft Electrical Engineering, Mathematics and Computer Science)

Demirović, E. (mentor)
Chakraborty, S.S. (graduation committee)

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2022-06-23

The multi-mode resource-constrained project scheduling problem (MRCPSP) is an NP-hard scheduling problem that concerns activities with several execution modes connected by precedence relations. Precedence relations define a partial ordering in which activities must be processed. The execution mode of an activity defines its processing time and resource needs.

Current solutions mostly rely on heuristics and meta-heuristics. However, Boolean maximum satisfiability (MaxSAT) solvers offer flexibility, the ability to certify optimal solutions, and constant performance improvements. This work proposes a SAT encoding of the MRCPSP that utilises priority-rule heuristics as an upper bound for the encoding and to improve the decisions taken by the solver.

Using priority-rule heuristics dramatically decreases the encoding size and improves the solver's performance. The improved solver can find solutions faster than the original when reasonable initial solutions are available. In their absence, the improved solver finds better solutions by focusing on finding a feasible mode assignment at the beginning of the solving stage.

Algorithm
Scheduling
SAT
RCPSP
MRCPSP
MaxSAT

http://resolver.tudelft.nl/uuid:22033a93-3795-46bd-a5d5-0a6ea4b1b113

Student theses

bachelor thesis

© 2022 João Miguel Teixeira de Mendonça