14. SAT 2011: Ann Arbor, MI, USA

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 Sat May 25 19:01:19 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page