Program
Go to: Wednesday 7 | Thursday 8 | Friday 9
Wednesday, July 7th
15:00-15:40 Session 1: Welcome and Best Papers
15:00 - 15:10 | Welcome |
15:10 - 15:25 | Shaowei Cai and Xindi Zhang. Deep Cooperation of CDCL and Local Search for SAT Slides | Presentation |
15:25 - 15:40 | Alexis de Colnet and Stefan Mengel. Characterizing Tseitin-formulas with short regular resolution refutations Slides | Presentation |
15:50-16:30 Session 2: Solving problems with SAT
15:50-16:00 | Alexey Ignatiev and Joao Marques-Silva. SAT-Based Rigorous Explanations for Decision Lists Slides | Presentation |
16:00-16:10 | Monika Trimoska, Gilles Dequen and Sorina Ionica. Logical cryptanalysis with WDSat Slides | Presentation |
16:10-16:20 | Marijn Heule. Chinese Remainder Encoding for Hamiltonian Cycles Slides | Presentation |
16:20-16:30 | Jiwei Jin, Yiqi Lv, Cunjing Ge, Feifei Ma and Jian Zhang. Investigating the Existence of Costas Latin Square via Satisfiability Testing Slides | Presentation |
16:30-16:50 Coffee break
16:50-18:00 Invited talk by Adnan Darwiche. The Knowledge Compilation Quest: How Far Have We Gone?
18:10-19:00 Session 3: Tools
18:10-18:20 | Norbert Hundeshagen, Martin Lange and Georg Siebert. DiMo – Discrete Modelling Using Propositional Logic Slides | Presentation |
18:20-18:30 | Carlos Ansótegui, Jesús Ojeda, Antonio Pacheco, Josep Pon, Josep M. Salvia and Eduard Torres. OptiLog: A Framework for SAT-based Systems Slides | Presentation |
18:30-18:40 | Olaf Beyersdorff, Luca Pulina, Martina Seidl and Ankit Shukla. QBFFam: A Tool for Generating QBF Families from Proof Complexity Slides | Presentation |
18:40-18:50 | Matthieu Py, Mohamed Sami Cherif and Djamal Habet. A Proof Builder for Max-SAT Slides | Presentation |
18:50-19:00 | Miki Hermann and Gernot Salzer. MCP: Capturing Big Data by Satisfiability Slides | Presentation |
19:10-20:00 Session 4: QBF
19:10-19:20 | Franz-Xaver Reichl, Friedrich Slivovsky and Stefan Szeider. Certified DQBF Solving by Definition Extraction Slides | Presentation |
19:20-19:30 | Benjamin Böhm and Olaf Beyersdorff. Lower Bounds for QCDCL via Formula Gauge Slides | Presentation |
19:30-19:40 | Stefan Mengel and Friedrich Slivovsky. Proof Complexity of Symbolic QBF Reasoning Slides | Presentation |
19:40-19:50 | Joshua Blinkhorn, Tomáš Peitl and Friedrich Slivovsky. Davis and Putnam Meet Henkin: Solving DQBF with Resolution Slides | Presentation |
19:50-20:00 | Leroy Chew. Hardness and Optimality in QBF Proof Systems Modulo NP Slides | Presentation |
Thursday, July 8th
15:00-15:50 Session 5: PB and Model Counting
15:00-15:10 | Daniel Le Berre and Romain Wallon. On Dedicated CDCL Strategies for PB Solvers Slides | Presentation |
15:10-15:20 | Zhendong Lei, Shaowei Cai, Chuan Luo and Holger Hoos. Efficient Local Search for Pseudo Boolean Optimization Slides | Presentation |
15:20-15:30 | Martin Mariusz Lester. Scheduling Reach Mahjong Tournaments using Pseudoboolean Constraints Slides | Presentation |
15:30-15:40 | Jeffrey M. Dudek, Vu H. N. Phan and Moshe Y. Vardi. ProCount: Weighted Projected Model Counting with Graded Project-Join Trees Slides | Presentation |
15:40-15:50 | Paulius Dilkas and Vaishak Belle. Weighted Model Counting Without Parameter Variables Slides | Presentation |
16:00-16:50 Session 6: Tools and solvers
16:00-16:10 | Carlos Ansótegui, Josep Pon, Meinolf Sellmann and Kevin Tierney. PyDGGA: Distributed GGA for Automatic Configuration Slides | Presentation |
16:10-16:20 | Junqiang Peng and Mingyu Xiao. A Fast Algorithm for SAT in Terms of Formula Length Slides | Presentation |
16:20-16:30 | Juraj Síč and Jan Strejček. DQBDD: An Efficient BDD-Based DQBF Solver Slides | Presentation |
16:30-16:40 | Norbert Manthey. The SAT solver MergeSat Slides | Presentation |
16:40-16:50 | Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli and Clark Barrett. Smt-Switch: a Solver-agnostic C++ API for SMT Solving Slides | Presentation |
16:50-17:10 Coffee break
17:10-18:00 Session 7: SAT: theory and practice
17:10-17:20 | Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Antonina Kolokolova, Noah Fleming, Alice Mu and Vijay Ganesh. On the Hierarchical Community Structure of Practical SAT Formulas Slides | Presentation |
17:20-17:30 | Tobias Friedrich, Frank Neumann, Ralf Rothenberger and Andrew Sutton. Solving Non-Uniform Planted and Filtered Random SAT Formulas Greedily Slides | Presentation |
17:30-17:40 | Oliver Kullmann and Oleg Zaikin. Projection heuristics for binary branchings between sum and product Slides | Presentation |
17:40-17:50 | Pei Huang, Rundong Li, Minghao Liu, Feifei Ma and Jian Zhang. Efficient SAT-based Minimal Model Generation Methods for Modal Logic S5 Slides | Presentation |
17:50-18:00 | Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen and Sanjit A. Seshia. MedleySolver: Online SMT Algorithm Selection Slides | Presentation |
18:00-18:50 Competitive events: EDA Challenge and MaxSAT Evaluation
19:00-20:30 SAT Association: Business meeting
Friday, July 9th
15:00-16:00 Session 8: SAT Solving
15:00-15:10 | Stepan Kochemazov, Alexey Ignatiev and Joao Marques-Silva. Assessing Progress in SAT Solvers Through the Lens of Incremental SAT Slides | Presentation |
15:10-15:20 | Mathias Fleury and Armin Biere. Efficient All-UIP Learned Clause Minimization Slides | Presentation |
15:20-15:30 | Henrik Cao. Hash-based preprocessing and inprocessing techniques in SAT solvers Slides | Presentation |
15:30-15:40 | Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn Heule and Armin Biere. XOR Local Search Slides | Presentation |
15:40-15:50 | Dominik Schreiber and Peter Sanders. Scalable SAT Solving in the Cloud Slides | Presentation |
15:50-16:00 | Nicolas Prévot, Mate Soos and Kuldeep S. Meel. Leveraging GPUs for Effective Clause Sharing in Parallel SAT Solving Slides | Presentation |