| Wednesday, July 5th |
|
|---|---|
| 09:15-09:30 |
Session 1: Opening Remarks (chair: Friedrich Slivovsky) |
| 09:30-10:50 |
Session 2: Contributed Talks 1 (chair: Oliver Kullmann) |
| 09:30-09:50 |
Neng-Fa Zhou, Ruiwei Wang and Roland Yap. A Comparison of SAT Encodings for Acyclicity of Directed Graphs |
| 09:50-10:20 |
Markus Kirchweger, Manfred Scheucher and Stefan Szeider. SAT-Based Generation of Planar Graphs |
| 10:20-10:50 |
Andrew Haberlandt, Harrison Green and Marijn Heule. Effective Auxiliary Variables via Structured Reencoding |
| 11:30-12:30 |
Session 3: Invited Talk 1 (chair: Meena Mahajan) |
| 11:30-12:30 |
Albert Atserias. Algorithmic Complexity of Certified Unsatisfiability |
| 14:00-15:20 |
Session 4: Contributed Talks 2 (chair: Jakob Nordstrom) |
| 14:00-14:30 |
Alexis de Colnet. Separating Incremental and Non-Incremental Bottom-Up Compilation |
| 14:30-14:50 |
Stefan Mengel. Bounds on BDD-Based Bucket Elimination |
| 14:50-15:20 |
Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova and Vijay Ganesh. Limits of CDCL Learning via Merge Resolution |
| 16:00-17:30 |
Session 5: Contributed Talks 3 (chair: Johannes Fichte) |
| 16:00-16:30 |
Olaf Beyersdorff, Tim Hoffmann and Luc Nicolas Spachmann. Proof Complexity of Propositional Model Counting |
| 16:30-17:00 |
Dror Fried, Alexander Nadel and Yogev Shalmon. AllSAT for Combinational Circuits |
| 17:00-17:30 |
Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani. On CNF Conversion for Disjoint SAT Enumeration |
| 17:45-19:00 |
Welcome Reception |
| Thursday, July 6th |
|
| 09:30-11:00 |
Session 6: Contributed Talks 4 (chair: Leroy Chew) |
| 09:30-10:00 |
Randal Bryant, Wojciech Nawrocki, Jeremy Avigad and Marijn Heule. Certified Knowledge Compilation with Application to Verified Model Counting |
| 10:00-10:30 |
Markus Kirchweger, Tomáš Peitl and Stefan Szeider. A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture |
| 10:30-11:00 |
Tereza Schwarzová, Jan Strejček and Juraj Major. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving |
| 11:30-12:45 |
Session 7: Awards Ceremony (chair: Olaf Beyersdorff) |
| 14:00-15:00 |
Session 8: Contributed Talks 5 (chair: Armin Biere) |
| 14:00-14:30 |
Anshujit Sharma, Matthew Burns and Michael Huang. Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT |
| 14:30-15:00 |
Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos and Kuldeep S. Meel. Explaining SAT Solving Using Causal Reasoning |
| 15:30-16:30 |
Session 9: Contributed Talks 6 (chair: Marijn Heule) |
| 15:30-16:00 |
Adrian Rebola Pardo. Even shorter proofs without new variables |
| 16:00-16:30 |
Markus Anders, Pascal Schweitzer and Mate Soos. Algorithms Transcending the SAT-Symmetry Interface |
| 17:00-19:00 |
Guided Tour / Excursion |
| 19:30-21:30 |
Social Dinner |
| Friday, July 7th |
|
| 09:30-11:00 |
Session 10: Contributed Talks 7 (chair: Marc Vinyals) |
| 09:30-10:00 |
Long-Hin Fung and Tony Tan. On the complexity of k-DQBF |
| 10:00-10:30 |
Ilario Bonacina, María-Luisa Bonet and Jordi Levy. Polynomial Calculus for MaxSAT |
| 10:30-11:00 |
Jacobo Torán and Florian Wörz. Cutting Planes Width and the Complexity of Graph Isomorphism Refutations |
| 11:30-12:30 |
Session 11: Invited Talk 2 (chair: Friedrich Slivovsky) |
| 11:30-12:30 |
Ryan Williams. Around the Fine-Grained Complexity of SAT |
| 14:00-15:20 |
Session 12: Contributed Talks 8 (chair: Daniel Le Berre) |
| 14:00-14:20 |
Alexander Nadel. Solving Huge Instances with Intel(R) SAT Solver |
| 14:20-14:40 |
Florian Pollitt, Mathias Fleury and Armin Biere. Faster LRAT Checking than Solving with CaDiCaL |
| 14:40-15:00 |
Armin Biere, Nils Froleyks and Wenxi Wang. CadiBack: Extracting Backbones with CaDiCaL |
| 15:00-15:20 |
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere. IPASIR-UP: User Propagators for CDCL |
| 15:50-17:20 |
Session 13: Competition Prizes (chair: Daniel La Berre) |
| 17:30-19:00 |
Session 14: Business Meeting |
| Saturday, July 8th |
|
| 09:30-11:20 |
Session 15: Contributed Talks 9 (chair: Luca Pulina) |
| 09:30-10:00 |
Junping Zhou, Jiaxin Liang, Minghao Yin and Bo He. LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem |
| 10:00-10:20 |
Pedro Orvalho, Vasco Manquinho and Ruben Martins. UpMax: User partitioning for MaxSAT |
| 10:20-10:50 |
George Katsirelos. An Analysis of Core-guided Maximum Satisfiability Solvers Using Linear Programming |
| 10:50-11:20 |
Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung and Vijay Ganesh. Learning Shorter Redundant Clauses in SDCL Using MaxSAT |
| 11:50-13:00 |
Session 16: Contributed Talks 10 (chair: Tomas Peitl) |
| 11:50-12:20 |
Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF Resolution: Further Insights |
| 12:20-12:40 |
Irfansha Shaik, Maximilian Heisinger, Martina Seidl and Jaco van de Pol. Validation of QBF Encodings with Winning Strategies |
| 12:40-13:00 |
Andreas Plank and Martina Seidl. QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas |