# What makes modern SAT Solvers work that well

From International Center for Computational Logic

# What makes modern SAT Solvers work that well

*Talk by Norbert Manthey*

- Location: APB 3105
- Start: July 20, 2015 at 2:50 pm
- End: July 20, 2015 at 3:50 pm
- Research group: Computational Logic
- Research group: Knowledge-Based Systems
- Event series: KBS Seminar
- iCal

When the satisfiability testing is explained to students, they usually hear about the DPLL algorithm from the 1960. Although modern algorithms are still build on the principles of that algorithm, a few modifications have been added that improve the strength of the reasoner significantly. With the CDCL algorithm, for some problems an unsatisfiability proof can be generated exponentially faster than with DPLL. The talk first presents the DPLL algorithm, and then presents the basic concepts of the CDCL algorithm.