Theory and Applications of Satisfiability Testing - SAT 2006
Springer Berlin (Verlag)
978-3-540-37206-6 (ISBN)
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.
| Erscheint lt. Verlag | 26.7.2006 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science | Theoretical Computer Science and General Issues |
| Zusatzinfo | XII, 440 p. |
| Verlagsort | Berlin |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Gewicht | 635 g |
| Themenwelt | Informatik ► Software Entwicklung ► Qualität / Testen |
| Mathematik / Informatik ► Informatik ► Theorie / Studium | |
| Schlagworte | Algorithm analysis and problem complexity • algorithms • Bioinformatics • Calculus • Complexity • Description Logics • Heuristics • learning • Local Search • MAX-SAT • Optimization • probabilistic algorithms • proof systems • Proof theory • propositional logic • QBF • quantified Boolean formulas • random walks • Resolution • SAT algorithms • satisfiability • satisfiability testing • SAT solvers • Searching • SMT • survey propagation |
| ISBN-10 | 3-540-37206-7 / 3540372067 |
| ISBN-13 | 978-3-540-37206-6 / 9783540372066 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
