可满足性测试理论及其应用 - SAT 2006 第9届国际会议/会议录Theory and applications of satisfiability testing -- SAT 2006
点此进入淘宝搜索页搜索分类: 图书,进口原版书,科学与技术 Science & Techology ,
作者： Armin Biere 著
出 版 社： 湖北辞书出版社
出版时间： 2006-12-1字数：版次： 1页数： 438印刷时间： 2006/12/01开本：印次：纸张： 胶版纸I S B N ： 9783540372066包装： 平装编辑推荐
The LNCS series reports state-of-the-art results in computer science research, development, and education, at a high level and in both printed and electronic form. Enjoying tight cooperation with the R&D community, with numerous individuals, as well as with prestigious organizations and societies, LNCS has grown into the most comprehensive computer science resarch forum available.
The scope of LNCS, including its subseries LNAI, spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields. The type of material publised traditionally includes.
-proceedings(published in time for the respective conference)
-post-proceedings(consisting of thoroughly revised final full papers)
-research monographs(which may be basde on outstanding PhD work, research projects, technical reports, etc.)
内容简介
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 SAT
Session 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 Quantification
Session 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 Paths
Session 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 Inference
Session 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 Theories
Session 5. Structure
Dependency Quantified Horn Formulas: Models and Complexity
On Linear CNF Formulas
……
Session 6. MAX-SAT
Session 7. Loacl Search and Survey Propagation
Session 8. QBF
Session 9. Counting and Concurrency
Author Index
