Theory and Applications of Satisfiability Testing -- SAT 2012

1. Front Matter

   PDF

2. Invited Talks

   1. Understanding IC3

      • Aaron R. Bradley

      Pages 1-14

   2. Satisfiability and The Art of Computer Programming

      • Donald Knuth

      Pages 15-15

3. Full Papers

   1. Stochastic Local Search

      1. Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break

         • Adrian Balint, Uwe Schöning

         Pages 16-29

      2. Off the Trail: Re-examining the CDCL Algorithm

         • Alexandra Goultiaeva, Fahiem Bacchus

         Pages 30-43

   2. Theory

      1. An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning

         • Maria Luisa Bonet, Sam Buss

         Pages 44-57

      2. Computing Resolution-Path Dependencies in Linear Time ,

         • Friedrich Slivovsky, Stefan Szeider

         Pages 58-71

      3. Strong Backdoors to Nested Satisfiability

         • Serge Gaspers, Stefan Szeider

         Pages 72-85

   3. Quantified Boolean Formulae

      1. Extended Failed-Literal Preprocessing for Quantified Boolean Formulas

         • Allen Van Gelder, Samuel B. Wood, Florian Lonsing

         Pages 86-99

      2. On Sequent Systems and Resolution for QBFs

         • Uwe Egly

         Pages 100-113

      3. Solving QBF with Counterexample Guided Refinement

         • Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke

         Pages 114-128

      4. Henkin Quantifiers and Boolean Formulae

         • Valeriy Balabanov, Hui-Ju Katherine Chiang, Jie-Hong Roland Jiang

         Pages 129-142

   4. Applications

      1. Lynx: A Programmatic SAT Solver for the RNA-Folding Problem

         • Vijay Ganesh, Charles W. O’Donnell, Mate Soos, Srinivas Devadas, Martin C. Rinard, Armando Solar-Lezama

         Pages 143-156

      2. Generalized Property Directed Reachability

         • Kryštof Hoder, Nikolaj Bjørner

         Pages 157-171

      3. SMT-Aided Combinatorial Materials Discovery

         • Stefano Ermon, Ronan Le Bras, Carla P. Gomes, Bart Selman, R. Bruce van Dover

         Pages 172-185

      4. Faulty Interaction Identification via Constraint Solving and Optimization

         • Jian Zhang, Feifei Ma, Zhiqiang Zhang

         Pages 186-199

   5. Parallel and Portfolio Approaches

      1. Revisiting Clause Exchange in Parallel SAT Solving

         • Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette

         Pages 200-213

      2. Designing Scalable Parallel SAT Solvers

         • Antti E. J. Hyvärinen, Norbert Manthey

         Pages 214-227

      3. Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors

         • Lin Xu, Frank Hutter, Holger Hoos, Kevin Leyton-Brown

         Pages 228-241

   6. CDCL SAT Solving

      1. Efficient SAT Solving under Assumptions

         • Alexander Nadel, Vadim Ryvchin

         Pages 242-255

This book constitutes the refereed proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, held in Trento, Italy, in June 2012. The 29 revised full papers, 7 tool papers, and 16 poster papers presented together with 2 invited talks were carefully reviewed and selected from 112 submissions (88 full, 10 tool and 14 poster papers). The papers are organized in topical sections on stochastic local search, theory, quantified Boolean formulae, applications, parallel and portfolio approaches, CDCL SAT solving, MAX-SAT, cores interpolants, complexity analysis, and circuits and encodings.

• SAT solvers
• algorithm complexity
• automated reasoning
• constraints programming
• resolution
• algorithm analysis and problem complexity
• information and communication, circuits

• Center for Information Technology, Fondazione Bruno Kessler, Trento, Italy

  Alessandro Cimatti

• Department of Information Engineering and Computer Science, University of Trento, Trento, Italy

  Roberto Sebastiani

Policies and ethics