可满足性测试理论及其应用 - SAT 2006 第9届国际会议/会议录Theory and applications of satisfiability testing

出版时间：2006-12  出版社：湖北辞书出版社  作者：Biere, Armin; Gomes, Carla P.;  页数：438  

内容概要

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.

书籍目录

Invited Talks　From Propositional Satisfiability to Satisfiability Modulo Theories　CSPs: Adding Structure to SATSession 1. Proofs and Cores　Complexity of Semialgebraic Proofs with Restricted Degree of Falsity　Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel　A Scalable Algorithm for Minimal Unsatisfiable Core Extraction　Minimum Witnesses for Unsatisfiable 2CNFs　Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs　Extended Resolution Proofs for Symbolic SAT Solving with QuantificationSession 2. Heuristics and Algorithms　Encoding CNFs to Empower Component Analysis　Satisfiability Checking of Non-clausal Formulas Using General Matings　Determinization of Resolution by an Algorithm Operating on Complete Assignments　A Complete Random Jump Strategy with Guiding PathsSession 3. Applications　Applications of SAT Solvers to Cryptanalysis of Hash Functions　Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies　Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC　SAT in Bioinformatics: Making the Case with Haplotype InferenceSession 4. SMT　Lemma Learning in SMT on Linear Constraints　On SAT Modulo Theories and Optimization Problems　Fast and Flexible Difference Constraint Propagation for DPLL(T)　A Progressive Simplifier for Satisfiability Modulo TheoriesSession 5. Structure　Dependency Quantified Horn Formulas: Models and Complexity　On Linear CNF Formulas……Session 6. MAX-SATSession 7. Loacl Search and Survey PropagationSession 8. QBFSession 9. Counting and ConcurrencyAuthor Index