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