This book constitutes the refereed proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing, SAT 2008, held in Guangzhou, P. R. China, in May 2008.
The 17 revised full papers presented together with 8 revised short papers and 2 invited talks were carefully selected from 70 submissions. All current research issues in propositional and quantified Boolean formula satisfiability testing are covered, including but not limited to proof systems, proof complexity, search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, simplifiers, tools, case studies and empirical results.
Author(s): Josep Argelich, Alba Cabiscol, Inês Lynce (auth.), Hans Kleine Büning, Xishun Zhao (eds.)
Series: Lecture Notes in Computer Science 4996 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2008
Language: English
Pages: 305
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 -
Modelling Max-CSP as Partial Max-SAT....Pages 1-14
A Preprocessor for Max-SAT Solvers....Pages 15-20
A Generalized Framework for Conflict Analysis....Pages 21-27
Adaptive Restart Strategies for Conflict Driven SAT Solvers....Pages 28-33
New Results on the Phase Transition for Random Quantified Boolean Formulas....Pages 34-47
Designing an Efficient Hardware Implication Accelerator for SAT Solving....Pages 48-62
Attacking Bivium Using SAT Solvers....Pages 63-76
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers....Pages 77-90
Random Instances of W[2]-Complete Problems: Thresholds, Complexity, and Algorithms....Pages 91-104
Complexity and Algorithms for Well-Structured k -SAT Instances....Pages 105-118
A Decision-Making Procedure for Resolution-Based SAT-Solvers....Pages 119-132
Online Estimation of SAT Solving Runtime....Pages 133-138
A Max-SAT Inference-Based Pre-processing for Max-Clique....Pages 139-152
SAT, UNSAT and Coloring....Pages 153-153
Computation of Renameable Horn Backdoors....Pages 154-160
A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors....Pages 161-167
Improvements to Hybrid Incremental SAT Algorithms....Pages 168-181
Searching for Autarkies to Trim Unsatisfiable Clause Sets....Pages 182-195
Nenofex: Expanding NNF for QBF Solving....Pages 196-210
SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions....Pages 211-224
Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms....Pages 225-230
A CNF Class Generalizing Exact Linear Formulas....Pages 231-245
How Many Conflicts Does It Need to Be Unsatisfiable?....Pages 246-256
Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning....Pages 257-270
Local Restarts....Pages 271-276
Regular and General Resolution: An Improved Separation....Pages 277-290
Finding Guaranteed MUSes Fast....Pages 291-304
Back Matter....Pages -
