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

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