Theoretical Foundations of SAT Solving Workshop
This Workshop will be held in Room 1200 in the Bahen Centre, University of Toronto
Description
The purpose of this workshop is to explore one of the most important problems in all of mathematics and computer science, namely, the Boolean satisfiability problem. While Boolean satisfiability is the quintessential NPcomplete problem, believed to be intractable in general, the last two decades have seen dramatic developments in algorithmic techniques in solving it. These techniques, often referred to as conflictdriven clauselearning (CDCL) SAT solving, routinely solve large realworld instances obtained from wideranging applications such as hardware and software verification, electronic design automation, artificial intelligence, bioinformatics, and operations research, just to name a few examples.
A surprising aspect of this development is that the stateoftheart CDCL SAT solvers can often handle realworld formulas with millions of variables and clauses, but may also get hopelessly stuck on formulas with just a few hundred variables. A fundamental question then is "why do CDCL SAT solvers perform as well as they do, and which underlying properties of Boolean formulas influence their performance the most?" Compounding the mystery is the curious phenomena that CDCLbased techniques are effective in solving large realworld instances from many other hard problem classes, such as the satisfiability problem for quantified Boolean logic which is PSPACEcomplete. These questions remain poorly understood, and worstcase complexity analysis is not sufficient to answer it. We need a deeper mathematical understanding of the inner workings of CDCL SAT solvers, and ideas from parameterized and proof complexity theory to better characterize the classes of instances on which they scale well.
This workshop will gather leading researchers in applied and theoretical areas of SAT solving, logic, and computational complexity, to stimulate an exchange of ideas between these communities that may finally lead to a solution to this problem of "understanding the CDCL paradigm". We see great opportunities for fruitful interplay between theoretical and applied research at the proposed workshop. Such an organized event on a problem as fundamental as Boolean satisfiability, and heuristics to solve it, has the potential for major longterm impact in mathematics, theoretical computer science, and industry.
A tabular schedule for the workshop can be downloaded here.
Schedule
08:50 to 09:00 
Welcome

09:00 to 10:15 
Joao MarquesSilva, University of Lisbon 
10:15 to 10:45 
Coffee break

10:45 to 12:00 
Sam Buss, Univ. of California, San Diego 
12:00 to 14:30 
Lunch

14:30 to 15:00 
Stefan Szeider, TU Wien 
15:00 to 15:30 
Coffee break

15:30 to 16:30 
Ed Zulkoski, University of Waterloo 
16:00 to 16:30 
Daniel Fremont, University of California Berkeley 
16:30 to 17:00 
David Mitchell, Simon Fraser University 
17:15 to 20:00 
Open problems session

09:00 to 10:15 
Jakob Nordstrom, KTH Royal Institute of Technology 
10:15 to 10:45 
Coffee break

10:45 to 12:00 
Armin Biere, Johannes Kepler University 
12:00 to 14:30 
Lunch

14:30 to 15:00 
Sharad Malik, Princeton University 
15:00 to 15:30 
Coffee break

15:30 to 16:30 
Vijay Ganesh, University of Waterloo 
16:00 to 16:30 
Holger Hoos, University of British Columbia 
16:30 to 17:00 
Maria Paola Bonacina, Universita' degli Studi di Verona 
18:30 to 22:00 
Reception and Dinner at Via Vai

09:00 to 10:15 
Moshe Vardi, Rice University 
10:15 to 10:45 
Coffee break

10:45 to 11:15 
Kristin Yvonne Rozier, Iowa State University 
11:15 to 11:45 
No Title Specified
Fahiem Bacchus, University of Toronto 
09:00 to 10:15 
Oliver Kullmann, Swansea University, Marijn Heule, University of Texas at Austin 
10:15 to 10:45 
Coffee break

10:45 to 11:15 
Ryan Williams, Stanford University 
11:15 to 11:45 
Kuldeep Meel, Rice University 
11:45 to 14:30 
Lunch

14:30 to 15:00 
Olaf Beyersdorff, University of Leeds 
15:00 to 15:30 
Coffee break

15:30 to 16:30 
Algebraic Proof Complexity
Toni Pitassi, University of Toronto 
16:30 to 17:00 
Marc Vinyals, KTH Royal Institute of Technology 
09:00 to 10:15 
Karem Sakallah, Qatar Computing Research Institute 
10:15 to 10:45 
Coffee break

10:45 to 11:15 
Eugene Goldberg 
11:15 to 11:45 
Massimo Lauria, Universitat Politecnica de Catalunya 
11:45 to 14:30 
Lunch

14:30 to 15:00 
Pascal Fontaine, Loria, Inria, U. of Lorraine 
15:00 to 15:30 
Coffee break

15:30 to 16:30 
David Witmer, CMU 
16:00 to 16:30 
Ilario Bonacina, KTH Royal Institute of Technology 