What makes modern SAT Solvers work that well
Aus International Center for Computational Logic
What makes modern SAT Solvers work that well
Vortrag von Norbert Manthey
- Veranstaltungsort: APB 3105
- Beginn: 20. Juli 2015 um 14:50
- Ende: 20. Juli 2015 um 15:50
- Forschungsgruppe: Computational Logic
- Forschungsgruppe: Wissensbasierte Systeme
- 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.
