Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers

ISBN-13: 9783540278290 / Angielski / Miękka / 2005 / 393 str.

Holger H. Hoos;David G. Mitchell

Opis

Constitutes the refereed proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004. This book contains papers and reports covering a spectrum of research in propositional and quantified Boolean formula satisfiability testing; and the fields of theoretical and experimental computer science.

Spis treści

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.