Site Overlay


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.


IMPORTANT! Shortly after you have registered, you will get an invitation to a Google group where all important information regarding conference participation is provided. If you cannot access it, write an email to

Program at a glance:

SAT 2020 Program


Monday, July 6th

Tuesday, July 7th

Wednesday, July 8th

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)
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

Hypergraph Transversals, Monotone Boolean Formula Dualization, and SAT 

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

With a little help from structured friends

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.


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
17:07 – 17:17 Hidetomo Nabeshima and Katsumi Inoue: Reproducible Efficient Parallel SAT Solving
17:17 – 17:27 Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon and Vijay Ganesh: Community and LBD-based Clause Sharing Policy for Parallel SAT Solving
17:28 – 17:35 Maximilian Heisinger, Mathias Fleury and Armin Biere: Distributed Cube and Conquer with Paracooba



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
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



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
18:35 – 18:42 Daniel Le Berre, Pierre Marquis and Romain Wallon: On Weakening Strategies for PB Solvers
18:42 – 18:49 Alexis de Colnet: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
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



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
17:07 – 17:17 Markus Hecher, Patrick Thier and Stefan Woltran: Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology
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



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
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



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
18:35 – 18:42 Leroy Chew and Marijn Heule: Sorting Parity Encodings by Reusing Variables
18:42 – 18:49 Rüdiger Ehlers, Kai Treutler and Volker Wesling: SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing
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



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
16:10 – 16:20 Randy Hickey and Fahiem Bacchus: Trail Saving on Backtrack
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



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

Session Chair: Joao Marques-Silva

17:00 – 17:10 Javier Larrosa and Emma Rollon: Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
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




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



  • Best Paper Award
  • Best Student Paper Award
  • Best Presentation Award