Skip to main content
SpringerLink
Log in
Book cover

Handbook on Project Management and Scheduling Vol.1 pp 135–160Cite as

A Satisfiability Solving Approach

  • Chapter
  • First Online:

Part of the book series: International Handbooks on Information Systems ((INFOSYS))

Abstract

Boolean satisfiability solving is a powerful approach for testing the feasibility of propositional logic formulae in conjunctive normal form. Nowadays, Boolean satisfiability solvers efficiently handle problems with millions of clauses and hundreds of thousands of Boolean variables. But still many combinatorial problems such as resource-constrained project scheduling are beyond their capabilities. However, hybrid solution approaches have recently been proposed for resource-constrained project scheduling with generalized precedence constraints (PS | temp | C max ) that incorporate advanced Boolean satisfiability technology such as nogood learning and conflict-driven search. In this chapter, we present a generic exact method for PS | temp | C max using one of the most successful hybrid approaches called lazy clause generation. This approach combines constraint programming solving with Boolean satisfiability solving.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In the literature, generalized precedence relations are also known as temporal precedences, arbitrary precedences, minimal and maximal time lags, or time windows.

References

  • Achterberg T (2009) SCIP: solving constraint integer programs. Math Program Comput 1(1):1–41

    Article  Google Scholar 

  • Aggoun A, Beldiceanu N (1993) Extending CHIP in order to solve complex scheduling and placement problems. Math Comput Model 17(7):57–73

    Article  Google Scholar 

  • Ansótegui C, Bofill M, Palahí M, Suy J, Villaret M (2011) Satisfiability modulo theories: an efficient approach for the resource-constrained project scheduling problem. In: Genesereth MR, Revesz PZ (eds) Proceedings of the ninth symposium on abstraction, reformulation, and approximation, SARA 2011. AAAI Press, Menlo Park

    Google Scholar 

  • Baptiste P, Le Pape C, Nuijten W (2001) Constraint-based scheduling. Kluwer, Norwell

    Book  Google Scholar 

  • Bartusch M, Möhring RH, Radermacher FJ (1988) Scheduling project networks with resource constraints and time windows. Ann Oper Res 16(1):199–240

    Article  Google Scholar 

  • Bellman R (1958) On a routing problem. Q Appl Math 16(1):87–90

    Google Scholar 

  • Berthold T, Heinz S, Lübbecke ME, Möhring RH, Schulz J (2010) A constraint integer programming approach for resource-constrained project scheduling. In: Lodi A, Milano M, Toth P (eds) Integration of AI and OR techniques in constraint programming for combinatorial optimization problems. Lecture notes in computer science, vol 6140. Springer, Heidelberg, pp 313–317

    Chapter  Google Scholar 

  • Brucker P, Drexl A, Möhring R, Neumann K, Pesch E (1999) Resource-constrained project scheduling: notation, classification, models, and methods. Eur J Oper Res 112(1):3–41

    Article  Google Scholar 

  • Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7:201–215

    Article  Google Scholar 

  • Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. Commun ACM 5(7):394–397

    Article  Google Scholar 

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

    Article  Google Scholar 

  • Dutertre B, de Moura L (2006) The Yices SMT solver. http://yices.csl.sri.com/tool-paper.pdf

  • Feydy T (2010) Constraint programming: improving propagation. Ph.D. dissertation, University of Melbourne, Melbourne

    Google Scholar 

  • Feydy T, Stuckey PJ (2009) Lazy clause generation reengineered. In: Gent I (ed) Proceedings of the 15th international conference on principles and practice of constraint programming. Lecture notes in computer science, vol 5732. Springer, Heidelberg, pp 352–366

    Google Scholar 

  • Feydy T, Schutt A, Stuckey PJ (2008) Global difference constraint propagation for finite domain solvers. In: Antoy S, Albert E (eds) Proceedings of principles and practice of declarative programming – PPDP 2008. ACM, New York, pp 226–235

    Google Scholar 

  • Feydy T, Somogyi Z, Stuckey PJ (2011) Half reification and flattening. In: Lee JHM (ed) Proceedings of principles and practice of constraint programming – CP 2011. Lecture notes in computer science, vol 6876. Springer, Heidelberg, pp 286–301

    Chapter  Google Scholar 

  • Ford LR Jr, Fulkerson DR (1962) Flows in networks. Princeton University Press, Princeton

    Google Scholar 

  • Franck B, Neumann K, Schwindt C (2001) Truncated branch-and-bound, schedule-construction, and schedule-improvement procedures for resource-constrained project scheduling. OR Spectr 23(3):297–324

    Article  Google Scholar 

  • Heinz S, Schulz J (2011) Explanations for the cumulative constraint: an experimental study. In: Pardalos PM, Rebennack S (eds) Experimental algorithms. Lecture notes in computer science, vol 6630. Springer, Heidelberg, pp 400–409

    Chapter  Google Scholar 

  • Heinz S, Schulz J, Beck JC (2013) Using dual presolving reductions to reformulate cumulative constraints. Constraints 18(2):166–201

    Article  Google Scholar 

  • Horbach A (2010) A boolean satisfiability approach to the resource-constrained project scheduling problem. Ann Oper Res 181:89–107

    Article  Google Scholar 

  • Huang J (2007) The effect of restarts on the efficiency of clause learning. In: Veloso MM (ed) Proceedings of artificial intelligence – IJCAI 2007, pp 2318–2323

    Google Scholar 

  • Kolisch R, Schwindt C, Sprecher A (1998) Benchmark instances for project scheduling problems. In: Wȩglarz J (ed) Project scheduling: recent models, algorithms and applications. Kluwer, Boston, pp 197–212

    Google Scholar 

  • Le Pape C (1994) Implementation of resource constraints in ILOG SCHEDULE: a library for the development of constraint-based scheduling systems. Intell Syst Eng 3(2):55–66

    Google Scholar 

  • Marriott K, Stuckey PJ (1998) Programming with constraints: an introduction. The MIT Press, Cambridge

    Google Scholar 

  • Mercier L, Van Hentenryck P (2008) Edge finding for cumulative scheduling. INFORMS J Comput 20(1):143–153

    Article  Google Scholar 

  • Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Design automation conference. ACM, New York, pp 530–535

    Google Scholar 

  • Neumann K, Schwindt C (1997) Activity-on-node networks with minimal and maximal time lags and their application to make-to-order production. OR Spectr 19:205–217

    Article  Google Scholar 

  • Ohrimenko O, Stuckey PJ, Codish M (2009) Propagation via lazy clause generation. Constraints 14(3):357–391

    Article  Google Scholar 

  • Project Duration Problem RCPSP/max (2010). http://www.wior.uni-karlsruhe.de/LS_Neumann/Forschung/ProGenMax/rcpspmax.html

  • Schutt A, Wolf A (2010) A new \(\mathcal{O}(n^{2}\log n)\) not-first/not-last pruning algorithm for cumulative resource constraints. In: Cohen D (ed) Principles and practice of constraint programming – CP 2010. Lecture notes in computer science, vol 6308. Springer, Heidelberg, pp 445–459

    Chapter  Google Scholar 

  • Schutt A, Feydy T, Stuckey PJ, Wallace MG (2009) Why cumulative decomposition is not as bad as it sounds. In: Gent IP (ed) Proceedings of principles and practice of constraint programming – CP 2009. Lecture notes in computer science, vol 5732. Springer, Heidelberg, pp 746–761

    Chapter  Google Scholar 

  • Schutt A, Feydy T, Stuckey PJ, Wallace MG (2011) Explaining the cumulative propagator. Constraints 16(3):250–282

    Article  Google Scholar 

  • Schutt A, Chu G, Stuckey PJ, Wallace MG (2012) Maximising the net present value for resource-constrained project scheduling. In: Beldiceanu N, Jussien N, Pinson E (eds) Integration of AI and OR techniques in contraint programming for combinatorial optimzation problems. Lecture notes in computer science, vol 7298. Springer, Heidelberg, pp 362–378

    Chapter  Google Scholar 

  • Schutt A, Feydy T, Stuckey P (2013a) Explaining time-table-edge-finding propagation for the cumulative resource constraint. In: Gomes CP, Sellmann M (eds) Integration of AI and OR techniques in constraint programming for combinatorial optimization problems. Lecture notes in computer science, vol 7874. Springer, Heidelberg, pp 234–250

    Chapter  Google Scholar 

  • Schutt A, Feydy T, Stuckey PJ, Wallace MG (2013b) Solving RCPSP/max by lazy clause generation. J Sched 16(3):273–289

    Article  Google Scholar 

  • Schwindt C (1995) ProGen/max: a new problem generator for different resource-constrained project scheduling problems with minimal and maximal time lags. WIOR 449, Universität Karlsruhe, Karlsruhe

    Google Scholar 

  • Tsang E (1993) Foundations of constraint satisfaction. Academic, London

    Google Scholar 

  • Vilím P (2011) Timetable edge finding filtering algorithm for discrete cumulative resources. In: Achterberg T, Beck JC (eds) Integration of AI and OR techniques in constraint programming for combinatorial optimization problems. Lecture notes in computer science, vol 6697. Springer, Heidelberg, pp 230–245

    Chapter  Google Scholar 

  • Walsh T (1999) Search in a small world. In: Proceedings of artificial intelligence – IJCAI 1999. Morgan Kaufmann, San Francisco, pp 1172–1177

    Google Scholar 

Download references

Acknowledgements

NICTA is funded by the Australian Government as represented by the Department of Communications and the Australian Research Council through the ICT Centre of Excellence program. This work was partially supported by Asian Office of Aerospace Research and Development grant 10-4123.

Author information

Authors and Affiliations

  1. National ICT Australia & Computing and Information Systems, University of Melbourne, Melbourne, VIC, Australia

    Andreas Schutt, Thibaut Feydy & Peter J. Stuckey

  2. Opturion & Faculty of Information Technology, Monash University, Caulfield, VIC, Australia

    Mark G. Wallace

Authors
  1. Andreas Schutt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thibaut Feydy
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter J. Stuckey
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mark G. Wallace
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andreas Schutt .

Editor information

Editors and Affiliations

  1. Institute of Management and Economics, Clausthal University of Technology, Clausthal-Zellerfeld, Germany

    Christoph Schwindt

  2. Institute of Management and Economics, Clausthal University of Technology, Clausthal-Zellerfeld, Germany

    Jürgen Zimmermann

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Schutt, A., Feydy, T., Stuckey, P.J., Wallace, M.G. (2015). A Satisfiability Solving Approach. In: Schwindt, C., Zimmermann, J. (eds) Handbook on Project Management and Scheduling Vol.1. International Handbooks on Information Systems. Springer, Cham. https://doi.org/10.1007/978-3-319-05443-8_7

Download citation

Publish with us

Policies and ethics

Search

Navigation