Explore the fundamentals and advanced concepts of SAT-Solving in this comprehensive 2-hour lecture by Armin Biere from Johannes Kepler University. Delve into topics such as variables, SAT, local constraints, operators, representations, and the assumption trick. Learn about the CDCL procedure and its interactive aspects, as well as the Reading Evaluate Print Loop. Gain insights into the theory and practice of satisfiability, and discover how it extends beyond traditional applications. This talk, part of the Satisfiability: Theory, Practice, and Beyond Boot Camp at the Simons Institute, offers a deep dive into the world of SAT-Solving for both beginners and experienced practitioners.
Overview
Syllabus
Intro
About the video
Variables
SATSolving Handbook
What is SATSolving
Local Constraints
Operators
Representations
Assumption Trick
Reading Evaluate Print Loop
Fine Points
Interactive CDC
DP Procedure
Taught by
Simons Institute