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: 20. July 2015 at 2:50 pm
- End: 20. July 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.
