Item


Scheduling through logic-based tools

Scheduling problems consist in determining how to execute the activities of a project in order to satisfy some requirements. Such problems are ubiquitous nowadays in industry and services, but finding solutions of scheduling problems is computationally hard. The main contribution of this thesis is the presentation of efficient SAT and SMT-based methods to solve scheduling problems. More precisely we tackle the well-known problem RCPSP as well as many extensions of it. The most challenging constraints in RCPSP-based problems are resource constraints, which specify that activities must share a set of finite resources. To handle such constraints we provide efficient SAT encodings of pseudo-Boolean (PB) constraints, which take into account the existence of collateral constraints. The provided PB encodings can have application to combinatorial problems in general, not only scheduling. The systems that we present are state-of-the-art in exact scheduling solving.

Un problema de scheduling consisteix en decidir com executar les activitats d’un projecte per tal de satisfer un seguit de requeriments. Aquests problemes són molt presents en els sectors de la industria i els serveis, però trobar una solució d’un problema de scheduling és computacionalment costós. La contribució principal d’aquesta tesi és presentar mètodes eficients basats en codifiacions de SAT i SMT per solucionar problemes de scheduling. Concretament ataquem el conegut problema RCPSP i diverses extensions d’aquest. Les restriccions més complexes en aquests problemes són les d’ús de recursos finits compartits entre activitats. Per tal de tractar aquestes restriccions, proporcionem codificacions eficients a SAT de restriccions pseudo-Booleanes (PB), que tenen en compte l’existència de restriccions col·laterals. Les codificacions de PB proposades són de propòsit general i poden tenir aplicació a tot tipus de problemes combinatoris. Les eines que presentem es situen en l’estat de l’art de solucionar problemes de scheduling.

Universitat de Girona

Manager: Suy Franch, Josep
Villaret i Ausellé, Mateu
Other contributions: Universitat de Girona. Departament d’Informàtica, Matemàtica Aplicada i Estadística (2013-)
Author: Coll Caballero, Jordi
Date: 2019 July 15
Abstract: Scheduling problems consist in determining how to execute the activities of a project in order to satisfy some requirements. Such problems are ubiquitous nowadays in industry and services, but finding solutions of scheduling problems is computationally hard. The main contribution of this thesis is the presentation of efficient SAT and SMT-based methods to solve scheduling problems. More precisely we tackle the well-known problem RCPSP as well as many extensions of it. The most challenging constraints in RCPSP-based problems are resource constraints, which specify that activities must share a set of finite resources. To handle such constraints we provide efficient SAT encodings of pseudo-Boolean (PB) constraints, which take into account the existence of collateral constraints. The provided PB encodings can have application to combinatorial problems in general, not only scheduling. The systems that we present are state-of-the-art in exact scheduling solving.
Un problema de scheduling consisteix en decidir com executar les activitats d’un projecte per tal de satisfer un seguit de requeriments. Aquests problemes són molt presents en els sectors de la industria i els serveis, però trobar una solució d’un problema de scheduling és computacionalment costós. La contribució principal d’aquesta tesi és presentar mètodes eficients basats en codifiacions de SAT i SMT per solucionar problemes de scheduling. Concretament ataquem el conegut problema RCPSP i diverses extensions d’aquest. Les restriccions més complexes en aquests problemes són les d’ús de recursos finits compartits entre activitats. Per tal de tractar aquestes restriccions, proporcionem codificacions eficients a SAT de restriccions pseudo-Booleanes (PB), que tenen en compte l’existència de restriccions col·laterals. Les codificacions de PB proposades són de propòsit general i poden tenir aplicació a tot tipus de problemes combinatoris. Les eines que presentem es situen en l’estat de l’art de solucionar problemes de scheduling.
Format: application/pdf
Other identifiers: http://hdl.handle.net/10803/667963
Document access: http://hdl.handle.net/10256/17246
Language: eng
Publisher: Universitat de Girona
Rights: L’accés als continguts d’aquesta tesi queda condicionat a l’acceptació de les condicions d’ús establertes per la següent llicència Creative Commons: http://creativecommons.org/licenses/by/4.0/
Subject: Scheduling
Programació de tasques
Programación de tareas
Pseudo-Boolean constraints
Restricciones pseudo-booleanas
Restriccions pseudo-Booleanes
Satisfiability modulo theories
Satisfactibilitat mòdul teories
Satisfacibilidad módulo teorias
004 - Informàtica
51 - Matemàtiques
68 - Indústries, oficis i comerç d’articles acabats. Tecnologia cibernètica i automàtica
Title: Scheduling through logic-based tools
Type: info:eu-repo/semantics/doctoralThesis
Repository: DUGiDocs

Subjects

Authors