Theory and Applications of Satisfiability Testing - SAT 2006 [[electronic resource] ] : 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings / / edited by Armin Biere, Carla P. Gomes

• Pubblicazione: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006
• Edizione: 1st ed. 2006.
• Descrizione fisica: 1 online resource (XII, 440 p.)
• Disciplina: 511.3
• Soggetto topico: Machine theory; Algorithms; Operating systems (Computers); Numerical analysis; Artificial intelligence; Mathematical logic; Formal Languages and Automata Theory; Operating Systems; Numerical Analysis; Artificial Intelligence; Mathematical Logic and Foundations
• Persona (resp. second.): BiereArmin; GomesCarla P
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: 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)/ -- 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 -- A Dichotomy Theorem for Typed Constraint Satisfaction Problems -- Session 6. MAX-SAT -- A Complete Calculus for Max-SAT -- On Solving the Partial MAX-SAT Problem -- MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in Time -- Average-Case Analysis for the MAX-2SAT Problem -- Session 7. Local Search and Survey Propagation -- Local Search for Unsatisfiability -- Efficiency of Local Search -- Implementing Survey Propagation on Graphics Processing Units -- Characterizing Propagation Methods for Boolean Satisfiability -- Session 8. QBF -- Minimal False Quantified Boolean Formulas -- Binary Clause Reasoning in QBF -- Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares -- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency -- Session 9. Counting and Concurrency -- Solving #SAT Using Vertex Covers -- Counting Models in Integer Domains -- sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP -- A Distribution Method for Solving SAT in Grids.
• Titolo autorizzato: Theory and Applications of Satisfiability Testing - SAT 2006
• ISBN: 3-540-37207-5
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996465581803316
• Lo trovi qui: Univ. di Salerno
• Serie: Theoretical Computer Science and General Issues, . 2512-2029 ; ; 4121