Theory and Applications of Satisfiability Testing -- SAT 2015 : 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings

This book constitutes the refereed proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing, SAT 2015, held in Austin, TX, USA, in September 2015. The 21 regular papers, 2 short papers and 7 tool papers presented together with 3 invited talks were carefully reviewed and selected from 70 submissions. The papers address different aspects of SAT, including theoretical advances (exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, and applications, as well as case studies and reports on insightful findings based on rigorous experimentation. The paper 'Constructing SAT Filters with a Quantum Annealer' is published open access under a CC BY-NC 2.5 license at link.springer.com. Front Matter....Pages I-XIX CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability....Pages 1-8 PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF....Pages 9-16 Speeding up MUS Extraction with Preprocessing and Chunking....Pages 17-32 Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP....Pages 33-45 Laissez-Faire Caching for Parallel #SAT Solving....Pages 46-61 Hints Revealed....Pages 62-70 Mining Backbone Literals in Incremental SAT....Pages 71-87 Constructing SAT Filters with a Quantum Annealer....Pages 88-103 Computing Maximal Autarkies with Few and Simple Oracle Queries....Pages 104-120 HordeSat: A Massively Parallel Portfolio SAT Solver....Pages 121-137 Preprocessing for DQBF....Pages 138-155 Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API....Pages 156-172 On Compiling CNFs into Structured Deterministic DNNFs....Pages 173-190 Community Structure Inspired Algorithms for SAT and #SAT....Pages 191-198 Using Community Structure to Detect Relevant Learnt Clauses....Pages 199-214 Recognition of Nested Gates in CNF Formulas....Pages 215-222 Exploiting Resolution-Based Representations for MaxSAT Solving....Pages 223-237 SAT-Based Formula Simplification....Pages 238-254 Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances....Pages 255-271 Between SAT and UNSAT: The Fundamental Difference in CDCL SAT....Pages 272-286 Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing....Pages 287-298 QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving....Pages 299-306 Search-Space Partitioning for Parallelizing SMT Solvers....Pages 307-323 A New Approach to Partial MUS Enumeration....Pages 324-342 Evaluating CDCL Variable Scoring Schemes....Pages 343-359 SAT-Based Horn Least Upper Bounds....Pages 360-368 Back Matter....Pages 369-386 ....Pages 387-404