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