12. SAT 2009: Swansea, UK

Invited Talks

• Robert Nieuwenhuis:
  SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. 1
  
• Moshe Y. Vardi:
  Symbolic Techniques in Propositional Satisfiability Solving. 2-3
  

Applications of SAT

• Maria Luisa Bonet, Katherine St. John:
  Efficiently Calculating Evolutionary Tree Measures Using SAT. 4-17
  
• Yury Chebiryak, Thomas Wahl, Daniel Kroening, Leopold Haller:
  Finding Lean Induced Cycles in Binary Hypercubes. 18-31
  
• Arist Kojevnikov, Alexander S. Kulikov, Grigory Yaroslavtsev:
  Finding Efficient Circuits Using SAT-Solvers. 32-44
  
• Marko Samer, Helmut Veith:
  Encoding Treewidth into SAT. 45-50
  

Complexity Theory

• Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer:
  The Complexity of Reasoning for Fragments of Default Logic. 51-64
  
• Olaf Beyersdorff, Sebastian Müller:
  Does Advice Help to Prove Propositional Tautologies? 65-72
  

Structures for SAT

• Bistra N. Dilkina, Carla P. Gomes, Ashish Sabharwal:
  Backdoors in the Context of Learning. 73-79
  
• Daniel Johannsen, Igor Razgon, Magnus Wahlström:
  Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences. 80-85
  
• Stefan Porschen, Tatjana Schmidt, Ewald Speckenmeyer:
  On Some Aspects of Mixed Horn Formulas. 86-100
  
• Patrick Traxler:
  Variable Influences in Conjunctive Normal Forms. 101-113
  

Resolution and SAT

• Albert Atserias, Johannes Klaus Fichte, Marc Thurley:
  Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. 114-127
  
• Jan Johannsen:
  An Exponential Lower Bound for Width-Restricted Clause Learning. 128-140
  
• Allen Van Gelder:
  Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces. 141-146
  
• Eugene Goldberg:
  Boundary Points and Resolution. 147-160
  

Translations to CNF

• Josep Argelich, Alba Cabiscol, Inês Lynce, Felip Manyà:
  Sequential Encodings from Max-CSP into Partial Max-SAT. 161-166
  
• Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
  Cardinality Networks and Their Applications. 167-180
  
• Olivier Bailleux, Yacine Boufkhad, Olivier Roussel:
  New Encodings of Pseudo-Boolean Constraints into CNF. 181-194
  
• Hyondeuk Kim, Fabio Somenzi, HoonSang Jin:
  Efficient Term-ITE Conversion for Satisfiability Modulo Theories. 195-208
  

Techniques for Conflict-Driven SAT Solvers

• HyoJung Han, Fabio Somenzi:
  On-the-Fly Clause Improvement. 209-222
  
• Bas Schaafsma, Marijn Heule, Hans van Maaren:
  Dynamic Symmetry Breaking by Simulating Zykov Contraction. 223-236
  
• Niklas Sörensson, Armin Biere:
  Minimizing Learned Clauses. 237-243
  
• Mate Soos, Karsten Nohl, Claude Castelluccia:
  Extending SAT Solvers to Cryptographic Problems. 244-257
  

Solving SAT by Local Search

• Anton Belov, Zbigniew Stachniak:
  Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability. 258-264
  
• Evgeny S. Skvortsov:
  A Theoretical Analysis of Search in GSAT. 265-275
  
• Stefan Szeider:
  The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT. 276-283
  

Hybrid SAT Solvers

• Adrian Balint, Michael Henn, Oliver Gableske:
  A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem. 284-297
  
• Jingchao Chen:
  Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques. 298-311
  

Automatic Adaption of SAT Solvers

• Shai Haim, Toby Walsh:
  Restart Strategy Selection Using Machine Learning Techniques. 312-325
  
• Mladen Nikolic, Filip Maric, Predrag Janicic:
  Instance-Based Selection of Policies for SAT Solvers. 326-340
  
• Knot Pipatsrisawat, Adnan Darwiche:
  Width-Based Restart Policies for Clause-Learning Satisfiability Solvers. 341-355
  
• Carsten Sinz, Markus Iser:
  Problem-Sensitive Restart Heuristics for the DPLL Procedure. 356-362
  

Stochastic Approaches to SAT Solving

• Nadia Creignou, Hervé Daudé, Uwe Egly, Raphaël Rossignol:
  (1, 2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. 363-376
  
• Eric I. Hsu, Sheila A. McIlraith:
  VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search. 377-390
  

QBFs and Their Representations

• Hans Kleine Büning, Xishun Zhao, Uwe Bubeck:
  Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits. 391-397
  
• Florian Lonsing, Armin Biere:
  A Compact Representation for Syntactic Dependencies in QBFs. 398-411
  
• Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchus:
  Beyond CNF: A Circuit-Based QBF Solver. 412-426
  

Optimisation Algorithms

• Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy:
  Solving (Weighted) Partial MaxSAT through Satisfiability Testing. 427-440
  
• Timo Berthold, Stefan Heinz, Marc E. Pfetsch:
  Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation?. 441-446
  
• Lukas Kroc, Ashish Sabharwal, Bart Selman:
  Relaxed DPLL Search for MaxSAT. 447-452
  
• Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
  Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. 453-466
  
• Chu Min Li, Felip Manyà, Nouredine Ould Mohamedou, Jordi Planes:
  Exploiting Cycle Structures in Max-SAT. 467-480
  
• Mark H. Liffiton, Karem A. Sakallah:
  Generalizing Core-Guided Max-SAT. 481-494
  
• Vasco M. Manquinho, João P. Marques Silva, Jordi Planes:
  Algorithms for Weighted Boolean Optimization. 495-508
  

Distributed and Parallel Solving

• Matthew D. T. Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia:
  PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing. 509-523
  
• Kei Ohmura, Kazunori Ueda:
  c-sat: A Parallel SAT Solver for Clusters. 524-537