Theory and Applications of Satisfiability Testing

Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables.- Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables.- A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints.- An Algebraic Approach to the Complexity of Generalized Conjunctive Queries.- Incremental Compilation-to-SAT Procedures.- Resolve and Expand.- Looking Algebraically at Tractable Quantified Boolean Formulas.- Derandomization of Schuler's Algorithm for SAT.- Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank.- QBF Reasoning on Real-World Instances.- Automatic Extraction of Functional Dependencies.- Algorithms for Satisfiability Using Independent Sets of Variables.- Aligning CNF- and Equivalence-Reasoning.- Using DPLL for Efficient OBDD Construction.- Approximation Algorithm for Random MAX-kSAT.- Clause Form Conversions for Boolean Circuits.- From Spin Glasses to Hard Satisfiable Formulas.- CirCUs: A Hybrid Satisfiability Solver.- Equivalence Models for Quantified Boolean Formulas.- Search vs. Symbolic Techniques in Satisfiability Solving.- Worst Case Bounds for Some NP-Complete Modified Horn-SAT Problems.- Satisfiability Threshold of the Skewed Random k-SAT.- NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances.- Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems.- UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT.- SAT Solver Competition and QBF Solver Evaluation (Invited Papers).- Fifty-Five Solvers in Vancouver: The SAT 2004 Competition.- March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver.- Zchaff2004: An Efficient SAT Solver.- The Second QBF Solvers Comparative Evaluation.