Symposium on Abstraction, Reformulation and Approximation · 2011 · 30 citations · 26 references
ManagementComputer ScienceOptimizationProject SchedulingSchedulingConstraint ProgrammingConstraint SatisfactionInteger ProgrammingResource-constrained SchedulingSatisfiability Modulo TheoriesScheduling TheoryBoolean SatisfiabilityBoolean Satisfiability Modulo TheoriesBoolean Satisfiability ProblemMixed-integer Linear ProgrammingMixed-integer ProgrammingResource-constrained Project SchedulingSatisfiabilityScheduling Problems
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.
26