1st of June, 16:00, room 609

Invited lecture by Prof. Vijay Ganesh (University of Waterloo, Ontario, Canada)

An Empirical Understanding of Conflict-Driven Clause-Learning SAT Solvers

Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. This phenomenon has stumped both theoreticians and practitioners since Boolean satisfiability is an NP-complete problem widely believed to be computationally hard. It is clear that these solvers somehow exploit the structure of real- world instances. However, to-date there have been few results that precisely characterize this structure, or shed any light on why these SAT solvers are so efficient.

In his talk Prof. Ganesh will present a few results that provide a deeper empirical understanding of why CDCL SAT solvers are so efficient. First, he provide evidence that industrial SAT instances have "good community structure", and that this correlates more strongly with the running time of SAT solvers than traditional complexity-theoretic measures of SAT instance size such as number of clauses, variables or clause-variable ratio. Second, we characterize the famous VSIDS branching heuristic through a set of behavioral invariants that we discovered through a rigorous scientific process. Finally, he will present an abstract model of a SAT solver as an "active learner with deductive corrective feedback" that we believe is an accurate and analyzable mathematical model of CDCL solvers.

Website: https://ece.uwaterloo.ca/~vganesh