AAAI Publications, Ninth Symposium of Abstraction, Reformulation, and Approximation

Font Size: 
Satisfiability Modulo Theories: An Efficient Approach for the Resource-Constrained Project Scheduling Problem
Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

Last modified: 2011-12-14


The Resource-Constrained Project Scheduling Problem (RCPSP) and some of its extensions have been widely studied. Many approaches have been considered to solve this problem: constraint programming (CP), Boolean satisfiability (SAT), mixed integer linear programming (MILP), branch and bound algorithms (BB) and others. In this paper, we present a new approach for solving this problem: satisfiability modulo theories (SMT). Solvers for SMT generalize SAT solving by adding the ability to handle arithmetic and other theories. We provide several encodings of the RCPSP into SMT, and introduce rcp2smt, a tool for solving RCPSP instances using SMT solvers, which exhibits good performance.


RCPSP; Weighted Max-SAT; SMT

Full Text: PDF