
×
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. GomesInhaltsverzeichnis
- 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.