Accepted Papers

Osamu Watanabe, Masaki Yamamoto
Average-case analysis of the MAX-2SAT problem

Stefan Porschen, Ewald Speckenmeyer, and Bert Randerath
On Linear CNF Formulas

Evgeny Dantsin, Alexander Wolpert
MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster than in $O(2^n)$ Time

Andrei Bulatov, Evgeny Skvortsov
Efficiency of Local Search

Zhaohui Fu, Sharad Malik
On Solving The Partial MAX-SAT Problem

Eric Hsu, Sheila McIlraith
Characterizing Propagation Methods for Boolean Satisfiability

António Morgado, Paulo Matos, Vasco Manquinho, and Joao Marques-Silva
Counting Models in Integer Domains

Scott Cotton, Oded Maler
Fast and Flexible Difference Constraint Propagation for DPLL(T)

Joshua Buresh-Oppenheim, David Mitchell
Minimum Witnesses for Unsatisfiable 2CNFs

Yuliya Zabiyaka, Adnan Darwiche
Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies

Ashish Sabharwal, Carlos Ansotegui, Carla P. Gomes, Justin W. Hart, and Bart Selman
QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

Hossein Sheini, Karem Sakallah
A Progressive Simplifier for Satisfiability Modulo Theories

Mark Chavira, Adnan Darwiche
Pre-Processing CNFs to Enhance Component Analysis

Hans Kleine Büning, Xishun Zhao
Minimal False Quantified Boolean Formulas

Yinlei Yu, Sharad Malik
Lemma Learning in SMT on Linear Constraints

Arist Kojevnikov, Alexander S. Kulikov
Complexity of Semialgebraic Proofs with Restricted Degree of Falsity

Roberto Sebastiani, Michele Vescovi
Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC

Ines Lynce, Joao Marques-Silva
SAT in Bioinformatics: Making the Case with Haplotype Inference

Panagiotis Manolios, Yimin Zhang
Implementing Survey Propagation on Graphics Processing Units

Oliver Kullmann, Ines Lynce, and Joao Marques-Silva
Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel

Eugene Goldberg
Determinization of resolution by an algorithm operating on complete assignments

Steven Prestwich, Ines Lynce
Local Search for Unsatisfiability

Horst Samulowitz, Fahiem Bacchus
Binary Clause Reasoning in QBF

Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider
Solving #SAT using Vertex Covers

Allen Van Gelder
Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs

María Luisa Bonet, Jordi Levy, and Felip Manyà
A Complete Calculus for Max-SAT

Alexander Nadel, Nachum Dershowitz, and Ziyad Hanna
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

Himanshu Jain, Constantinos Bartzis, and Edmund Clarke
Satisfiability Checking of Non-clausal Formulas using General Matings

Marc Thurley
sharpSAT - counting models with advanced component caching and implicit BCP

Hantao Zhang
A Complete Random Jump Strategy with Guiding Paths

Antti Eero Johannes Hyvärinen, Tommi Junttila, and Ilkka Niemelä
A Distribution Method for Solving SAT in Grids

Toni Jussila, Carsten Sinz, and Armin Biere
Extended Resolution Proofs for Symbolic SAT Solving with Quantification

Robert Nieuwenhuis, Albert Oliveras
On SAT Modulo Theories and Optimization Problems

Ilya Mironov, Lintao Zhang
Applications of SAT-Solvers to Cryptanalysis

Su Chen, Tomasz Imielinski, Karin Johnsgard, Donald Smith, and Mario Szegedy
A Dichotomy Theorem for Constraint Satisfaction Problems with Disjoint Domains

Uwe Bubeck, Hans Kleine Büning
Dependency Quantified Horn Formulas: Models and Complexity

Daijue Tang, Sharad Malik
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares