Theory and Applications of Satisfiability Testing - SAT 2006  9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings /  [electronic resource] : 
edited by Armin Biere, Carla P. Gomes. 
 - 1st ed. 2006. 
 - XII, 440 p.  online resource. 
 - Theoretical Computer Science and General Issues,  4121  2512-2029 ; .
 - Theoretical Computer Science and General Issues,  4121 .
<br/><br/>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 ClauseDensity 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. 
<br/><br/><label>ISBN: </label>9783540372073 
<br/><br/><label>Standard No.: </label>10.1007/11814948  doi 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Machine theory.<br/>Algorithms.<br/>Operating systems (Computers).<br/>Numerical analysis.<br/>Artificial intelligence.<br/>Mathematical logic.<br/>Formal Languages and Automata Theory.<br/>Algorithms.<br/>Operating Systems.<br/>Numerical Analysis.<br/>Artificial Intelligence.<br/>Mathematical Logic and Foundations.
<br/><br/><label>LC Class. No.: </label>QA267-268.5 
<br/><br/><label>Dewey Class. No.: </label>005.131