Site Overlay

Program

Due to the current circumstances regarding the COVID-19 pandemic outbreak, the conference program chairs have decided to hold SAT 2020 as a fully virtual conference which will be held from 3 to 10 July 2020.

 

Program at a glance:

SAT 2020 Program

Time

Monday, July 6th

Tuesday, July 7th

Wednesday, July 8th

15:45-16:00Welcome
16:00-17:00Invited Talk: Aarti GuptaInvited Talk: Georg GottlobQ&A Session 7
17:00-17:35 Q&A Session 1Q&A Session 4Q&A Session 8
17:40-18:20Q&A Session 2Q&A Session 5Awards(10 min)
Competition
Closing (5 min)
18:25-19:10Q&A Session 3Q&A Session 6
19:15-20:00Welcome ReceptionBusiness 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 6th

Session Chair: Marijn Heule   

17:00 – 17:07 Stepan Kochemazov: Improving Implementation of SAT Competitions 2017-2019 Winners

Video | Slides

17:28 – 17:35 Maximilian Heisinger, Mathias Fleury and Armin Biere: Distributed Cube and Conquer with Paracooba

Video | Slides

 

Time

Q&A Session 2 (QBF) – Monday, July 6th

Session Chair: Florian Lonsing

17:40 – 17:50 Olaf Beyersdorff, Joshua Blinkhorn and Tomáš Peitl: Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths

Video | Slides

17:50 – 18:00 Ankit Shukla, Friedrich Slivovsky and Stefan Szeider: Short Q-Resolution Proofs with Homomorphisms

Video | Slides

18:00 – 18:10 Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher and Florian Zuleger: Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness

Video | Slides

18:10 – 18:20 Valentin Mayer-Eichberger and Abdallah Saffidine: Positional Games and QBF: The Corrective Encoding

Video | Slides

 

Time

Q&A Session 3 (PB, SMT) – Monday, July 6th

Session 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

Video | Slides

18:35 – 18:42 Daniel Le Berre, Pierre Marquis and Romain Wallon: On Weakening Strategies for PB Solvers

Video | Slides

18:49 – 18:59 Thomas Seed, Andy King and Neil Evans: Reducing Bit-Vector Polynomials to SAT using Groebner Bases

Video | Slides

19:00 – 19:10 Martin Jonáš and Jan Strejček: Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Video | Slides

 

Time

Q&A Session 4 – Tuesday, July 7th

Session Chair: Fahiem Bacchus

17:00 – 17:07 Carlos Mencía and Joao Marques-Silva: Reasoning About Strong Inconsistency in ASP

Video | Slides

17:17 – 17:24 Friedrich Slivovsky and Stefan Szeider: A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth

Video | Slides

17:25 – 17:35 Durgesh Agrawal, Bhavishya and Kuldeep S. Meel: On the Sparsity of XORs in Approximate Model Counting

Video | Slides

 

Time

Q&A Session 5 (Proofs) – Tuesday, July 7th

Session Chair: Olaf Beyersdorff

17:40 – 17:50 Maria Luisa Bonet and Jordi Levy: Equivalence Between Systems Stronger Than Resolution

Video | Slides

17:50 – 18:00 Nathan Mull, Shuo Pang and Alexander Razborov: On CDCL-based Proof Systems with the Ordered Decision Strategy

Video | Slides

18:00 – 18:10 Marc Vinyals, Jan Elffers, Jan Johannsen and Jakob Nordstrom: Simplified and Improved Separations Between Regular and General Resolution by Lifting

Video | Slides

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

Video | Slides

 

Time

Q&A Session 6 (Applications) – Tuesday, July 7th

Session Chair: Kuldeep Meel

18:25 – 18:35 Matthew Anderson, Zongliang Ji and Anthony Xu: Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles

Video | Slides

18:35 – 18:42 Leroy Chew and Marijn Heule: Sorting Parity Encodings by Reusing Variables

Video | Slides

18:49 – 18:59 Mikolas Janota and António Morgado: SAT-based Encodings for Optimal Decision Trees with Explicit Paths

Video | Slides

19:00 – 19:10 Emre Yolcu, Xinyu Wu and Marijn Heule: Mycielski graphs and PR proofs

Video | Slides

 

Time

Q&A Session 7 (SAT Solving 2) – Wednesday, July 8th

Session Chair: Laurent Simon

16:00 – 16:10 Nick Feng and Fahiem Bacchus: Clause size reduction with all-UIP Learning

Video | Slides

16:20 – 16:27 Sibylle Möhle, Roberto Sebastiani and Armin Biere: Four Flavors of Entailment

Video | Slides

16:27 – 16:37 Arijit Shaw and Kuldeep S. Meel: Designing New Phase Selection Heuristics

Video | Slides

16:37 – 16:47 Jan-Hendrik Lorenz and Florian Wörz: On the Effect of Learned Clauses on Stochastic Local Search

Video | Slides

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

Video | Slides

 

Time

Q&A Session 8 (MaxSAT) – Wednesday, July 8th

Session Chair: Joao Marques-Silva

17:10 – 17:20 Jeremias Berg, Fahiem Bacchus and Alex Poole: Abstract Cores in Implicit Hitting Set MaxSat Solving

Video | Slides

17:20 – 17:30 Yuval Filmus, Meena Mahajan, Gaurav Sood and Marc Vinyals: MaxSAT Resolution and SubCube Sums

Video | Slides

17:30 – 17:37 Milan Ceska, Jiri Matyas, Vojtech Mrazek and Tomas Vojnar: Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits

Video | Slides

 

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