Scheduling through logic-based tools

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.