Scheduling through logic-based tools

Author

Coll Caballero, Jordi

Director

Suy Franch, Josep

Villaret i Ausellé, Mateu

Date of defense

2019-07-15

Pages

168 p.



Department/Institute

Universitat de Girona. Departament d'Informàtica, Matemàtica Aplicada i Estadística (2013-)

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.

Keywords

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

Subjects

004 - Computer science and technology. Computing. Data processing; 51 - Mathematics; 68 - Industries, crafts and trades for finished or assembled articles

Documents

tjcc_20190715.pdf

1.610Mb

 

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/
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/

This item appears in the following Collection(s)