Theory and applications of satisfiability testing : 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5-8 2003 : selected revised papers

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. 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 - 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 Numbers / Michael R. Dransfield, Victor W. Marek And Miroslaw Truszczynski -- An Algorithm For Sat Above The Threshold / Hubie Chen -- Watched Data Structures For Qbf Solvers / Ian Gent, Enrico Giunchiglia, Massimo Narizzano, Andrew Rowley And Armando Tacchella. Enrico Giunchiglia, Armando Tacchella (eds.). Includes Bibliographical References And Index. This book is devoted to the 6th International Conference on Theory and applications of Satisability Testing (SAT 2003) held in Santa Margherita Ligure (Genoa, Italy), during May 5-8,2003. SAT 2003 followed the Workshops on S- 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, specific 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 algorithm 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 presentation and discussion of research related to the theory and applications of pro- sitional and QBF satis?ability testing