Table of Contents

Parameterized Compilation Lower Bounds for Restricted CNF-formulas.- Satisfiability via Smooth Pictures.- Solution-Graphs of Boolean Formulas and Isomorphism.- Strong Backdoors for Default Logic.- The Normalized Autocorrelation Length of Max r-Sat Converges in Probability to (1-1/2=r)/r.- Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle.- Extreme Cases in SAT Problems.- Improved Static Symmetry Breaking for SAT.- Learning Rate Based Branching Heuristic for SAT Solvers.- On the Hardness of SAT with Community Structure.- Trade-offs between Time and Memory in a Tighter Model of CDCL SAT Solvers.- A SAT Approach to Branch Width.- Computing Maximum Unavoidable Subgraphs Using SAT Solvers.- Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT.- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer.- Deciding Bit-Vector Formulas with mcSAT.- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams.- Speeding Up the Constraint-Based Method in Difference Logic.- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers.- Finding Finite Models in Multi-Sorted First Order Logic.- MCS Extraction with Sublinear Oracle Queries.- Predicate Elimination for Preprocessing in First-Order Theorem Proving.- Quantified Boolean Formula Incremental Determinization.- Non-prenex QBF Solving using Abstraction.- On Q-Resolution and CDCL QBF Solving.- On Stronger Calculi for QBFs.- Q-Resolution with Generalized Axioms.- 2QBF: Challenges and Solutions.- Dependency Schemes for DQBF.- Lifting QBF Resolution Calculi to DQBF.- Long Distance Q-Resolution with Dependency Schemes.- BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies.- HordeQBF: A Modular and Massively Parallel QBF Solver.- LMHS: A SAT-IP Hybrid MaxSAT Solver.- OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing.- SpyBug: Automated Bug Detection in the Con_guration Space of SAT Solvers.