13. SAT 2011: Ann Arbor, MI, USA

Karem A. Sakallah, Laurent Simon (Eds.): Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings. Lecture Notes in Computer Science 6695 Springer 2011, ISBN 978-3-642-21580-3

Invited Talks

Ryan Williams:
Connecting SAT Algorithms and Complexity Lower Bounds. 1-2
Koushik Sen:
Concolic Testing and Constraint Satisfaction. 3-4

Complexity Analysis

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria:
Parameterized Complexity of DPLL Search Procedures. 5-18
Evgeny Dantsin, Edward A. Hirsch:
Satisfiability Certificates Verifiable in Subexponential Time. 19-32
Oliver Kullmann, Xishun Zhao:
On Variables with Few Occurrences in Conjunctive Normal Forms. 33-46
Sebastian Ordyniak, Daniël Paulusma, Stefan Szeider:
Satisfiability of Acyclic and almost Acyclic CNF Formulas (II). 47-60

Binary Decision Diagrams

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
BDDs for Pseudo-Boolean Constraints - Revisited. 61-75
Alexey Ignatiev, Alexander Semenov:
DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions. 76-89
Shin-ichi Minato:
πDD: A New Decision Diagram for Efficient Problem Solving in Permutation Space. 90-104

Theoretical Analysis

Martin Mundhenk, Robert Zeranski:
How to Apply SAT-Solving for the Equivalence Test of Monotone Normal Forms. 105-119
Nadia Creignou, Frédéric Olive, Johannes Schmidt:
Enumerating All Solutions of a Boolean CSP by Non-decreasing Weight. 120-133
Ewald Speckenmeyer, Andreas Wotzlaw, Stefan Porschen:
A Satisfiability-Based Approach for Embedding Generalized Tanglegrams on Level Graphs. 134-144

Extraction of Minimal Unsatisfiable Subsets

Anton Belov, João P. Marques Silva:
Minimally Unsatisfiable Boolean Circuits. 145-158
João P. Marques Silva, Inês Lynce:
On Improving MUS Extraction Algorithms. 159-173
Vadim Ryvchin, Ofer Strichman:
Faster Extraction of High-Level Minimal Unsatisfiable Cores. 174-187

SAT Algorithms

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Sais:
On Freezing and Reactivating Learnt Clauses. 188-200
Marijn Heule, Matti Järvisalo, Armin Biere:
Efficient CNF Simplification Based on Binary Implication Graphs. 201-215
Antonio Ramos, Peter van der Tak, Marijn Heule:
Between Restarts and Backjumps. 216-229

Quantified Boolean Formulae

Mikolás Janota, João P. Marques Silva:
Abstraction-Based Algorithm for 2QBF. 230-244
Hans Kleine Büning, Xishun Zhao, Uwe Bubeck:
Transformations into Normal Forms for Quantified Circuits. 245-258
Florian Lonsing, Armin Biere:
Failed Literal Detection for QBF. 259-272

Model Enumeration, Local Search

Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey:
Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One. 273-286
Alexander Nadel:
Generating Diverse Solutions in SAT. 287-301
Dave A. D. Tompkins, Adrian Balint, Holger H. Hoos:
Captain Jack: New Variable Selection Heuristics in Local Search for SAT. 302-316

Empirical Evaluation

Allen Van Gelder:
Careful Ranking of Multiple Solvers with Timeouts and Ties. 317-328
Allen Van Gelder:
Generalized Conflict-Clause Strengthening for Satisfiability Solvers. 329-342
Hadi Katebi, Karem A. Sakallah, João P. Marques Silva:
Empirical Study of the Anatomy of Modern Sat Solvers. 343-356

Extended Abstracts

Amir Aavani:
Translating Pseudo-Boolean Constraints into CNF. 357-359
Josep Argelich, Chu Min Li, Felip Manyà, Jordi Planes:
Analyzing the Instances of the MaxSAT Evaluation. 360-361
Huxley Bennett, Sriram Sankaranarayanan:
Model Counting Using the Inclusion-Exclusion Principle. 362-363
Jian Gao, Minghao Yin, Ke Xu:
Phase Transitions in Knowledge Compilation: An Experimental Study. 364-366
Oliver Gableske, Marijn Heule:
EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation. 367-368
Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf Sellmann:
Non-Model-Based Algorithm Portfolios for SAT. 369-370
Justyna Petke, Peter Jeavons:
The Order Encoding: From Tractable CSP to Tractable SAT. 371-372
Alessandro Previti, Raghuram Ramanujan, Marco Schaerf, Bart Selman:
Applying UCT to Boolean Satisfiability. 373-374
Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara:
A Compact and Efficient SAT-Encoding of Finite Domain CSP. 375-376
Bryan Silverthorn, Risto Miikkulainen:
Learning Polarity from Structure in SAT. 377-378

Last update Fri May 25 08:35:21 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page