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.
Author(s): Carlos Ansótegui, Felip Manyà (auth.), Holger H. Hoos, David G. Mitchell (eds.)
Series: Lecture Notes in Computer Science 3542 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 393
Tags: Mathematical Logic and Formal Languages; Algorithm Analysis and Problem Complexity; Operating Systems; Numeric Computing; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations
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 -
