Monday April 22, 2013 at 16h30 in Celestijnenlaan 200A (auditorium 00.225)
Recent Advances in Automated Search Algorithms
by Broes De Cat (PhD student DTAI)
Around 2004, clause learning algorithms were integrated in SAT systems, solvers for Boolean satisfiability problems. Capable of solving many SAT problems without requiring custom choice heuristics was an important step forwards over (traditional) Constraint Programming techniques. In this talk, we give an overview of important subsequent developments in solving search problems, finding solutions to a given set of constraints. These involve for example how to integrate SAT with Constraint Programming and lifting inference techniques to handle the input languages which become ever more general. Although low-level input can be highly optimized, several case studies are presented which illustrate the advantages of high-level encodings and lifted inference available.