| Authors | Title | Paper | Talk |
|---|
| Marijn Heule | Computable Short Proofs |  | Jul 11 11:00 |
| Christoph Scholl and Ralf Wimmer | Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications | | |
| Rahul Santhanam | Modelling SAT | | |
| Rüdiger Ehlers and Francisco Palau Romero | Approximately Propagation Complete and Conflict Propagating Constraint Encodings | | Jul 09 14:00 |
| Tobias Paxian, Sven Reimer and Bernd Becker | Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT | | Jul 09 14:30 |
| Alexander Nadel | Solving MaxSAT with Bit-Vector Optimization | | Jul 09 15:00 |
| Jan Elffers, Jesus Giráldez-Cru, Jakob Nordstrom and Marc Vinyals | Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers | | Jul 09 16:00 |
| Jia Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li and Vijay Ganesh | Machine Learning-based Restart Policy for CDCL SAT Solvers | | Jul 09 16:30 |
| Vadim Ryvchin and Alexander Nadel | Chronological Backtracking | | Jul 09 17:00 |
| Sima Jamali and David Mitchell | Centrality-Based Improvements to CDCL Heuristics | | Jul 09 17:30 |
| Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos | Fast Sampling of Perfectly Uniform Satisfying Assignments | | Jul 10 09:00 |
| Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos | Fast and Flexible Probabilistic Model Counting | | Jul 10 09:30 |
| Johannes K. Fichte, Markus Hecher, Michael Morak and Stefan Woltran | Exploiting Treewidth for Projected Model Counting and its Limits | | Jul 10 10:00 |
| Mikolas Janota | Circuit-based Search Space Pruning in QBF | | Jul 10 14:00 |
| Manuel Kauers and Martina Seidl | Symmetries for QBF | | Jul 10 14:30 |
| Martin Suda and Bernhard Gleiss | Local Soundness for QBF Calculi | | Jul 10 15:00 |
| Michael Lampis, Stefan Mengel and Valia Mitsou | QBF as an Alternative to Courcelle's Theorem | | Jul 10 16:00 |
| Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider | Polynomial-Time Validation of QCDCL Certificates | | Jul 10 16:30 |
| Tobias Friedrich and Ralf Rothenberger | Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT | | Jul 11 09:00 |
| Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob Nordstrom | In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving | | Jul 11 09:30 |
| Nicola Galesi, Navid Talebanfard and Jacobo Toran | Cops-Robber games and the resolution of Tseitin formulas | | Jul 11 10:00 |
| Hoda Abbasizanjani and Oliver Kullmann | Minimal unsatisfiability and minimal strongly connected digraphs | | Jul 11 16:00 |
| Ryan Berryhill, Alexander Ivrii and Andreas Veneris | Finding all Minimal Safe Inductive Sets | | Jul 11 16:30 |
| Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav Bansal | Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition | | Jul 12 11:00 |
| Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani | Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization | | Jul 12 11:30 |
| Sean Weaver, Hannah Roberts and Michael Smith | XORSAT Set Membership Filters | | Jul 12 12:00 |
| Stepan Kochemazov and Oleg Zaikin | ALIAS: A Modular Tool for Finding Backdoors for SAT | | Jul 12 14:00 |
| Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva | PySAT: A Python Toolkit for Prototyping with SAT Oracles | | Jul 12 14:30 |
| Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjorner and Mooly Sagiv | Constrained Image Generation Using Binarized Neural Networks with Decision Procedures | | Jul 12 15:00 |