Detail

Boolean Satisfiability: Algorithms and Applications

The success story of Boolean Satisfiability (SAT) solvers is explained by their increasing effectiveness in solving practical problems. Since the mid 90s, SAT has evolved from a decision problem with theoretical interest, being the first problem to be proved NP-complete, to a problem with key practical interest, finding a wide range of practical applications. SAT solvers are now able to solve instances with hundreds of thousands of variables and millions of clauses. Moreover, SAT solvers are commonly incorporated as black boxes in solvers dealing with richer languages. This talk surveys the organization of modern SAT solvers, highlighting the most relevant algorithmic techniques, and outlines the use of SAT in practical applications.