A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture

Markus Kirchweger, Tomáš Peitl and Stefan Szeider

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Tereza Schwarzová, Jan Strejček and Juraj Major

A Comparison of SAT Encodings for Acyclicity of Directed Graphs

Neng-Fa Zhou, Ruiwei Wang and Roland Yap

Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

Jacobo Torán and Florian Wörz

Certified Knowledge Compilation with Application to Verified Model Counting

Randal Bryant, Wojciech Nawrocki, Jeremy Avigad and Marijn Heule

Validation of QBF Encodings with Winning Strategies

Irfansha Shaik, Maximilian Heisinger, Martina Seidl and Jaco van de Pol

On CNF Conversion for Disjoint SAT Enumeration

Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani

Proof Complexity of Propositional Model Counting

Olaf Beyersdorff, Tim Hoffmann and Luc Nicolas Spachmann

Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT

Anshujit Sharma, Matthew Burns and Michael Huang

Even Shorter Proofs Without New Variables

Adrian Rebola Pardo

CadiBack: Extracting Backbones with CaDiCaL

Armin Biere, Nils Froleyks and Wenxi Wang

Explaining SAT Solving Using Causal Reasoning

Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos and Kuldeep S. Meel

On the Complexity of k-DQBF

Long-Hin Fung and Tony Tan

Effective Auxiliary Variables via Structured Reencoding

Andrew Haberlandt, Harrison Green and Marijn Heule

Separating Incremental and Non-Incremental Bottom-up Compilation

Alexis de Colnet

AllSAT for Combinational Circuits

Yogev Shalmon, Dror Fried and Alexander Nadel

QCDCL vs QBF Resolution: Further Insights

Benjamin Böhm and Olaf Beyersdorff

Limits of CDCL Learning via Merge Resolution

Marc Vinyals, Noah Fleming, Vijay Ganesh, Antonina Kolokolova and Chunxiao Li

UpMax: User Partitioning for MaxSAT

Pedro Orvalho, Vasco Manquinho and Ruben Martins

Faster LRAT Checking than Solving with CaDiCaL

Florian Pollitt, Mathias Fleury and Armin Biere

An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming

George Katsirelos

Learning Shorter Redundant Clauses in SDCL Using MaxSAT

Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung and Vijay Ganesh

LS-DTKMS: a Local Search Algorithm for Diversified Top-K MaxSAT Problem

Junping Zhou, Jiaxin Liang, Minghao Yin and Bo He