Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings

Front Matter ....Pages i-xiv
 Circular (Yet Sound) Proofs  (Albert Atserias, Massimo Lauria)....Pages 1-18
 Short Proofs in QBF Expansion  (Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan)....Pages 19-35
 Proof Complexity of QBF Symmetry Recomputation  (Joshua Blinkhorn, Olaf Beyersdorff)....Pages 36-52
 Satisfiability Threshold for Power Law Random 2-SAT in Configuration Model  (Oleksii Omelchenko, Andrei A. Bulatov)....Pages 53-70
 DRAT Proofs, Propagation Redundancy, and Extended Resolution  (Sam Buss, Neil Thapen)....Pages 71-89
 Knowledge Compilation Languages as Proof Systems  (Florent Capelli)....Pages 90-99
 The Equivalences of Refutational QRAT  (Leroy Chew, Judith Clymo)....Pages 100-116
 A SAT-Based System for Consistent Query Answering  (Akhil A. Dixit, Phokion G. Kolaitis)....Pages 117-135
 Incremental Inprocessing in SAT Solving  (Katalin Fazekas, Armin Biere, Christoph Scholl)....Pages 136-154
 Local Search for Fast Matrix Multiplication  (Marijn J. H. Heule, Manuel Kauers, Martina Seidl)....Pages 155-163
 Speeding Up Assumption-Based SAT  (Randy Hickey, Fahiem Bacchus)....Pages 164-182
 Simplifying CDCL Clause Database Reduction  (Sima Jamali, David Mitchell)....Pages 183-192
 QRAT Polynomially Simulates \\(\\forall \\text {-Exp+Res}\\)  (Benjamin Kiesl, Martina Seidl)....Pages 193-202
 QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties  (Florian Lonsing, Uwe Egly)....Pages 203-210
 On Computing the Union of MUSes  (Carlos Mencía, Oliver Kullmann, Alexey Ignatiev, Joao Marques-Silva)....Pages 211-221
 Revisiting Graph Width Measures for CNF-Encodings  (Stefan Mengel, Romain Wallon)....Pages 222-238
 DRMaxSAT with MaxHS: First Contact  (Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva, Sam Buss)....Pages 239-249
 Backing Backtracking  (Sibylle Möhle, Armin Biere)....Pages 250-266
 Assessing Heuristic Machine Learning Explanations with Model Counting  (Nina Narodytska, Aditya Shrotri, Kuldeep S. Meel, Alexey Ignatiev, Joao Marques-Silva)....Pages 267-278
 Syntax-Guided Rewrite Rule Enumeration for SMT Solvers  (Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett et al.)....Pages 279-297
 DRAT-based Bit-Vector Proofs in CVC4  (Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark Barrett)....Pages 298-305
 Combining Resolution-Path Dependencies with Dependency Learning  (Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider)....Pages 306-318
 Proof Complexity of Fragments of Long-Distance Q-Resolution  (Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider)....Pages 319-335
 Guiding High-Performance SAT Solvers with Unsat-Core Predictions  (Daniel Selsam, Nikolaj Bjørner)....Pages 336-353
 Verifying Binarized Neural Networks by Angluin-Style Learning  (Andy Shih, Adnan Darwiche, Arthur Choi)....Pages 354-370
 \\(\\mathsf {CrystalBall}\\): Gazing in the Black Box of SAT Solving  (Mate Soos, Raghav Kulkarni, Kuldeep S. Meel)....Pages 371-387
 Clausal Abstraction for DQBF  (Leander Tentrup, Markus N. Rabe)....Pages 388-405
 On Super Strong ETH  (Nikhil Vyas, Ryan Williams)....Pages 406-423
Back Matter ....Pages 425-425