This book constitutes the thoroughly refereed post-proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, SAT 2003, held in Santa Margherita Ligure, Italy, in May 2003.
The 33 revised full papers presented together with 5 articles reporting results of the related SAT competition and QBF evaluation were carefully selected during two rounds of reviewing and improvement from 67 submissions. The whole spectrum of research in propositional and quantified Boolean formula satisfiability testing is covered including proof systems, search techniques, probabilistic analysis of algorithms and their properties, problem encodings, industrial applications, specific tools, case studies, and empirical results.
Author(s): Michael R. Dransfield, Victor W. Marek (auth.), Enrico Giunchiglia, Armando Tacchella (eds.)
Series: Lecture Notes in Computer Science 2919
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2004
Language: English
Pages: 530
Tags: Mathematical Logic and Formal Languages; Algorithm Analysis and Problem Complexity; Numeric Computing; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations
Front Matter....Pages -
Satisfiability and Computing van der Waerden Numbers....Pages 1-13
An Algorithm for SAT Above the Threshold....Pages 14-24
Watched Data Structures for QBF Solvers....Pages 25-36
How Good Can a Resolution Based SAT-solver Be?....Pages 37-52
A Local Search SAT Solver Using an Effective Switching Strategy and an Efficient Unit Propagation....Pages 53-68
Density Condensation of Boolean Formulas....Pages 69-77
SAT Based Predicate Abstraction for Hardware Verification....Pages 78-92
On Boolean Models for Quantified Boolean Horn Formulas....Pages 93-104
Local Search on SAT-encoded Colouring Problems....Pages 105-119
A Study of Pure Random Walk on Random Satisfiability Problems with “Physical” Methods....Pages 120-134
Hidden Threshold Phenomena for Fixed-Density SAT-formulae....Pages 135-149
Improving a Probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs....Pages 150-161
Width-Based Algorithms for SAT and CIRCUIT-SAT....Pages 162-171
Linear Time Algorithms for Some Not-All-Equal Satisfiability Problems....Pages 172-187
On Fixed-Parameter Tractable Parameterizations of SAT....Pages 188-202
On the Probabilistic Approach to the Random Satisfiability Problem....Pages 203-213
Comparing Different Prenexing Strategies for Quantified Boolean Formulas....Pages 214-228
Solving Error Correction for Large Data Sets by Means of a SAT Solver....Pages 229-241
Using Problem Structure for Efficient Clause Learning....Pages 242-256
Abstraction-Driven SAT-based Analysis of Security Protocols....Pages 257-271
A Case for Efficient Solution Enumeration....Pages 272-286
Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms....Pages 287-298
Local Consistencies in SAT....Pages 299-314
Guiding SAT Diagnosis with Tree Decompositions....Pages 315-329
On Computing k -CNF Formula Properties....Pages 330-340
Effective Preprocessing with Hyper-Resolution and Equality Reduction....Pages 341-355
Read-Once Unit Resolution....Pages 356-369
The Interaction Between Inference and Branching Heuristics....Pages 370-382
Hypergraph Reductions and Satisfiability Problems....Pages 383-397
SBSAT: a State-Based, BDD-Based Satisfiability Solver....Pages 398-410
Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution....Pages 411-425
The Combinatorics of Conflicts between Clauses....Pages 426-440
Conflict-Based Selection of Branching Rules....Pages 441-451
The Essentials of the SAT 2003 Competition....Pages 452-467
Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers....Pages 468-485
kcnfs : An Efficient Solver for Random k -SAT Formulae....Pages 486-501
An Extensible SAT-solver....Pages 502-518
Survey and Belief Propagation on Random K -SAT....Pages 519-528
Back Matter....Pages -
