Skip to main content
SpringerLink
Log in

A Boolean satisfiability approach to the resource-constrained project scheduling problem

  • Published:
Annals of Operations Research Aims and scope Submit manuscript

Abstract

We formulate the resource-constrained project scheduling problem as a satisfiability problem and adapt a satisfiability solver for the specific domain of the problem. Our solver is lightweight and shows good performance both in finding feasible solutions and in proving lower bounds. Our numerical tests allowed us to close several benchmark instances of the RCPSP that have never been closed before by proving tighter lower bounds and by finding better feasible solutions. Using our method we solve optimally more instances of medium and large size from the benchmark library PSPLIB and do it faster compared to any other existing solver.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Abdulla, P. A., Bjesse, P., & Eén, N. (2000). Symbolic reachability analysis based on SAT-solvers. In S. Graf & M. I. Schwartzbach (Eds.), Lecture notes in computer science : Vol. 1785. TACAS (pp. 411–425). Berlin: Springer.

    Google Scholar 

  • Achterberg, T. (2007). Conflict analysis in mixed integer programming. Discrete Optimization, 4(1), 4–20.

    Article  Google Scholar 

  • Aloul, F. A., Ramani, A., Markov, I. L., & Sakallah, K. A. (2002). Generic ILP versus specialized 0-1 ILP: an update. In L. T. Pileggi, & A. Kuehlmann (Eds.), ICCAD (pp. 450–457). New York: ACM.

    Chapter  Google Scholar 

  • Asín, R., Nieuwenhuis, R., Oliveras, A., & Rodríguez-Carbonell, E. (2009). Cardinality networks and their applications. In Kullmann (pp. 167–180).

  • Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In F. Rossi (Ed.), Lecture notes in computer science : Vol. 2833. CP (pp. 108–122). Berlin: Springer.

    Google Scholar 

  • Bailleux, O., & Boufkhad, Y. (2004). Full CNF encoding: the counting constraints case. In SAT.

  • Bailleux, O., Boufkhad, Y., & Roussel, O. (2009). New encodings of pseudo-Boolean constraints into CNF. In O. Kullmann (Ed.), Lecture notes in compute science : Vol. 5584. Theory and applications of satisfiability testing—SAT 2009 (pp. 181–194). 12th International Conference, SAT 2009, Swansea, UK, June 30—July 3, 2009. Berlin: Springer.

    Chapter  Google Scholar 

  • Baptiste, P., & Demassey, S. (2004). Tight LP bounds for resource constrained project scheduling. OR Spectrum, 26, 251–262.

    Article  Google Scholar 

  • Biere, A., Cimatti, A., Clarke, E. M., & Zhu, Y. (1999). Symbolic model checking without BDDs. In R. Cleaveland (Ed.), Lecture notes in computer science : Vol. 1579. TACAS (pp. 193–207). Berlin: Springer.

    Google Scholar 

  • Brucker, P., & Knust, S. (2000). A linear programming and constraint propagation-based lower bound for the RCPSP. European Journal of Operational Research, 127, 355–362.

    Article  Google Scholar 

  • Brucker, P., Knust, S., Schoo, A., & Thiele, O. (1998). A branch and bound algorithm for the resource-constrained project scheduling problem. European Journal of Operational Research, 107, 272–288.

    Article  Google Scholar 

  • Brucker, P., Drexl, A., Möhring, R., Neumann, K., & Pesch, E. (1999). Resource-constrained project scheduling: notation, classification, models, and methods. European Journal of Operational Research, 112, 3–41.

    Article  Google Scholar 

  • Cook, S. A. (1971). The complexity of theorem proving procedures. In Conf. record of 3rd STOC, Shaker Height, OH (pp. 151–158).

  • Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7(3), 201–215.

    Article  Google Scholar 

  • Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394–397.

    Article  Google Scholar 

  • Debels, D., & Vanhoucke, M. (2007). A decomposition-based genetic algorithm for the resource-constrained project-scheduling problem. Operations Research, 55(3), 457–469.

    Article  Google Scholar 

  • Demeulemeester, E. L., & Herroelen, W. S. (1997). New benchmark results for the resource-constrained project scheduling problem. Management Science, 43(11), 1485–1492.

    Article  Google Scholar 

  • Demeulemeester, E. L., & Herroelen, W. S. (2002). Project scheduling: a research handbook. Boston: Kluwer Academic.

    Google Scholar 

  • Dorndorf, U., Pesch, E., & Phan-Huy, T. (2000a). A branch-and-bound algorithm for the resource-constrained project scheduling problem. Mathematical Methods of Operations Research, 52, 413–439.

    Article  Google Scholar 

  • Dorndorf, U., Pesch, E., & Phan-Huy, T. (2000b). Constraint propagation techniques for the disjunctive scheduling problem. Artificial Intelligence, 122, 189–240.

    Article  Google Scholar 

  • Dorndorf, U., Pesch, E., & Phan-Huy, T. (2000c). A time-oriented branch-and-bound algorithm for resource-constrained project scheduling with generalised precedence constraints. Management Science, 46(10), 1365–1384.

    Article  Google Scholar 

  • Eén, N., & Sörensson, N. (2004). An extensible SAT-solver. In Theory and applications of satisfiability testing (pp. 502–518). Berlin: Springer.

    Chapter  Google Scholar 

  • Eén, N., & Sörensson, N. (2006). Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2, 1–26.

    Google Scholar 

  • Ernst, M. D., Millstein, T. D., & Weld, D. S. (1997). Automatic SAT-compilation of planning problems. In IJCAI (pp. 1169–1177).

  • Gelder, A. V. (2008). Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics, 156(2), 230–243.

    Article  Google Scholar 

  • Gent, I. P. (2002). Arc consistency in SAT. In F. van Harmelen (Ed.), ECAI (pp. 121–125). Amsterdam: IOS Press.

    Google Scholar 

  • Gomes, C. P., Kautz, H., Sabharwal, A., & Selman, B. (2008). Satisfiability solvers. In Handbook of knowledge representations (pp. 89–132). Amsterdam: Elsevier.

    Chapter  Google Scholar 

  • Hartmann, S., & Briskorn, D. (2008). A survey of deterministic modeling approaches for project scheduling under resource constraints. Tech. Rep. 2/2008, Hamburg School of Business Administration.

  • Herroelen, W. (2005). Project scheduling—theory and practice. Production & Operations Management, 14(4), 413–432.

    Article  Google Scholar 

  • Hooker, J. N. (2007). Relaxation. In Integrated methods for optimization (Vol. 100). New York: Springer.

    Google Scholar 

  • Igelmund, G., & Radermacher, F. J. (1983a). Algorithmic approaches to preselective strategies for stochastic scheduling problems. Networks, 13, 29–48.

    Article  Google Scholar 

  • Igelmund, G., & Radermacher, F. J. (1983b). Preselective strategies for the optimization of stochastic project networks under resource constraints. Networks, 13, 1–28.

    Article  Google Scholar 

  • Klein, R., & Scholl, A. (1999a). Computing lower bounds by destructive improvement: an application to resource-constrained project scheduling. European Journal of Operational Research, 112(2), 322–346.

    Article  Google Scholar 

  • Klein, R., & Scholl, A. (1999b). Scattered branch and bound: an adaptive search strategy applied to resource-constrained project scheduling. Central European Journal of Operations Research, 7, 177–201.

    Google Scholar 

  • Kolisch, R., Sprecher, A., & Drexl, A. (1995). Characterization and generation of a general class of resource-constrained project scheduling problems. Management Science, 41, 1693–1703.

    Article  Google Scholar 

  • Levin, L. (1973). Universal sequential search problem. Problems of Information Transmission, 9, 265–266.

    Google Scholar 

  • Liess, O., & Michelon, P. (2008). A constraint programming approach for the resource-constrained project scheduling problem. Annals of Operations Research, 157, 25–36.

    Article  Google Scholar 

  • Marques-Silva, J. (2008). Model checking with Boolean satisfiability. Journal of Algorithms, 63(1–3), 3–16.

    Article  Google Scholar 

  • Marques-Silva, J., & Sakallah, K. A. (1999). GRAPS: a search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5), 506–521.

    Article  Google Scholar 

  • Marques-Silva, J. P., & Lynce, I. (2007). Towards robust CNF encodings of cardinality constraints. In C. Essiere (Ed.), Lecture notes in computer science : Vol. 4741. CP (pp. 483–497). Berlin: Springer.

    Google Scholar 

  • Mingozzi, A., Maniezzo, V., Ricciardelli, S., & Bianco, L. (1998). An exact algorithm for the resource-constrained project scheduling problem based on a new mathematical formulation. Management Science, 44, 714–729.

    Article  Google Scholar 

  • Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: engineering an efficient SAT solver. In DAC (pp. 530–535).

  • Pesch, E., & Tetzlaff, U. A. W. (1996). Constraint propagation based scheduling of job shops. INFORMS Journal on Computing, 8, 144–157.

    Article  Google Scholar 

  • Sebastiani, R. (2007). Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, 3, 141–224.

    Google Scholar 

  • Sprecher, A. (2000). Scheduling resource-constrained projects competitively at modest memory requirements. Management Science, 46, 710–723.

    Article  Google Scholar 

  • Warners, J. P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63–69.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Business Administration, Christian-Albrechts-Universität zu Kiel, Kiel, 24098, Germany

    Andrei Horbach

Authors
  1. Andrei Horbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrei Horbach.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Horbach, A. A Boolean satisfiability approach to the resource-constrained project scheduling problem. Ann Oper Res 181, 89–107 (2010). https://doi.org/10.1007/s10479-010-0693-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10479-010-0693-2

Keywords

Search

Navigation