+612 9045 4394
Theory and Applications of Satisfiability Testing : 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003, Selected Revised Papers - Enrico Giunchiglia

Theory and Applications of Satisfiability Testing

6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003, Selected Revised Papers

By: Enrico Giunchiglia (Editor), Armando Tacchella (Editor)


Published: 26th January 2004
Ships: 5 to 9 business days
5 to 9 business days
or 4 easy payments of $39.60 with Learn more
if ordered within

This book is devoted to the 6th International Conference on Theory and - plications of Satis?ability Testing (SAT 2003) held in Santa Margherita Ligure (Genoa, Italy), during May5-8,2003. SAT 2003followedthe WorkshopsonS- is?ability held in Siena (1996), Paderborn (1998), and Renesse (2000), and the Workshop on Theory and Applications of Satis?ability Testing held in Boston (2001) and in Cincinnati (2002). As in the last edition, the SAT event hosted a SAT solvers competition, and, starting from the 2003 edition, also a Quanti?ed Boolean Formulas (QBFs) solvers comparative evaluation. There were 67 submissions of high quality, authored by researchers from all over the world. All the submissions were thoroughly evaluated, and as a result 42 were selected for oral presentations, and 16 for a poster presentation. The presentations covered the whole spectrum of research in propositional and QBF satis?ability testing, including proof systems, search techniques, probabilistic analysis of algorithms and their properties, problem encodings, industrial app- cations, speci?c tools, case studies and empirical results. Further, the program was enriched by three invited talks, given by Riccardo Zecchina (on "Survey Propagation: from Analytic Results on Random k-SAT to a Message-Passing - gorithm for Satis?ability"), Toby Walsh (on "Challenges in SAT (and QBF)") and Wolfgang Kunz (on "ATPG Versus SAT: Comparing Two Paradigms for Boolean Reasoning"). SAT 2003 thus provided a unique forum for the presen- tion and discussion of research related to the theory and applications of pro- sitional and QBF satis?ability testing.

Satisfiability and computing van der Waerden numbersp. 1
An algorithm for SAT above the thresholdp. 14
Watched data structures for QBF solversp. 25
How good can a resolution based SAT-solver be?p. 37
A local search SAT solver using an effective switching strategy and an efficient unit propagationp. 53
Density condensation of Boolean formulasp. 69
SAT based predicate abstraction for hardware verificationp. 78
On Boolean models for quantified Boolean horn formulasp. 93
Local search on SAT-encoded colouring problemsp. 105
A study of pure random walk on random satisfiability problems with "physical" methodsp. 120
Hidden threshold phenomena for fixed-density SAT-formulaep. 135
Improving a probabilistic 3-SAT algorithm by dynamic search and independent clause pairsp. 150
Width-based algorithms for SAT and CIRCUIT-SATp. 162
Linear time algorithms for some not-all-equal satisfiability problemsp. 172
On fixed-parameter tractable parameterizations of SATp. 188
On the probabilistic approach to the random satisfiability problemp. 203
Comparing different prenexing strategies for quantified Boolean formulasp. 214
Solving error correction for large data sets by means of a SAT solverp. 229
Using problem structure for efficient clause learningp. 242
Abstraction-driven SAT-based analysis of security protocolsp. 257
A case for efficient solution enumerationp. 272
Cache performance of SAT solvers : a case study for efficient implementation of algorithmsp. 287
Local consistencies in SATp. 299
Guiding SAT diagnosis with tree decompositionsp. 315
On computing k-CNF formula propertiesp. 330
Effective preprocessing with hyper-resolution and equality reductionp. 341
Read-once unit resolutionp. 356
The interaction between inference and branching heuristicsp. 370
Hypergraph reductions and satisfiability problemsp. 383
SBSAT : a state-based, BDD-based satisfiability solverp. 398
Computing vertex eccentricity in exponentially large graphs : QBF formulation and solutionp. 411
The combinatorics of conflicts between clausesp. 426
Conflict-based selection of branching rulesp. 441
The essentials of the SAT 2003 competitionp. 452
Challenges in the QBF arena : the SAT'03 evaluation of QBF solversp. 468
kcnfs : an efficient solver for random k-SAT formulaep. 486
An extensible SAT-solverp. 502
Survey and belief propagation on random K-SATp. 519
Author indexp. 529
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540208518
ISBN-10: 3540208518
Series: Lecture Notes in Computer Science,
Audience: General
Format: Paperback
Language: English
Number Of Pages: 530
Published: 26th January 2004
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 2.82
Weight (kg): 0.76