| Invited Talks |
| From Propositional Satisfiability to Satisfiability Modulo Theories / Hossein M. Sheini ; Karem A. Sakallah |
| CSPs: Adding Structure to SAT / Fahiem Bacchus |
| Proofs and Cores / Session 1： |
| Complexity of Semialgebraic Proofs with Restricted Degree of Falsity / Arist Kojevnikov ; Alexander S. Kulikov |
| Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel / Oliver Kullmann ; Ines Lynce ; Joao Marques-Silva |
| A Scalable Algorithm for Minimal Unsatisfiable Core Extraction / Nachum Dershowitz ; Ziyad Hanna ; Alexander Nadel |
| Minimum Witnesses for Unsatisfiable 2CNFs / Joshua Buresh-Oppenheim ; David Mitchell |
| Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs / Allen Van Gelder |
| Extended Resolution Proofs for Symbolic SAT Solving with Quantification / Toni Jussila ; Carsten Sinz ; Armin Biere |
| Heuristics and Algorithms / Session 2： |
| Encoding CNFs to Empower Component Analysis / Mark Chavira ; Adnan Darwiche |
| Satisfiability Checking of Non-clausal Formulas Using General Matings / Himanshu Jain ; Constantinos Bartzis ; Edmund Clarke |
| Determinization of Resolution by an Algorithm Operating on Complete Assignments / Eugene Goldberg |
| A Complete Random Jump Strategy with Guiding Paths / Hantao Zhang |
| Applications / Session 3： |
| Applications of SAT Solvers to Cryptanalysis of Hash Functions / Ilya Mironov ; Lintao Zhang |
| Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies / Yuliya Zabiyaka |
| Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC / Roberto Sebastiani ; Michele Vescovi |
| SAT in Bioinformatics: Making the Case with Haplotype Inference |
| SMT / Session 4： |
| Lemma Learning in SMT on Linear Constraints / Yinlei Yu ; Sharad Malik |
| On SAT Modulo Theories and Optimization Problems / Robert Nieuwenhuis ; Albert Oliveras |
| Fast and Flexible Difference Constraint Propagation for DPLL(T) / Scott Cotton ; Oded Maler |
| A Progressive Simplifier for Satisfiability Modulo Theories |
| Structure / Session 5： |
| "Dependency Quantified Horn Formulas: Models and Complexity / Uwe Bubeck ; Hans Kleine Buning |
| On Linear CNF Formulas / Stefan Porschen ; Ewald Speckenmeyer ; Bert Randerath |
| A Dichotomy Theorem for Typed Constraint Satisfaction Problems / Su Chen ; Tomasz Imielinski ; Karin Johnsgard ; Donald Smith ; Mario Szegedy |
| Max-SAT / Session 6： |
| A Complete Calculus for Max-SAT / Maria Luisa Bonet ; Jordi Levy ; Felip Manya |
| On Solving the Partial Max-Sat Problem / Zhaohui Fu |
| Max-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(2n) Time / Eugeny Dantsin ; Alexander Wolpert |
| Average-Case Analysis for the Max-2SAT Problem / Osamu Watanabe ; Masaki Yamamoto |
| Local Search and Survey Propagation / Session 7： |
| Local Search for Unsatisfiability / Steven Prestwich |
| Efficiency of Local Search / Andrei A. Bulatov ; Evgeny S. Skvortsov |
| Implementing Survey Propagation on Graphics Processing Units / Panagiotis Manolios ; Yimin Zhang |
| Characterizing Propagation Methods for Boolean Satisfiability / Eric I. Hsu ; Sheila A. McIlraith |
| QBF / Session 8： |
| Minimal False Quantified Boolean Formulas / Xishun Zhao |
| Binary Clause Reasoning in QBF / Horst Samulowitz |
| Solving Quantified Boolean Formulas with Circuit Observability Don't Cares / Daijue Tang |
| QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency / Ashish Sabharwal ; Carlos Ansotegui ; Carla P. Gomes ; Justin W. Hart ; Bart Selman |
| Counting and Concurrency / Session 9： |
| Solving #SAT Using Vertex Covers / Naomi Nishimura ; Prabhakar Ragde ; Stefan Szeider |
| Counting Models in Integer Domains / Antonio Morgado ; Paulo Matos ; Vasco Manquinho |
| SharpSAT - Counting Models with Advanced Component Caching and Implicit BCP / Marc Thurley |
| A Distribution Method for Solving SAT in Grids / Antti Eero Johannes Hyvarinen ; Tommi Junttila ; Ilkka Niemela |
| Author Index |
| Invited Talks |
| From Propositional Satisfiability to Satisfiability Modulo Theories / Hossein M. Sheini ; Karem A. Sakallah |
| CSPs: Adding Structure to SAT / Fahiem Bacchus |
図書
