Program

PROGRAM

Days: Wednesday, July 5th Thursday, July 6th Friday, July 7th Saturday, July 8th

Wednesday, July 5th

View this program: with abstracts session overview talk overview

09:15-09:30 Session 1: Opening Remarks

Chair:

Friedrich Slivovsky

09:30-10:50 Session 2: Contributed Talks 1

Chair:

Oliver Kullmann

09:30	Neng-Fa Zhou, Ruiwei Wang and Roland Yap A Comparison of SAT Encodings for Acyclicity of Directed Graphs (abstract)
09:50	Markus Kirchweger, Manfred Scheucher and Stefan Szeider SAT-Based Generation of Planar Graphs (abstract) PRESENTER: Markus Kirchweger
10:20	Andrew Haberlandt, Harrison Green and Marijn Heule Effective Auxiliary Variables via Structured Reencoding (abstract)

11:30-12:30 Session 3: Invited Talk 1

Chair:

Meena Mahajan

11:30

Albert Atserias

Algorithmic Complexity of Certified Unsatisfiability

14:00-15:20 Session 4: Contributed Talks 2

Chair:

Jakob Nordstrom

14:00	Alexis de Colnet Separating Incremental and Non-Incremental Bottom-Up Compilation (abstract)
14:30	Stefan Mengel Bounds on BDD-Based Bucket Elimination (abstract)
14:50	Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova and Vijay Ganesh Limits of CDCL Learning via Merge Resolution (abstract) PRESENTER: Marc Vinyals

16:00-17:30 Session 5: Contributed Talks 3

Chair:

Johannes Fichte

16:00	Olaf Beyersdorff, Tim Hoffmann and Luc Nicolas Spachmann Proof Complexity of Propositional Model Counting (abstract) PRESENTER: Tim Hoffmann
16:30	Dror Fried, Alexander Nadel and Yogev Shalmon AllSAT for Combinational Circuits (abstract) PRESENTER: Yogev Shalmon
17:00	Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani On CNF Conversion for Disjoint SAT Enumeration (abstract) PRESENTER: Gabriele Masina

17:45-19:00 Welcome Reception

Thursday, July 6th

View this program: with abstracts session overview talk overview

09:30-11:00 Session 6: Contributed Talks 4

Chair:

Leroy Chew

09:30	Randal Bryant, Wojciech Nawrocki, Jeremy Avigad and Marijn Heule Certified Knowledge Compilation with Application to Verified Model Counting (abstract)
10:00	Markus Kirchweger, Tomáš Peitl and Stefan Szeider A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture (abstract) PRESENTER: Tomáš Peitl
10:30	Tereza Schwarzová, Jan Strejček and Juraj Major Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving (abstract) PRESENTER: Tereza Schwarzová

11:30-12:45 Session 7: Awards Ceremony

Chair:

Olaf Beyersdorff

14:00-15:00 Session 8: Contributed Talks 5

Chair:

Armin Biere

14:00	Anshujit Sharma, Matthew Burns and Michael Huang Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT (abstract) PRESENTER: Matthew Burns
14:30	Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos and Kuldeep S. Meel Explaining SAT Solving Using Causal Reasoning (abstract)

15:30-16:30 Session 9: Contributed Talks 6

Chair:

Marijn Heule

15:30	Adrian Rebola Pardo Even shorter proofs without new variables (abstract)
16:00	Markus Anders, Pascal Schweitzer and Mate Soos Algorithms Transcending the SAT-Symmetry Interface (abstract) PRESENTER: Markus Anders

17:00-19:00 Guided Tour / Excursion

19:30-21:30 Social Dinner

Friday, July 7th

View this program: with abstracts session overview talk overview

09:30-11:00 Session 10: Contributed Talks 7

Chair:

Marc Vinyals

09:30	Long-Hin Fung and Tony Tan On the complexity of k-DQBF (abstract)
10:00	Ilario Bonacina, María-Luisa Bonet and Jordi Levy Polynomial Calculus for MaxSAT (abstract)
10:30	Jacobo Torán and Florian Wörz Cutting Planes Width and the Complexity of Graph Isomorphism Refutations (abstract)

11:30-12:30 Session 11: Invited Talk 2

Chair:

Friedrich Slivovsky

11:30

Ryan Williams

Around the Fine-Grained Complexity of SAT

14:00-15:20 Session 12: Contributed Talks 8

Chair:

Daniel Le Berre

14:00	Alexander Nadel Solving Huge Instances with Intel(R) SAT Solver (abstract)
14:20	Florian Pollitt, Mathias Fleury and Armin Biere Faster LRAT Checking than Solving with CaDiCaL (abstract)
14:40	Armin Biere, Nils Froleyks and Wenxi Wang CadiBack: Extracting Backbones with CaDiCaL (abstract)
15:00	Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere IPASIR-UP: User Propagators for CDCL (abstract) PRESENTER: Katalin Fazekas

15:50-17:20 Session 13: Competition Prizes

Chair:

Daniel Le Berre

17:30-19:00 Session 14: Business Meeting

Saturday, July 8th

View this program: with abstracts session overview talk overview

09:30-11:20 Session 15: Contributed Talks 9

Chair:

Luca Pulina

09:30	Junping Zhou, Jiaxin Liang, Minghao Yin and Bo He LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem (abstract)
10:00	Pedro Orvalho, Vasco Manquinho and Ruben Martins UpMax: User partitioning for MaxSAT (abstract) PRESENTER: Pedro Orvalho
10:20	George Katsirelos An Analysis of Core-guided Maximum Satisfiability Solvers Using Linear Programming (abstract)
10:50	Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung and Vijay Ganesh Learning Shorter Redundant Clauses in SDCL Using MaxSAT (abstract) PRESENTER: Albert Oliveras

11:50-13:00 Session 16: Contributed Talks 10

Chair:

Tomáš Peitl

11:50	Benjamin Böhm and Olaf Beyersdorff QCDCL vs QBF Resolution: Further Insights (abstract)
12:20	Irfansha Shaik, Maximilian Heisinger, Martina Seidl and Jaco van de Pol Validation of QBF Encodings with Winning Strategies (abstract)
12:40	Andreas Plank and Martina Seidl QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas (abstract)