SAT PROGRAM
Days: Tuesday, August 2nd Wednesday, August 3rd Thursday, August 4th Friday, August 5th
Tuesday, August 2nd
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 44G: QBF-1
Chair:
| 09:00 | Classes of Hard Formulas for QBF Resolution (abstract)   PRESENTER: Olaf Beyersdorff |
| 09:30 | Should decisions in QCDCL follow prefix order? (abstract) PRESENTER: Benjamin Böhm |
| 10:00 | Changing Partitions in Rectangle Decision Lists (abstract) |
10:30-11:00Coffee Break
11:10-12:10 Session 48: Keynote
Chair:
Location: Churchill Auditorium
| 11:10 | Information Structures for Privacy and Fairness (abstract) |
12:10-12:40 Session 49C: Application of SAT to Quantum circuits
Chair:
| 12:10 | Towards a SAT Encoding for Quantum Circuits (abstract) PRESENTER: Robert Wille |
12:30-14:00Lunch Break
Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).
14:00-15:30 Session 50H: SAT
Chair:
| 14:00 | SAT Preprocessors and Symmetry (abstract) |
| 14:30 | A Comprehensive Study of k-Portfolios of Recent SAT Solvers (abstract) PRESENTER: Jakob Bach |
| 15:00 | SAT-based Leximax Optimisation Algorithms (abstract) PRESENTER: Mikolas Janota |
15:30-16:00Coffee Break
16:00-17:30 Session 54H: MaxSAT
Chair:
| 16:00 | MaxSAT-Based Bi-Objective Boolean Optimization (abstract) PRESENTER: Christoph Jabs |
| 16:30 | Incremental Maximum Satisfiability (abstract) PRESENTER: Andreas Niskanen |
| 17:00 | Analysis of Core-Guided MaxSAT Using Cores and Correction Sets (abstract) PRESENTER: Nina Narodytska |
17:30-18:30 Session 55: Logic Lounge
Chair:
Location: Churchill Auditorium
| 17:30 | Thinking Fast and Slow in AI (abstract) |
Wednesday, August 3rd
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 56F: QBF-2 + Stochastic Boolean Satisfiability
Chair:
| 09:00 | Quantified CDCL with Universal Resolution (abstract) |
| 09:30 | Relating existing powerful proof systems for QBF (abstract) PRESENTER: Leroy Chew |
| 10:00 | Quantifier Elimination in Stochastic Boolean Satisfiability (abstract) PRESENTER: Hao-Ren Wang |
10:30-11:00Coffee Break
11:00-12:30 Session 58H: Applications + pragmatics
Chair:
| 11:00 | A SAT Attack on Rota's Basis Conjecture (abstract) PRESENTER: Markus Kirchweger |
| 11:30 | The packing chromatic number of the infinite square grid is at least 14 (abstract) PRESENTER: Bernardo Subercaseaux |
| 12:00 | Migrating Solver State (abstract) PRESENTER: Benjamin Kiesl |
12:30-14:00Lunch Break
Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).
14:00-15:30 Session 59G: Theory
Chair:
| 14:00 | Tight Bounds for Tseitin Formulas (abstract) PRESENTER: Petr Smirnov |
| 14:30 | A generalization of the Satisfiability Coding Lemma and its applications (abstract) PRESENTER: Harry Sha |
| 15:00 | On the Parallel Parameterized Complexity of MaxSAT Variants (abstract) PRESENTER: Max Bannach |
15:30-16:00Coffee Break
16:00-17:30 Session 61H: Model Counting
Chair:
| 16:00 | Proofs for Propositional Model Counting (abstract) PRESENTER: Markus Hecher |
| 16:30 | A New Exact Solver for (Weighted) Max#SAT (abstract) PRESENTER: Marie Miceli |
| 17:00 | Weighted Model Counting with Twin-Width (abstract) PRESENTER: Stefan Szeider |
18:30-20:30 Walking tour (at Haifa)
pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)
Thursday, August 4th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 63H: 25 years of SAT
25-years of SAT
Chair:
| 09:00 | 25 years of SAT: Conflict-Driven SAT Solving (abstract) |
| 09:24 | 25 years of SAT: Maximum Satisfiability for Real-World Optimization (abstract) |
| 09:48 | 25 years of SAT: Trusting SAT Solvers (abstract) |
| 10:12 | 25 years of SAT: Proof complexity and SAT solving (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 65G: Machine-Learning for SAT/SMT
Chair:
| 11:00 | 25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren (abstract) |
| 11:30 | On the performance of deep generative models of realistic SAT instances (abstract) PRESENTER: Jesús Giráldez-Cru |
| 12:00 | Towards Learning Quantifier Instantiation in SMT (abstract) PRESENTER: Mikolas Janota |
12:30-14:00Lunch Break
Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).
14:00-15:30 Session 67H: SAT / PBS
Chair:
| 14:00 | Introducing Intel(R) SAT Solver (abstract) |
| 14:30 | Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization (abstract) PRESENTER: Matti Järvisalo |
| 15:00 | Certified CNF Translations for Pseudo-Boolean Solving (abstract) PRESENTER: Andy Oertel |
15:30-16:00Coffee Break
16:00-17:00 Session 70: Plenary
Chair:
Location: Churchill Auditorium
| 16:00 | Complexity Measures for Reactive Systems (abstract) |
Friday, August 5th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
10:30-11:00Coffee Break
11:00-12:30 Session 76I: Bryant Discoveries Day (BDD) event + Tool papers
Chair:
| 11:00 | (BDD event) |
| 11:30 | Pedant: A Certifying DQBF Solver (abstract) PRESENTER: Franz-Xaver Reichl |
| 11:50 | QBF Programming with the Modeling Language Bule (abstract) PRESENTER: Abdallah Saffidine |
| 12:10 | OptiLog v2: Model, Solve, Tune And Run (abstract) PRESENTER: Josep Alos |
12:30-14:00Lunch Break
Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).
14:00-15:30 Session 78F: QBF + Awards / competitions
Chair:
| 14:00 | QBF Merge Resolution is powerful but unnatural (abstract) PRESENTER: Gaurav Sood |
| 14:30 | Awards / Competition Results - I (with Live Broadcast) (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 81E: Awards / Competitions
Awards / Competitions
Chair:
| 16:00 | Awards and Competition - II (with Live Broadcast) (abstract) |