A Satisfiability Solving Approach

Abstract

Boolean satisfiability solving is a powerful approach for testing the feasibility of propositional logic formulae in conjunctive normal fosrm. 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 (PStemp Cmax) that incorporate advanced Boolean satisfiability technology such as nogood learning and conflict-driven search. In this chapter, we pres..