List of Accepted Papers

Uwe Bubeck and Hans Kleine Büning.
Dependency Quantified Horn Formulas: Models and Complexity.
(regular paper).

Andrei Bulatov and Evgeny Skvortsov.
Efficiency of Local Search.
(regular paper).

Joshua Buresh-Oppenheim and David Mitchell.
On the Exact Resolution Complexity of 2SAT.
(short paper).

Mark Chavira and Adnan Darwiche.
Pre-Processing CNFs to Enhance Component Analysis.
(regular paper).

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

Scott Cotton and Oded Maler.
Fast and Flexible Difference Constraint Propagation for DPLL(T).
(regular paper).

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

Zhaohui Fu and Sharad Malik.
On Solving The Partial MAX-SAT Problem.
(regular paper).

Eugene Goldberg.
Determinization of resolution by an algorithm operating on complete assignments.
(short paper).

Eric Hsu and Sheila McIlraith.
Characterizing Propagation Methods for Boolean Satisfiability.
(regular paper).

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

Himanshu Jain, Constantinos Bartzis and Edmund Clarke.
Satisfiability Checking of Non-clausal Formulae using General Matings.
(regular paper).

Toni Jussila, Carsten Sinz and Armin Biere.
Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
(short paper).

Hans Kleine Büning and Xishun Zhao.
Minimal False Quantified Boolean Formulas.
(regular paper).

Arist Kojevnikov and Alexander S. Kulikov.
Complexity of Semialgebraic Proofs with Restricted Degree of Falsity.
(regular paper).

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

María Luisa Bonet, Jordi Levy and Felip Manyà.
A Complete Calculus for Max-SAT.
(regular paper).

Ines Lynce and Joao Marques-Silva.
SAT in Bioinformatics: Making the Case with Haplotype Inference.
(short paper).

Panagiotis Manolios and Yimin Zhang.
Implementing Survey Propagation Algorithm on Graphics Processing Units.
(regular paper).

Ilya Mironov and Lintao Zhang.
Applications of SAT-Solvers to Cryptanalysis.
(regular paper).

António Morgado, Paulo Matos, Vasco Manquinho and Joao Marques-Silva.
Counting Models in Integer Domains.
(regular paper).

Alexander Nadel, Nachum Dershowitz and Ziyad Hanna.
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction.
(short paper).

Robert Nieuwenhuis and Albert Oliveras.
On SAT Modulo Theories and Optimization Problems.
(regular paper).

Naomi Nishimura, Prabhakar Ragde and Stefan Szeider.
Solving #SAT using Vertex Covers.
(regular paper).

Stefan Porschen, Ewald Speckenmeyer and Bert Randerath.
On Linear CNF Formulas.
(regular paper).

Steven Prestwich and Ines Lynce.
Local Search for Unsatisfiability.
(regular paper).

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

Horst Samulowitz and Fahiem Bacchus.
Binary Clause Reasoning in QBF.
(regular paper).

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

Hossein Sheini and Karem Sakallah.
A Progressive Simplifier for Satisfiability Modulo Theories.
(regular paper).

Daijue Tang and Sharad Malik.
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares.
(regular paper).

Marc Thurley.
sharpSAT - counting models with advanced component caching and implicit BCP.
(short paper).

Allen Van Gelder.
Input Cover Number as a Metric for Propositional Resolution Proofs.
(short paper).

Osamu Watanabe and Masaki Yamamoto.
Average-case analysis of the MAX-2SAT problem.
(short paper).

Yinlei Yu and Sharad Malik.
On Learning in SMT.
(regular paper).

Yuliya Zabiyaka and Adnan Darwiche.
Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies.
(regular paper).

Hantao Zhang.
A Complete Random Jump Strategy with Guiding Paths.
(short paper).