Theory and Applications of Satisfiability Testing - SAT 2006 | 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings | ISBN 9783540372066

Theory and Applications of Satisfiability Testing - SAT 2006

9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings

herausgegeben von Armin Biere und Carla P. Gomes
Mitwirkende
Herausgegeben vonArmin Biere
Herausgegeben vonCarla P. Gomes
Buchcover Theory and Applications of Satisfiability Testing - SAT 2006  | EAN 9783540372066 | ISBN 3-540-37206-7 | ISBN 978-3-540-37206-6

Theory and Applications of Satisfiability Testing - SAT 2006

9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings

herausgegeben von Armin Biere und Carla P. Gomes
Mitwirkende
Herausgegeben vonArmin Biere
Herausgegeben vonCarla P. Gomes

Inhaltsverzeichnis

  • 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.