A scheduling problem can be defined in a nutshell as the problem of determining when and how the activities of a project have to be run, according to some project requirements. Such problems are ubiquitous nowadays since they frequently appear in industry and services. In most cases the computation of solutions of scheduling problems is hard, especially when some objective, such as the duration of the project, has to be optimised. The recent performance advances on solving the problems of Boolean Satisfiability (SAT) and SAT Modulo Theories (SMT) have risen the interest in formulating hard combinatorial problems as SAT or SMT formulas, which are then solved with efficient algorithms. One of the principal advantages of such logic-based techniques is that they can certify optimality of solutions.
The main contribution of this thesis is the presentation of efficient SMT-based methods to solve scheduling problems. More precisely we tackle the well-known Resource-Constrained Project Scheduling Problem (RCPSP) as well as many extensions of this problem with additional requirements and modelling challenges. Namely, we also solve the problems commonly denoted by MRCPSP, RCPSP/t, MRCPSP/max and MSPSP. The most challenging constraints in RCPSP-based problems are resource constraints, which specify a limited availability of shared resources, usually renewable, that activities cannot surpass at any time. To handle such constraints we use decision diagram based SAT encodings of pseudo-Boolean (PB) constraints. Since these encodings have a high impact on solving times, we take advantage of collateral constraints to compactly encode PB constraints, while preserving good propagation properties. However we go one step further, because we believe that such PB encoding technique can be useful in other fields different than scheduling. With this idea in mind, we design our PB encodings in an application-independent way, and we provide many encoding alternatives different from decision diagram representations. The systems that we present are able to outperform the best state-of-the-art exact solvers for the studied scheduling problems.Air Jordan Retro 1 red black white