Theory and Applications of Satisfiability Testing

Satisfiability and Computing van der Waerden Numbers.- An Algorithm for SAT Above the Threshold.- Watched Data Structures for QBF Solvers.- How Good Can a Resolution Based SAT-solver Be?.- A Local Search SAT Solver Using an Effective Switching Strategy and an Efficient Unit Propagation.- Density Condensation of Boolean Formulas.- SAT Based Predicate Abstraction for Hardware Verification.- On Boolean Models for Quantified Boolean Horn Formulas.- Local Search on SAT-encoded Colouring Problems.- A Study of Pure Random Walk on Random Satisfiability Problems with “Physical” Methods.- Hidden Threshold Phenomena for Fixed-Density SAT-formulae.- Improving a Probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs.- Width-Based Algorithms for SAT and CIRCUIT-SAT.- Linear Time Algorithms for Some Not-All-Equal Satisfiability Problems.- On Fixed-Parameter Tractable Parameterizations of SAT.- On the Probabilistic Approach to the Random Satisfiability Problem.- Comparing Different Prenexing Strategies for Quantified Boolean Formulas.- Solving Error Correction for Large Data Sets by Means of a SAT Solver.- Using Problem Structure for Efficient Clause Learning.- Abstraction-Driven SAT-based Analysis of Security Protocols.- A Case for Efficient Solution Enumeration.- Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms.- Local Consistencies in SAT.- Guiding SAT Diagnosis with Tree Decompositions.- On Computing k-CNF Formula Properties.- Effective Preprocessing with Hyper-Resolution and Equality Reduction.- Read-Once Unit Resolution.- The Interaction Between Inference and Branching Heuristics.- Hypergraph Reductions and Satisfiability Problems.- SBSAT: a State-Based, BDD-Based Satisfiability Solver.- Computing VertexEccentricity in Exponentially Large Graphs: QBF Formulation and Solution.- The Combinatorics of Conflicts between Clauses.- Conflict-Based Selection of Branching Rules.- The Essentials of the SAT 2003 Competition.- Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers.- kcnfs: An Efficient Solver for Random k-SAT Formulae.- An Extensible SAT-solver.- Survey and Belief Propagation on Random K-SAT.

Includes supplementary material: sn.pub/extras