SAT 2019
July 7 - 12, Lisboa, Portugal

The proceedings will be published by Springer in the series Lecture Notes in Computer Science, see www.springer.com/lncs.

  Proceedings Access (free until end of August)

• Akhil Dixit and Phokion Kolaitis. A SAT-based System for Consistent Query Answering
• Albert Atserias and Massimo Lauria. Circular (Yet Sound) Proofs
• Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar and Clark Barrett. DRAT-based Bit-Vector Proofs in CVC4
• Andrei Bulatov and Oleksii Omelchenko. Satisfiability Threshold for Power Law Random
• Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett and Cesare Tinelli. Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
• Andy Shih, Adnan Darwiche and Arthur Choi. Verifying Binarized Neural Networks by Angluin-Style Learning
• Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva and Sam Buss. DRMaxSAT with MaxHS: First Contact
• Benjamin Kiesl and Martina Seidl. QRAT Polynomially Simulates \forall-Exp+Res
• Carlos Mencía, Oliver Kullmann, Alexey Ignatiev and Joao Marques-Silva. On Computing the Union of MUSes
• Daniel Selsam and Nikolaj Bjorner. NeuroCore: Guiding CDCL with Unsat Core Predictions
• Florent Capelli. Knowledge compilation languages as proof systems
• Florian Lonsing and Uwe Egly. QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
• Joshua Blinkhorn and Olaf Beyersdorff. Proof Complexity of QBF Symmetry Recomputation
• Katalin Fazekas, Armin Biere and Christoph Scholl. Incremental Inprocessing in SAT Solving
• Leander Tentrup and Markus N. Rabe. Clausal Abstraction for DQBF
• Leroy Chew and Judith Clymo. The Equivalences of Refutational QRAT
• Marijn Heule, Manuel Kauers and Martina Seidl. Local Search for Fast Matrix Multiplication
• Mate Soos, Raghav Kulkarni and Kuldeep S. Meel. CrystalBall: Gazing in the Black Box of SAT Solving
• Nikhil Vyas and Ryan Williams. On Super Strong ETH
• Nina Narodytska, Aditya Shrotri, Kuldeep S. Meel, Alexey Ignatiev and Joao Marques Silva. Assessing Heuristic Machine Learning Explanations with Model Counting
• Olaf Beyersdorff, Leroy Chew, Judith Clymo and Meena Mahajan. Short Proofs in QBF Expansion
• Randy Hickey and Fahiem Bacchus. Speeding Up Assumption-Based SAT
• Sam Buss and Neil Thapen. DRAT Proofs, Propagation Redundancy, and Extended Resolution
• Sibylle Möhle and Armin Biere. Backing Backtracking
• Sima Jamali and David Mitchell. Simplifying CDCL Clause Database Reduction
• Stefan Mengel and Romain Wallon. Revisiting Graph Width Measures for CNF-Encodings
• Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider. Combining Resolution-Path Dependencies with Dependency Learning
• Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider. Proof Complexity of Fragments of Long-Distance Q-Resolution