Schedule for: 18w5208 - Theory and Practice of Satisfiability Solving

Beginning on Sunday, August 26 and ending Friday August 31, 2018

All times in Oaxaca, Mexico time, CDT (UTC-5).

Sunday, August 26
14:00 - 23:59 Check-in begins (Front desk at your assigned hotel)
19:30 - 22:00 Dinner (Restaurant Hotel Hacienda Los Laureles)
20:30 - 21:30 Informal gathering (Hotel Hacienda Los Laureles)
Monday, August 27
07:30 - 08:45 Breakfast (Restaurant at your assigned hotel)
08:45 - 09:00 Introduction and Welcome (Conference Room San Felipe)
09:00 - 10:00 Laurent Simon: Towards an (experimental) understanding of SAT Solvers (Conference Room San Felipe)
10:00 - 11:00 Massimo Lauria: Introduction to Proof Complexity for SAT practitioner (Conference Room San Felipe)
11:00 - 11:30 Coffee Break (Conference Room San Felipe)
11:30 - 12:30 Marijn Heule: Computable Short Proofs (Conference Room San Felipe)
12:30 - 13:15 Presentation of participants (Conference Room San Felipe)
13:20 - 13:30 Group Photo (Hotel Hacienda Los Laureles)
13:30 - 14:30 Lunch (Restaurant Hotel Hacienda Los Laureles)
14:30 - 16:00 Siesta (Conference Room San Felipe)
16:00 - 16:30 Coffee Break (Conference Room San Felipe)
16:30 - 17:30 Jo Devriendt: Symmetry in SAT - a quest for pigeonhole (Conference Room San Felipe)
17:30 - 18:00 Stephan Gocht: Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (Conference Room San Felipe)
18:00 - 18:30 Susanna de Rezende: Clique Is Hard for State-of-the-Art Algorithms (Conference Room San Felipe)
18:30 - 19:00 Moshe Vardi: Boolean Satisfiability: Theory and Engineering (Conference Room San Felipe)
19:00 - 21:00 Dinner (Restaurant Hotel Hacienda Los Laureles)
Tuesday, August 28
07:30 - 09:00 Breakfast (Restaurant at your assigned hotel)
09:00 - 10:00 Jakob Nordstrom: Towards Faster Conflict-Driven Pseudo-Boolean Solving (Conference Room San Felipe)
10:00 - 11:00 Fahiem Bacchus: MaxSat, successful solution techniques and some questions they raise. (Conference Room San Felipe)
11:00 - 11:30 Coffee Break (Conference Room San Felipe)
11:30 - 12:30 Nikolaj Bjorner: SMT solving - foundations and directions (Conference Room San Felipe)
12:30 - 13:30 Ambros Gleixner: Computational Mixed-Integer Programming (Conference Room San Felipe)
13:30 - 14:30 Lunch (Restaurant Hotel Hacienda Los Laureles)
14:30 - 16:00 Siesta (Conference Room San Felipe)
16:00 - 16:30 Coffee Break (Conference Room San Felipe)
16:30 - 17:00 Joao Marques-Silva: Towards MaxSAT-Based Proof Systems (Conference Room San Felipe)
17:00 - 17:30 Nina Narodytska: Formal Analysis of Deep Binarized Neural Networks (Conference Room San Felipe)
17:30 - 18:00 Daniel Le Berre: Pseudo-Boolean Optimization (Conference Room San Felipe)
18:00 - 18:30 Marc Vinyals: Proof Systems for Pseudo-Boolean Solving (Conference Room San Felipe)
18:30 - 19:00 Sam Buss: The (un)reasonable (in)effectiveness of theory for Sat solvers (Conference Room San Felipe)
19:00 - 20:30 Dinner (Restaurant Hotel Hacienda Los Laureles)
20:30 - 22:00 Demo session, discussion on empirical evaluation (Conference Room San Felipe)
Wednesday, August 29
07:30 - 09:00 Breakfast (Restaurant at your assigned hotel)
09:00 - 10:00 Mikoláš Janota: Advances in QBF Solving (Conference Room San Felipe)
10:00 - 11:00 Olaf Beyersdorff: QBF Proof Complexity (Conference Room San Felipe)
11:00 - 11:30 Coffee Break (Conference Room San Felipe)
11:30 - 12:30 Klas Markström: Random k-sat. A review and some new results. (Conference Room San Felipe)
12:30 - 13:30 Lunch (Restaurant Hotel Hacienda Los Laureles)
13:30 - 19:00 Free Afternoon (Oaxaca)
19:00 - 21:00 Dinner (Restaurant Hotel Hacienda Los Laureles)
Thursday, August 30
07:30 - 09:00 Breakfast (Restaurant at your assigned hotel)
09:00 - 10:00 Manuel Kauers: Gröbner bases and applications (Conference Room San Felipe)
10:00 - 11:00 Susan Margulies: Hilbert's Nullstellensatz, Grobner Bases, and NP-Complete Problems (Conference Room San Felipe)
11:00 - 11:30 Coffee Break (Conference Room San Felipe)
11:30 - 12:30 Rahul Santhanam: A Survey on Worst-Case Complexity of SAT (Conference Room San Felipe)
12:30 - 13:00 Kristin Yvonne Rozier: MAX-SAT for Temporal Logics (Conference Room San Felipe)
13:00 - 13:30 Ruben Martins: Conflict-Driven Synthesis (Conference Room San Felipe)
13:30 - 14:30 Lunch (Restaurant Hotel Hacienda Los Laureles)
14:30 - 16:00 Siesta (Conference Room San Felipe)
16:00 - 16:30 Coffee Break (Conference Room San Felipe)
16:30 - 17:00 Martina Seidl: The Symmetry Rule for Quantified Boolean Formulas (Conference Room San Felipe)
17:00 - 17:30 Antonina Kolokolova: The Proof Complexity of SMT Solvers (Conference Room San Felipe)
17:30 - 18:00 Nathan Mull: On CDCL-based Proof Systems with the Ordered Decision Strategy (Conference Room San Felipe)
18:00 - 18:30 Maria Luisa Bonet: Algorithms beyond Resolution using MaxSAT (Conference Room San Felipe)
18:30 - 19:00 Laurent Simon: A few results, questions, and pitfalls in the experimental study of SAT solvers (Conference Room San Felipe)
19:00 - 21:00 Dinner (Restaurant Hotel Hacienda Los Laureles)
Friday, August 31
07:30 - 09:00 Breakfast (Restaurant at your assigned hotel)
09:00 - 09:30 Kuldeep Meel: CrystalBall: Gazing in the Black Box of SAT Solving (Conference Room San Felipe)
09:30 - 10:00 Vijay Ganesh: Machine Learning for SAT Solvers (Conference Room San Felipe)
10:00 - 10:30 Aina Niemetz: From Local Search to Quantifier Elimination for Bit-Vectors in SMT (Conference Room San Felipe)
10:30 - 11:00 Coffee Break (Conference Room San Felipe)
11:00 - 11:30 Albert Atserias: Circular (Yet Sound) Proofs (Conference Room San Felipe)
11:30 - 12:00 Alexander Knop: Hard Satisfiable Formulas for Splittings by Linear Combinations (Conference Room San Felipe)
12:00 - 14:00 Lunch (Restaurant Hotel Hacienda Los Laureles)