Seminar: Vinyal -- CDCL versus Resolution

Title: CDCL versus Resolution
Speaker: Marc Vinyal (University of Auckland)

Time/Venue: Monday June 15, 10am, J12, Level 2 room 236
Coffee and snacks will be served.

Abstract: Even if SAT is an NP-hard problem, during the last 20 years the
practitioners' viewpoint on SAT has evolved to it being an efficiently solvable
problem. Many problems can now be solved by reducing them to SAT, and even
combinatorial conjectures have been solved in such way. The algorithm behind
this success is called CDCL.

Understanding why CDCL works is hard, and so far the most successful tool for
its analysis has been proof complexity. Under certain assumptions, CDCL is
equivalent to the resolution proof system, which has been studied for a
century. In this talk we will discuss how realistic these assumptions are, what
breaks when we try to make the assumptions more realistic, and how much of an
overhead is hidden under a polynomial equivalence.

Bio: I find how current algorithms for solving hard computational problems
break down after they run into the laws of logic. I am fascinated by the
ability of simple heuristic techniques to solve extremely complex problems,
more so when the same heuristics get stuck when asked to count up to 20.

More formally, my research interests include several areas of computational
complexity, in particular proof complexity and the plentiful connections to
theoretical computer science, logic, and combinatorics. I am also interested in
the theory of Boolean and pseudo-Boolean satisfiability solving.