Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT

The Multi-Mode Resource-Constrained Project Scheduling Problem (MRCPSP) is a generalization of the well known Resource-Constrained Project Scheduling Problem (RCPSP). The most common exact approaches for solving this problem are based on branch-and-bound algorithms, mixed integer linear programming...

Full description

Saved in:
Bibliographic Details
Main Authors: Bofill, Miquel, Coll, Jordi, Suy, Josep, Villaret, Mateu
Format: Conference Proceeding
Language:English
Subjects:
Encoding
Integer linear programming
MRCPSP
Optimization
SAT
Schedules
scheduling
Search problems
Silicon
SMT
Upper bound
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The Multi-Mode Resource-Constrained Project Scheduling Problem (MRCPSP) is a generalization of the well known Resource-Constrained Project Scheduling Problem (RCPSP). The most common exact approaches for solving this problem are based on branch-and-bound algorithms, mixed integer linear programming and Boolean satisfiability (SAT). In this paper, we present a new exact approach for solving this problem, using Satisfiability Modulo Theories (SMT). We provide two encodings into SMT and several reformulation and preprocessing techniques. The optimization algorithm that we propose uses an SMT solver as an oracle, and depending on its answer is able to update the encoding for the next optimization step. We report extensive performance experiments showing the utility of the proposed techniques and the good performance of our approach that allows us to close several open instances.
ISSN:2375-0197
DOI:10.1109/ICTAI.2016.0045