Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, held in Vancouver, BC, Canada in May 2004. The 24 revised full papers presented together with 2 invited papers were carefully selected from 72 submissions. In addition there are 2 reports on the 2004 SAT Solver Competition and the 2004 QBF Solver Evaluation. The whole spectrum of research in propositional and quantified Boolean formula satisfiability testing is covered; bringing together the fields of theoretical and experimental computer science as well as the many relevant application areas. Front Matter....Pages - Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables....Pages 1-15 A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints....Pages 16-29 An Algebraic Approach to the Complexity of Generalized Conjunctive Queries....Pages 30-45 Incremental Compilation-to-SAT Procedures....Pages 46-58 Resolve and Expand....Pages 59-70 Looking Algebraically at Tractable Quantified Boolean Formulas....Pages 71-79 Derandomization of Schuler’s Algorithm for SAT....Pages 80-88 Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank....Pages 89-104 QBF Reasoning on Real-World Instances....Pages 105-121 Automatic Extraction of Functional Dependencies....Pages 122-132 Algorithms for Satisfiability Using Independent Sets of Variables....Pages 133-144 Aligning CNF- and Equivalence-Reasoning....Pages 145-156 Using DPLL for Efficient OBDD Construction....Pages 157-172 Approximation Algorithm for Random MAX- k SAT....Pages 173-182 Clause Form Conversions for Boolean Circuits....Pages 183-198 From Spin Glasses to Hard Satisfiable Formulas....Pages 199-210 CirCUs: A Hybrid Satisfiability Solver....Pages 211-223 Equivalence Models for Quantified Boolean Formulas....Pages 224-234 Search vs. Symbolic Techniques in Satisfiability Solving....Pages 235-250 Worst Case Bounds for Some NP-Complete Modified Horn-SAT Problems....Pages 251-262 Satisfiability Threshold of the Skewed Random k -SAT....Pages 263-275 NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances....Pages 276-291 Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems....Pages 292-305 UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT....Pages 306-320 Fifty-Five Solvers in Vancouver: The SAT 2004 Competition....Pages 321-344 March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver....Pages 345-359 Zchaff2004: An Efficient SAT Solver....Pages 360-375 The Second QBF Solvers Comparative Evaluation....Pages 376-392 Back Matter....Pages -

This book constitutes the refereed proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, held in Vancouver, BC, Canada in May 2004.

The 24 revised full papers presented together with 2 invited papers were carefully selected from 72 submissions. In addition there are 2 reports on the 2004 SAT Solver Competition and the 2004 QBF Solver Evaluation. The whole spectrum of research in propositional and quantified Boolean formula satisfiability testing is covered; bringing together the fields of theoretical and experimental computer science as well as the many relevant application areas.

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. In the last few years, the AI community has investigated the generic problem solving approach which consists of modeling hard combinatorial problems as instances of the propositional satisfiability problem (SAT) and then solving the resulting encodings with algorithms for SAT.