Theory and Applications of Satisfiability Testing

Preface.- Solving Over-Constrained Problems with SAT Technology.- A Symbolic Search Based Approach for Quantified Boolean Formulas.- Substitutional Definition of Satisfiability in Classical Propositional Logic.- A Clause-Based Heuristic for SAT Solvers.- Effective Preprocessing in SAT Through Variable and Clause Elimination.- Resolution and Pebbling Games.- Local and Global Complete Solution Learning Methods for QBF.- Equivalence Checking of Circuits with Parameterized Specifications.- Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming.- Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution.- Resolution Tunnels for Improved SAT Solver Performance.- Diversification and Determinism in Local Search for Satisfiability.- On Finding All Minimally Unsatisfiable Subformulas.- Optimizations for Compiling Declarative Models into Boolean Formulas.- Random Walk with Continuously Smoothed Variable Weights.- Derandomization of PPSZ for Unique-k-SAT.- Heuristics for Fast Exact Model Counting.- A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic.- DPvis - A Tool to Visualize the Structure of SAT Instances.- Constraint Metrics for Local Search.- Input Distance and Lower Bounds for Propositional Resolution Proof Length.- Sums of Squares, Satisfiability and Maximum Satisfiability.- Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable.- A New Approach to Model Counting.- Benchmarking SAT Solvers for Bounded Model Checking.- Model-Equivalent Reductions.- Improved Exact Solvers for Weighted Max-SAT.- Quantifier Trees for QBFs.- Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas.- A Branching Heuristics for Quantified Renamable Horn Formulas.- An Improved Upper Bound for SAT.- Bounded Model Checking with QBF.- Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies.- Cost-Effective Hyper-Resolution for