Accepted Papers

  • Markus Anders. SAT Preprocessors and Symmetry
  • Jakob Bach, Markus Iser and Klemens Böhm. A Comprehensive Study of k-Portfolios of Recent SAT Solvers
  • Iván Garzón, Pablo Mesejo and Jesús Giráldez-Cru. On the performance of deep generative models of realistic SAT instances
  • Markus Kirchweger, Manfred Scheucher and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture
  • Miguel Cabral, Mikolas Janota and Vasco Manquinho. SAT-based Leximax Optimisation Algorithms
  • Agnes Schleitzer and Olaf Beyersdorff. Classes of Hard Formulas for QBF Resolution
  • Dmitry Itsykson, Artur Riazanov and Petr Smirnov. Tight Bounds for Tseitin Formulas
  • Mikolas Janota, Jelle Piepenbrock and Bartosz Piotrowski. Towards Learning Quantifier Instantiation in SMT
  • Alexander Nadel. Introducing Intel(R) SAT Solver
  • Milan Mosse, Harry Sha and Li-Yang Tan. A generalization of the Satisfiability Coding Lemma and its applications
  • Leroy Chew and Marijn Heule. Relating existing powerful proof systems for QBF
  • Valentin Roland, Johannes K. Fichte and Markus Hecher. Proofs for Propositional Model Counting
  • Benjamin Böhm, Tomáš Peitl and Olaf Beyersdorff. Should decisions in QCDCL follow prefix order?
  • Christoph Jabs, Jeremias Berg, Andreas Niskanen and Matti Järvisalo. MaxSAT-Based Bi-Objective Boolean Optimization
  • Pavel Smirnov, Jeremias Berg and Matti Järvisalo. Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
  • Andreas Niskanen, Jeremias Berg and Matti Järvisalo. Incremental Maximum Satisfiability
  • Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov and Stefan Szeider. Weighted Model Counting with Twin-Width
  • Stephan Gocht, Ruben Martins, Jakob Nordström and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving
  • Stefan Mengel. Changing Partitions in Rectangle Decision Lists
  • Armin Biere, Md Solimul Chowdhury, Benjamin Kiesl, Marijn Heule and Michael Whalen. Migrating Solver State
  • Lucas Berent, Lukas Burgholzer and Robert Wille. Towards a SAT Encoding for Quantum Circuits
  • Nina Narodytska and Nikolaj Bjørner. Analysis of Core-Guided MaxSAT Using Cores and Correction Sets
  • Max Bannach, Malte Skambath and Till Tantau. On the Parallel Parameterized Complexity of MaxSAT Variants
  • Franz-Xaver Reichl and Friedrich Slivovsky. Pedant: A Certifying DQBF Solver
  • Jean Christoph Jung, Valentin Mayer-Eichberger and Abdallah Saffidine. QBF Programming with the Modeling Language Bule
  • Bernardo Subercaseaux and Marijn Heule. The packing chromatic number of the infinite square grid is at least 14
  • Meena Mahajan and Gaurav Sood. QBF Merge Resolution is powerful but unnatural
  • Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang and Christoph Scholl. Quantifier Elimination in Stochastic Boolean Satisfiability
  • Gilles Audemard, Jean Marie Lagniez and Marie Miceli. A New Exact Solver for (Weighted) Max#SAT
  • Friedrich Slivovsky. Quantified CDCL with Universal Resolution
  • Josep Alos, Carlos Ansótegui, Eduard Torres Montiel and Jose María Salvia. OptiLog v2: Model, Solve, Tune And Run