Marijn Heule | Computable Short Proofs | | Jul 11 11:00 |

Christoph Scholl and Ralf Wimmer | Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications | | |

Rahul Santhanam | Modelling SAT | | |

Rüdiger Ehlers and Francisco Palau Romero | Approximately Propagation Complete and Conflict Propagating Constraint Encodings | | Jul 09 14:00 |

Tobias Paxian, Sven Reimer and Bernd Becker | Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT | | Jul 09 14:30 |

Alexander Nadel | Solving MaxSAT with Bit-Vector Optimization | | Jul 09 15:00 |

Jan Elffers, Jesus Giráldez-Cru, Jakob Nordstrom and Marc Vinyals | Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers | | Jul 09 16:00 |

Jia Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li and Vijay Ganesh | Machine Learning-based Restart Policy for CDCL SAT Solvers | | Jul 09 16:30 |

Vadim Ryvchin and Alexander Nadel | Chronological Backtracking | | Jul 09 17:00 |

Sima Jamali and David Mitchell | Centrality-Based Improvements to CDCL Heuristics | | Jul 09 17:30 |

Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos | Fast Sampling of Perfectly Uniform Satisfying Assignments | | Jul 10 09:00 |

Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos | Fast and Flexible Probabilistic Model Counting | | Jul 10 09:30 |

Johannes K. Fichte, Markus Hecher, Michael Morak and Stefan Woltran | Exploiting Treewidth for Projected Model Counting and its Limits | | Jul 10 10:00 |

Mikolas Janota | Circuit-based Search Space Pruning in QBF | | Jul 10 14:00 |

Manuel Kauers and Martina Seidl | Symmetries for QBF | | Jul 10 14:30 |

Martin Suda and Bernhard Gleiss | Local Soundness for QBF Calculi | | Jul 10 15:00 |

Michael Lampis, Stefan Mengel and Valia Mitsou | QBF as an Alternative to Courcelle's Theorem | | Jul 10 16:00 |

Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider | Polynomial-Time Validation of QCDCL Certificates | | Jul 10 16:30 |

Tobias Friedrich and Ralf Rothenberger | Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT | | Jul 11 09:00 |

Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob Nordstrom | In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving | | Jul 11 09:30 |

Nicola Galesi, Navid Talebanfard and Jacobo Toran | Cops-Robber games and the resolution of Tseitin formulas | | Jul 11 10:00 |

Hoda Abbasizanjani and Oliver Kullmann | Minimal unsatisfiability and minimal strongly connected digraphs | | Jul 11 16:00 |

Ryan Berryhill, Alexander Ivrii and Andreas Veneris | Finding all Minimal Safe Inductive Sets | | Jul 11 16:30 |

Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav Bansal | Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition | | Jul 12 11:00 |

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani | Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization | | Jul 12 11:30 |

Sean Weaver, Hannah Roberts and Michael Smith | XORSAT Set Membership Filters | | Jul 12 12:00 |

Stepan Kochemazov and Oleg Zaikin | ALIAS: A Modular Tool for Finding Backdoors for SAT | | Jul 12 14:00 |

Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva | PySAT: A Python Toolkit for Prototyping with SAT Oracles | | Jul 12 14:30 |

Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjorner and Mooly Sagiv | Constrained Image Generation Using Binarized Neural Networks with Decision Procedures | | Jul 12 15:00 |