Skip to main content

SAT Research

Resource-constrained project scheduling using boolean satisfiability problem solvers

We have solved various extensions of the well-known resource-constrained project scheduling problem (RCPSP) using a combination of a fast and efficient meta-heuristic search algorithm and a satisfiability solver (SAT), resulting in the publications discussed below. 

1. First paper: multi-mode RCPSP and SAT

Our first paper that includes SAT solvers to solve resource-constrained project scheduling problems has been published in the European Journal of Operational Research. This paper solves the multi-mode project scheduling problem and the computational results sections shows that it can compete with the best performing procedures from literature. More information on the multi-mode problem and a benchmarking of solution procedures from literature can be found here.

2. Second paper: Including logical constraints

The inclusion of OR constraints and bi-directional (BI) constraints into both the single mode and multi mode resource-constrained project scheduling problem has been investigates in a new paper entitled:

Since the data used in this paper is manupulated to add OR and BI constraints to the project data, we have put all our test data available online, as summarized along the following lines (cf. bottom of this page).

3. Third paper: Activity splitting

The resource-constrained project scheduling problem is extended with activity preemption with setup times, and the SAT algorithm could - once again - easily cope with this challenging problem. The study is published in:

Extra. Download the data for the paper with logical constraints

In the paper, both the PSPLIB and MMLIB instances have been used and transformed to networks with logical constraints. Although the description in the paper should allow the researcher to replicate the instances, we have decided to put them available on this webpage. Each file has a new name XYZ.txt as follows

  • X: Refers to the percentage of logical constraints, e.g. OR10 refers to 10% of OR constraints, and likewise, BI20 refers to 20% bidirectional constraints.
  • Y: Refers to the name of the original database, e.g. j30, j60, j90 or j120 for the PSPLIB and J50, J100 and Jall for the MMLIB50, MMLIB100 and MMLIB+ instances.
  • Z: Refers to the original ID of the file without logical constraints, e.g. 37_8 is file with ID 37_8.

The files contains two main parts, one for describing the SAT clauses and one for describing the activity network

SAT clauses

First number: Number of literals

Second number: Number of clauses that needs to be satisfied.

For each row:

  • Each row starting with a c is a comment row
  • Normal clause row
    • First number: the number of literals that needs to be satisfied
    • Next numbers (except last): the literals (negative means: not)
    • Last number: Always ends with a zero (0)
    • These clauses use the new activity numbering obtained after the network transformations (see below)
  • A clause that starts with a -1 is a special clause that contains non-renewable resource information, as follows
    • The first one third of the numbers is used to refer to the activity modes ID (i.e. the new activity numbering after the network transformations)
    • The second one third of the numbers is used to refer to the resource consumption
    • The last one third of the numbers refers to the activity ID (i.e. the original activity numbering ID, see below)
    • More information on resource clauses can be found in figure 3 of the paper "Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers" by Coelho and Vanhoucke. In this paper, no logical constraints have been used.

Activity network

The activity network is printed in the well-known Patterson format that is widely used in literature. Details of this format can be found here. However, due to the network transformations, the original data instance contains another activity numbering. Therefore, the last lines of the files contain information about the correspondence between the new activity numbering and the numbering of the original format.