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. ​
​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: