This book constitutes the refereed proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006, held in Seattle, WA, USA in August 2006 as part of the 4th Federated Logic Conference, FLoC 2006.
The 26 revised full papers presented together with 11 revised short papers presented together with 2 invited talks were carefully selected from 95 submissions. All current research issues in propositional and quantified Boolean formula satisfiability testing are covered; the papers are organized in topical sections on proofs and cores, heuristics and algorithms, applications, SMT, structure, MAX-SAT, local search and survey propagation, QBF, as well as counting and concurrency.
Author(s): Hossein M. Sheini, Karem A. Sakallah (auth.), Armin Biere, Carla P. Gomes (eds.)
Series: Lecture Notes in Computer Science 4121 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2006
Language: English
Pages: 440
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 -
From Propositional Satisfiability to Satisfiability Modulo Theories....Pages 1-9
CSPs: Adding Structure to SAT....Pages 10-10
Complexity of Semialgebraic Proofs with Restricted Degree of Falsity....Pages 11-21
Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel....Pages 22-35
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction....Pages 36-41
Minimum Witnesses for Unsatisfiable 2CNFs....Pages 42-47
Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs....Pages 48-53
Extended Resolution Proofs for Symbolic SAT Solving with Quantification....Pages 54-60
Encoding CNFs to Empower Component Analysis....Pages 61-74
Satisfiability Checking of Non-clausal Formulas Using General Matings....Pages 75-89
Determinization of Resolution by an Algorithm Operating on Complete Assignments....Pages 90-95
A Complete Random Jump Strategy with Guiding Paths....Pages 96-101
Applications of SAT Solvers to Cryptanalysis of Hash Functions....Pages 102-115
Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies....Pages 116-129
Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ $\mathcal{ALC}$ ....Pages 130-135
SAT in Bioinformatics: Making the Case with Haplotype Inference....Pages 136-141
Lemma Learning in SMT on Linear Constraints....Pages 142-155
On SAT Modulo Theories and Optimization Problems....Pages 156-169
Fast and Flexible Difference Constraint Propagation for DPLL(T)....Pages 170-183
A Progressive Simplifier for Satisfiability Modulo Theories....Pages 184-197
Dependency Quantified Horn Formulas: Models and Complexity....Pages 198-211
On Linear CNF Formulas....Pages 212-225
A Dichotomy Theorem for Typed Constraint Satisfaction Problems....Pages 226-239
A Complete Calculus for Max-SAT....Pages 240-251
On Solving the Partial MAX-SAT Problem....Pages 252-265
MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in $\mathcal{O}(2^n)$ Time....Pages 266-276
Average-Case Analysis for the MAX-2SAT Problem....Pages 277-282
Local Search for Unsatisfiability....Pages 283-296
Efficiency of Local Search....Pages 297-310
Implementing Survey Propagation on Graphics Processing Units....Pages 311-324
Characterizing Propagation Methods for Boolean Satisfiability....Pages 325-338
Minimal False Quantified Boolean Formulas....Pages 339-352
Binary Clause Reasoning in QBF....Pages 353-367
Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares....Pages 368-381
QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency....Pages 382-395
Solving #SAT Using Vertex Covers....Pages 396-409
Counting Models in Integer Domains....Pages 410-423
sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP....Pages 424-429
A Distribution Method for Solving SAT in Grids....Pages 430-435
Back Matter....Pages -
