Theory and Applications of Satisfiability Testing – SAT 2017

1. Front Matter

   Pages I-XIII

   PDF

2. Algorithms, Complexity, and Lower Bounds

   1. Front Matter

      Pages 1-1

      PDF

   2. Probabilistic Model Counting with Short XORs

      • Dimitris Achlioptas, Panos Theodoropoulos

      Pages 3-19

   3. Backdoor Treewidth for SAT

      • Robert Ganian, M. S. Ramanujan, Stefan Szeider

      Pages 20-37

   4. New Width Parameters for Model Counting

      • Robert Ganian, Stefan Szeider

      Pages 38-52

   5. Hard Satisfiable Formulas for Splittings by Linear Combinations

      • Dmitry Itsykson, Alexander Knop

      Pages 53-61

3. Clause Learning and Symmetry Handling

   1. Front Matter

      Pages 63-63

      PDF

   2. On the Community Structure of Bounded Model Checking SAT Problems

      • Guillaume Baud-Berthier, Jesús Giráldez-Cru, Laurent Simon

      Pages 65-82

   3. Symmetric Explanation Learning: Effective Dynamic Symmetry Handling for SAT

      • Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe

      Pages 83-100

   4. An Adaptive Prefix-Assignment Technique for Symmetry Reduction

      • Tommi Junttila, Matti Karppa, Petteri Kaski, Jukka Kohonen

      Pages 101-118

   5. An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate

      • Jia Hui Liang, Hari Govind V.K., Pascal Poupart, Krzysztof Czarnecki, Vijay Ganesh

      Pages 119-135

   6. Coverage-Based Clause Reduction Heuristics for CDCL Solvers

      • Hidetomo Nabeshima, Katsumi Inoue

      Pages 136-144

4. Maximum Satisfiability and Minimal Correction Sets

   1. Front Matter

      Pages 145-145

      PDF

   2. (I Can Get) Satisfaction: Preference-Based Scheduling for Concert-Goers at Multi-venue Music Festivals

      • Eldan Cohen, Guoyu Huang, J. Christopher Beck

      Pages 147-163

   3. On Tackling the Limits of Resolution in SAT Solving

      • Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

      Pages 164-183

   4. Improving MCS Enumeration via Caching

      • Alessandro Previti, Carlos Mencía, Matti Järvisalo, Joao Marques-Silva

      Pages 184-194

   5. Introducing Pareto Minimal Correction Subsets

      • Miguel Terra-Neves, Inês Lynce, Vasco Manquinho

      Pages 195-211

5. Parallel SAT Solving

   1. Front Matter

      Pages 213-213

      PDF

   2. A Distributed Version of Syrup

      • Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, Sébastien Tabary

      Pages 215-232

   3. PaInleSS: A Framework for Parallel SAT Solving

      • Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon

      Pages 233-250

This book constitutes the refereed proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, held in Melbourne, Australia, in August/September 2017.


The 22 revised full papers, 5 short papers, and 3 tool papers were carefully reviewed and selected from 64 submissions. The papers are organized in the following topical sections: algorithms, complexity, and lower bounds; clause learning and symmetry handling; maximum satisfiability and minimal correction sets; parallel SAT solving; quantified Boolean formulas; satisfiability modulo theories; and SAT encodings.

• artificial intelligence
• computer architecture
• computer software selection and evaluation
• constraint theory
• formal logic
• formal methods
• formal verifications
• genetic algorithms
• learning algorithms
• learning systems
• machine learning
• model checking
• problem solving
• program processors
• sat solvers
• satisfiability
• semantics
• software engineering
• theorem proving
• verification

• UNSW Sydney, Sydney, Australia

  Serge Gaspers

• University of New South Wales , Sydney, Australia

  Toby Walsh

Policies and ethics