Accepted Papers

  • Martin Suda and Bernhard Gleiss: Local Soundness for QBF Calculi
  • Alexander Nadel: Solving MaxSAT with Bit-Vector Optimization
  • Sean Weaver, Hannah Roberts and Michael Smith: XORSAT Set Membership Filters
  • Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani: Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
  • Ryan Berryhill, Alexander Ivrii and Andreas Veneris: Finding all Minimal Safe Inductive Sets
  • Manuel Kauers and Martina Seidl: Symmetries for QBF
  • Nicola Galesi, Navid Talebanfard and Jacobo Torán: Cops-Robber games and the resolution of Tseitin formulas
  • Hoda Abbasizanjani and Oliver Kullmann: Minimal unsatisfiability and minimal strongly connected digraphs
  • Sima Jamali and David Mitchell: Centrality-Based Improvements to CDCL Heuristics
  • Johannes K. Fichte, Markus Hecher, Michael Morak and Stefan Woltran: Exploiting Treewidth for Projected Model Counting and its Limits
  • Vadim Ryvchin and Alexander Nadel: Chronological Backtracking
  • Tobias Paxian, Sven Reimer and Bernd Becker: Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
  • Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob Nordström: In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
  • Mikolas Janota: Circuit-based Search Space Pruning in QBF
  • Ruediger Ehlers and Francisco Palau-Romero: Approximately Propagation Complete and Conflict Propagating Constraint Encodings
  • Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos: Fast and Flexible Probabilistic Model Counting
  • Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos: Fast Sampling of Perfectly Uniform Satisfying Assignments
  • Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjørner and Mooly Sagiv: Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
  • Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva: PySAT: A Python Toolkit for Prototyping with SAT Oracles
  • Jia Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li and Vijay Ganesh: Machine Learning-based Restart Policy for CDCL SAT Solvers
  • Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav Bansal: Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
  • Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider: Polynomial-Time Validation of QCDCL Certificates
  • Jan Elffers, Jesús Giráldez-Crú, Jakob Nordström and Marc Vinyals: Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
  • Michael Lampis, Stefan Mengel and Valia Mitsou: QBF as an Alternative to Courcelle’s Theorem
  • Tobias Friedrich and Ralf Rothenberger: Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
  • Stepan Kochemazov and Oleg Zaikin: ALIAS: A Modular Tool for Finding Backdoors for SAT