Program at a glance:
- Pragmatics of SAT (POS), July 3rd, 2020
- SAT conference, July 6th-8th, 2020
- Model Counting, July 9th, 2020
- QBF Workshop, July 10th, 2020
SAT 2020 Program
Time | Monday, July 6th | Tuesday, July 7th | Wednesday, July 8th |
|---|---|---|---|
| 15:45-16:00 | Welcome | ||
| 16:00-17:00 | Invited Talk: Aarti Gupta | Invited Talk: Georg Gottlob | Q&A Session 7 |
| 17:00-17:35 | Q&A Session 1 | Q&A Session 4 | Q&A Session 8 |
| 17:40-18:20 | Q&A Session 2 | Q&A Session 5 | Awards(10 min) Competition Closing (5 min) |
| 18:25-19:10 | Q&A Session 3 | Q&A Session 6 | |
| 19:15-20:00 | Welcome Reception | Business Meeting |
* Times are Central European Summer Time (CEST)
Invited Speakers
Georg Gottlob, University of Oxford and TU Wien
Session Chair: Stefan Szeider
Title: Hypergraph Transversals, Monotone Boolean Formula Dualization, and SAT (Slide)
Abstract: Hypergraph Transversals have been studied in Mathematics for a long time. Generating minimal transversals of a hypergraph is equivalent to monotone Boolean DNF dualization, which, in turn, is equivalent to restricted versions of SAT. These important problems have many applications in Computer Science, for instance, in data mining. The complexity of checking whether two hypergraphs are dual to each other has been open for about 40 years. I will give an overview of various applications and equivalent formulations, and of some algorithms and complexity bounds for this mysterious problem.
Aarti Gupta, Princeton University, US
Session Chair: Armin Biere
Title: With a little help from structured friends (Slide: Part 1 – Part 2)
Abstract: SAT and SMT solvers have enabled tremendous advances in automated verification and synthesis in a wide range of application domains. However, to extract maximum mileage, it is often helpful to suitably formulate the verification problem or supplement the solvers with other techniques to bridge the gap between satisfiability on one hand and verification/synthesis on the other. In this talk, I will describe some techniques that leverage the structure of the underlying models to further enhance the capabilities of SAT/SMT-based verification. I will show successful instances from the domains of computer networks, hardware designs, and theorem-proving.
Time |
Session 1 (SAT Solving 1) – Monday, July 6thSession Chair: Marijn Heule
|
| 17:00 – 17:07 | Stepan Kochemazov: Improving Implementation of SAT Competitions 2017-2019 Winners |
| 17:28 – 17:35 | Maximilian Heisinger, Mathias Fleury and Armin Biere: Distributed Cube and Conquer with Paracooba |
Time |
Q&A Session 2 (QBF) – Monday, July 6thSession Chair: Florian Lonsing
|
| 17:40 – 17:50 | Olaf Beyersdorff, Joshua Blinkhorn and Tomáš Peitl: Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths |
| 17:50 – 18:00 | Ankit Shukla, Friedrich Slivovsky and Stefan Szeider: Short Q-Resolution Proofs with Homomorphisms |
| 18:00 – 18:10 | Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher and Florian Zuleger: Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness |
| 18:10 – 18:20 | Valentin Mayer-Eichberger and Abdallah Saffidine: Positional Games and QBF: The Corrective Encoding |
Time |
Q&A Session 3 (PB, SMT) – Monday, July 6thSession Chair: Roberto Sebastiani
|
| 18:25 – 18:35 | Michał Karpiński and Marek Piotrów: Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks |
| 18:35 – 18:42 | Daniel Le Berre, Pierre Marquis and Romain Wallon: On Weakening Strategies for PB Solvers |
| 18:49 – 18:59 | Thomas Seed, Andy King and Neil Evans: Reducing Bit-Vector Polynomials to SAT using Groebner Bases |
| 19:00 – 19:10 | Martin Jonáš and Jan Strejček: Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions |
Time |
Q&A Session 4 – Tuesday, July 7thSession Chair: Fahiem Bacchus
|
| 17:00 – 17:07 | Carlos Mencía and Joao Marques-Silva: Reasoning About Strong Inconsistency in ASP |
| 17:17 – 17:24 | Friedrich Slivovsky and Stefan Szeider: A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth |
| 17:25 – 17:35 | Durgesh Agrawal, Bhavishya and Kuldeep S. Meel: On the Sparsity of XORs in Approximate Model Counting |
Time |
Q&A Session 5 (Proofs) – Tuesday, July 7thSession Chair: Olaf Beyersdorff
|
| 17:40 – 17:50 | Maria Luisa Bonet and Jordi Levy: Equivalence Between Systems Stronger Than Resolution |
| 17:50 – 18:00 | Nathan Mull, Shuo Pang and Alexander Razborov: On CDCL-based Proof Systems with the Ordered Decision Strategy |
| 18:00 – 18:10 | Marc Vinyals, Jan Elffers, Jan Johannsen and Jakob Nordstrom: Simplified and Improved Separations Between Regular and General Resolution by Lifting |
| 18:10 – 18:20 | Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi and Vijay Ganesh: Towards a Complexity-theoretic Understanding of Restarts in SAT solvers |
Time |
Q&A Session 6 (Applications) – Tuesday, July 7thSession Chair: Kuldeep Meel
|
| 18:25 – 18:35 | Matthew Anderson, Zongliang Ji and Anthony Xu: Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles |
| 18:35 – 18:42 | Leroy Chew and Marijn Heule: Sorting Parity Encodings by Reusing Variables |
| 18:49 – 18:59 | Mikolas Janota and António Morgado: SAT-based Encodings for Optimal Decision Trees with Explicit Paths |
| 19:00 – 19:10 | Emre Yolcu, Xinyu Wu and Marijn Heule: Mycielski graphs and PR proofs |
Time |
Q&A Session 7 (SAT Solving 2) – Wednesday, July 8thSession Chair: Laurent Simon
|
| 16:00 – 16:10 | Nick Feng and Fahiem Bacchus: Clause size reduction with all-UIP Learning |
| 16:20 – 16:27 | Sibylle Möhle, Roberto Sebastiani and Armin Biere: Four Flavors of Entailment |
| 16:27 – 16:37 | Arijit Shaw and Kuldeep S. Meel: Designing New Phase Selection Heuristics |
| 16:37 – 16:47 | Jan-Hendrik Lorenz and Florian Wörz: On the Effect of Learned Clauses on Stochastic Local Search |
| 16:45 – 16:52 | Gilles Audemard, Loïc Paulevé and Laurent Simon: SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers |
Time |
Q&A Session 8 (MaxSAT) – Wednesday, July 8thSession Chair: Joao Marques-Silva
|
| 17:10 – 17:20 | Jeremias Berg, Fahiem Bacchus and Alex Poole: Abstract Cores in Implicit Hitting Set MaxSat Solving |
| 17:20 – 17:30 | Yuval Filmus, Meena Mahajan, Gaurav Sood and Marc Vinyals: MaxSAT Resolution and SubCube Sums |
| 17:30 – 17:37 | Milan Ceska, Jiri Matyas, Vojtech Mrazek and Tomas Vojnar: Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits |
Competition
Session chair: Daniel Leberre
| Time | Competition |
| 18:05-18:25 | Model Counting Competition |
| 18:25-18:45 | MaxSAT Evaluation |
| 18:45-19:05 | QBFEval |
| 19:05-19:25 | SAT Competition |
Awards
- Best Paper Award: Jeremias Berg, Fahiem Bacchus and Alex Poole: Abstract Cores in Implicit Hitting Set MaxSat Solving
- Best Student Paper Award: Emre Yolcu, Xinyu Wu and Marijn Heule: Mycielski graphs and PR proofs
- Best Presentation Award: Maximilian Heisinger, Mathias Fleury and Armin Biere: Distributed Cube and Conquer with Paracooba