Abstract is missing.
- Circular (Yet Sound) ProofsAlbert Atserias, Massimo Lauria. 1-18 [doi]
- Short Proofs in QBF ExpansionOlaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan. 19-35 [doi]
- Proof Complexity of QBF Symmetry RecomputationJoshua Blinkhorn, Olaf Beyersdorff. 36-52 [doi]
- Satisfiability Threshold for Power Law Random 2-SAT in Configuration ModelOleksii Omelchenko, Andrei A. Bulatov. 53-70 [doi]
- DRAT Proofs, Propagation Redundancy, and Extended ResolutionSam Buss, Neil Thapen. 71-89 [doi]
- Knowledge Compilation Languages as Proof SystemsFlorent Capelli. 90-99 [doi]
- The Equivalences of Refutational QRATLeroy Chew, Judith Clymo. 100-116 [doi]
- A SAT-Based System for Consistent Query AnsweringAkhil A. Dixit, Phokion G. Kolaitis. 117-135 [doi]
- Incremental Inprocessing in SAT SolvingKatalin Fazekas, Armin Biere, Christoph Scholl. 136-154 [doi]
- Local Search for Fast Matrix MultiplicationMarijn J. H. Heule, Manuel Kauers, Martina Seidl. 155-163 [doi]
- Speeding Up Assumption-Based SATRandy Hickey, Fahiem Bacchus. 164-182 [doi]
- Simplifying CDCL Clause Database ReductionSima Jamali, David Mitchell. 183-192 [doi]
- QRAT Polynomially Simulates ∀ \text -Exp+ResBenjamin Kiesl, Martina Seidl. 193-202 [doi]
- QRATPre+: Effective QBF Preprocessing via Strong Redundancy PropertiesFlorian Lonsing, Uwe Egly. 203-210 [doi]
- On Computing the Union of MUSesCarlos Mencía, Oliver Kullmann, Alexey Ignatiev, João Marques-Silva. 211-221 [doi]
- Revisiting Graph Width Measures for CNF-EncodingsStefan Mengel, Romain Wallon. 222-238 [doi]
- DRMaxSAT with MaxHS: First ContactAntónio Morgado, Alexey Ignatiev, Maria Luisa Bonet, João Marques-Silva, Sam Buss. 239-249 [doi]
- Backing BacktrackingSibylle Möhle, Armin Biere. 250-266 [doi]
- Assessing Heuristic Machine Learning Explanations with Model CountingNina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, João Marques-Silva. 267-278 [doi]
- Syntax-Guided Rewrite Rule Enumeration for SMT SolversAndres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli. 279-297 [doi]
- DRAT-based Bit-Vector Proofs in CVC4Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett. 298-305 [doi]
- Combining Resolution-Path Dependencies with Dependency LearningTomás Peitl, Friedrich Slivovsky, Stefan Szeider. 306-318 [doi]
- Proof Complexity of Fragments of Long-Distance Q-ResolutionTomás Peitl, Friedrich Slivovsky, Stefan Szeider. 319-335 [doi]
- Guiding High-Performance SAT Solvers with Unsat-Core PredictionsDaniel Selsam, Nikolaj Bjørner. 336-353 [doi]
- Verifying Binarized Neural Networks by Angluin-Style LearningAndy Shih, Adnan Darwiche, Arthur Choi. 354-370 [doi]
- \mathsf CrystalBall : Gazing in the Black Box of SAT SolvingMate Soos, Raghav Kulkarni, Kuldeep S. Meel. 371-387 [doi]
- Clausal Abstraction for DQBFLeander Tentrup, Markus N. Rabe. 388-405 [doi]
- On Super Strong ETHNikhil Vyas, Ryan Williams. 406-423 [doi]