Welcome Dates Committees CFP Workshops Proceedings Program Competitions Speakers Summer-School Registration Venue

Tuesday, July 9th
09:00-09:30Session 1: Welcome
09:30-10:30Session 2: Best papers ( chair: Roberto Sebastiani )
09:30-10:00Nikhil Vyas and Ryan Williams. On Super Strong ETH
10:00-10:30Katalin Fazekas, Armin Biere and Christoph Scholl. Incremental Inprocessing in SAT Solving
10:30-11:00Coffee break
11:00-12:30Session 3 ( chair: Friedrich Slivovsky )
11:00-11:30Leroy Chew and Judith Clymo. The Equivalences of Refutational QRAT[slides]
11:30-12:00Benjamin Kiesl and Martina Seidl. QRAT Polynomially Simulates \forall-Exp+Res
12:00-12:30Sam Buss and Neil Thapen. DRAT Proofs, Propagation Redundancy, and Extended Resolution[slides]
14:00-15:30Session 4 ( chair: Armin Biere )
14:00-14:30Daniel Selsam and Nikolaj Bjorner. NeuroCore: Guiding CDCL with Unsat Core Predictions
14:30-15:00Carlos Mencía, Oliver Kullmann, Alexey Ignatiev and Joao Marques-Silva. On Computing the Union of MUSes
15:00-15:30Marijn Heule, Manuel Kauers and Martina Seidl. Local Search for Fast Matrix Multiplication
15:30-16:00Coffee break
16:00-17:30Session 5 ( chair: Luca Pulina )
16:00-16:30Joshua Blinkhorn and Olaf Beyersdorff. Proof Complexity of QBF Symmetry Recomputation
16:30-17:00Leander Tentrup and Markus N. Rabe. Clausal Abstraction for DQBF
17:00-17:30Olaf Beyersdorff, Leroy Chew, Judith Clymo and Meena Mahajan. Short Proofs in QBF Expansion
Wednesday, July 10th
09:00-10:30Session 6: Invited Talk ( chair: Inês Lynce )
09:00-10:30Carla Gomes. Computational Sustainability: Computing for a Better World
10:30-11:00Coffee break
11:00-12:30Session 7 ( chair: Jan Johannsen )
11:00-11:30Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider. Proof Complexity of Fragments of Long-Distance Q-Resolution[slides]
11:30-12:00Andrei Bulatov and Oleksii Omelchenko. Satisfiability Threshold for Power Law Random 2-SAT in Configuration Model
12:00-12:30Albert Atserias and Massimo Lauria. Circular ( Yet Sound) Proofs[slides]
14:00-15:30Session 8 ( chair: Markus Rabe )
14:00-14:30Nina Narodytska, Aditya Shrotri, Kuldeep S. Meel, Alexey Ignatiev and Joao Marques Silva. Assessing Heuristic Machine Learning Explanations with Model Counting
14:30-15:00Andy Shih, Adnan Darwiche and Arthur Choi. Verifying Binarized Neural Networks by Angluin-Style Learning
15:00-15:30Mate Soos, Raghav Kulkarni and Kuldeep S. Meel. CrystalBall: Gazing in the Black Box of SAT Solving
15:30-16:00Coffee break
16:00-16:40Session 9: Tool papers ( chair: Marijn Heule )
16:00-16:20Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar and Clark Barrett. DRAT-based Bit-Vector Proofs in CVC4
16:20-16:40Florian Lonsing and Uwe Egly. QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
16:40-17:40Session 10: SAT association general assembly
Thursday, July 11th
09:00-10:30Session 11: Invited talk ( chair: Mikoláš Janota )
09:00-10:30Josef Urban. Machine Learning in Automated and Interactive Theorem Proving
10:30-11:00Coffee break
11:00-12:30Session 12 ( chair: Stefan Szeider )
12:00-12:30Stefan Mengel and Romain Wallon. Revisiting Graph Width Measures for CNF-Encodings
11:30-12:00Akhil Dixit and Phokion Kolaitis. A SAT-based System for Consistent Query Answering
12:00-12:30Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett and Cesare Tinelli. Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
14:30-23:59Excursion and banquet
Friday, July 12th
09:30-10:30Session 13: Competitions results ( chair: Pascal Fontaine )
10:30-11:00Coffee break
11:00-12:30Session 14 ( chair: Olaf Beyersdorff )
11:00-11:30Florent Capelli. Knowledge compilation languages as proof systems[slides]
11:30-12:00Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider. Combining Resolution-Path Dependencies with Dependency Learning
11:00-11:30Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva and Sam Buss. DRMaxSAT with MaxHS: First Contact[slides]
14:00-15:30Session 15 ( chair: Kuldeep Meel )
14:00-14:30Randy Hickey and Fahiem Bacchus. Speeding Up Assumption-Based SAT
14:30-15:00Sima Jamali and David Mitchell. Simplifying CDCL Clause Database Reduction
15:00-15:30Sibylle Möhle and Armin Biere. Backing Backtracking