Theory and Applications of Satisfiability Testing - SAT 2006 Book

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