SAT 2011 Conference Proceedings
Session 1: Complexity Analysis
Satisfiability Certificates Verifiable in Subexponential Time (BP) [pdf]
Evgeny Dantsin and Edward A. Hirsch
Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II) [pdf]
Sebastian Ordyniak, Daniel Paulusma and Stefan Szeider
How to apply SAT-solving for the equivalence test of monotone normal forms [pdf]
Martin Mundhenk and Robert Zeranski
Parameterized Complexity of DPLL Search Procedures (BP) [pdf]
Olaf Beyersdorff, Nicola Galesi and Massimo Lauria
Session 2: Binary Decision Diagrams
PiDD: A New Decision Diagram for Efficient Problem Solving in Permutation Space [pdf]
Shin-Ichi Minato
DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions [pdf]
Alexey Ignatiev and Alexander Semenov
BDDs for Pseudo-Boolean Constraints - Revisited [pdf]
Ignasi Abio, Robert Nieuwenhuis, Albert Oliveras and Rodriguez-Carbonell Enric
Session 3: Empirical Evaluation
Generalized Conflict-Clause Strengthening for Satisfiability Solvers [pdf]
Allen Van Gelder
SAT Competition 2011 Preview and First Phase Analysis (presentation)
Daniel Le Berre, Olivier Roussel and Matti Jarvisalo
Careful Ranking of Multiple Solvers with Timeouts and Ties [pdf]
Allen Van Gelder
Invited Talk 1
Ryan Williams
Connecting SAT Algorithms and Complexity Lower Bounds [pdf]
Session 4: Theoretical Analysis
A Satisfiability-based Approach for Embedding Generalized Tanglegrams on Level Graphs [pdf]
Ewald Speckenmeyer, Andreas Wotzlaw and Stefan Porschen
Enumerating All Solutions of a Boolean CSP by Non-Decreasing Weight [pdf]
Johannes Schmidt, Nadia Creignou and Frederic Olive
On variables with few occurrences in conjunctive normal forms [pdf]
Oliver Kullmann and Xishun Zhao
Session 5: Extraction of Minimal Unsatisfiable Subsets
Minimally Unsatisfiable Boolean Circuits [pdf]
Anton Belov and Joao Marques-Silva
Faster Extraction of High-Level Minimal Unsatisfiable Cores [pdf]
Vadim Ryvchin and Ofer Strichman
On Improving MUS Extraction Algorithms [pdf]
Joao Marques-Silva and Ines Lynce
Panel Discussion
Topic: Establishing Standards for Empirical Evaluations
Moderator: Allen Van Gelder
Invited Talk 2
Koushik Sen
Concolic Testing and Constraint Satisfaction [pdf]
Session 6: SAT Algorithms
On Freezing and Reactivating Learnt Clauses (BP) [pdf]
Gilles Audemard, Jean Marie Lagniez, Bertrand Mazure and Lakdhar Sais
Efficient CNF Simplification based on Binary Implication Graphs [pdf]
Marijn Heule, Matti Jarvisalo and Armin Biere
Between Restarts and Backjumps [pdf]
Antonio Ramos, Peter Van Der Tak and Marijn Heule
Captain Jack: New Variable Selection Heuristics in Local Search for SAT [pdf]
Dave Tompkins, Adrian Balint and Holger Hoos
Session 7: Quantified Boolean Formulae
Failed Literal Detection for QBF [pdf]
Florian Lonsing and Armin Biere
Abstraction-Based Algorithm for 2QBF [pdf]
Mikolas Janota and Joao Marques-Silva
Transformations into Normal Forms for Quantified Circuits [pdf]
Hans Kleine Buning, Xishun Zhao and Uwe Bubeck
Session 8: Model Enumeration, Empirical Study
Generating Diverse Solutions in SAT [pdf]
Alexander Nadel
Reducing Chaos in SAT-like Search: Finding Solutions Close to a Given One [pdf]
Ignasi Abio, Morgan Deters, Robert Nieuwenhuis and Peter Stuckey
Empirical Study of the Anatomy of Modern SAT Solvers [pdf]
Hadi Katebi, Karem A. Sakallah and Joao Marques-Silva
Poster Sessions
Translating Pseudo-Boolean Constraints into CNF [pdf]
Amir Aavani
Experimenting with the Instances of the MaxSAT Evaluation [pdf]
Josep Argelich, Chu Min Li, Felip Manya and Jordi Planes
Model Counting Using the Inclusion-Exclusion Principle. [pdf]
Huxley Bennett and Sriram Sankaranarayanan
Phase Transitions in Knowledge Compilation: an Experimental Study [pdf]
Jian Gao, Minghao Yin and Ke Xu
EagleUP: Solving Random 3-SAT using SLS with Unit Propagation [pdf]
Oliver Gableske and Marijn Heule
Non-Model-Based Algorithm Portfolios for SAT [pdf]
Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz and Meinolf Sellmann
The order encoding: from tractable CSP to tractable SAT [pdf]
Justyna Petke and Peter Jeavons
Applying UCT to Boolean Satisfiability [pdf]
Alessandro Previti, Raghuram Ramanujan, Marco Schaerf and Bart Selman
A Compact and Efficient SAT-encoding of Finite Domain CSP [pdf]
Tomoya Tanjo, Naoyuki Tamura and Mutsunori Banbara
Learning Polarity from Structure in SAT [pdf]
Bryan Silverthorn and Risto Miikkulainen
