List of accepted papers

 

Full Papers

  • Alexander Nadel and Vadim Ryvchin. Efficient SAT Solving under Assumptions
  • Oliver Kullmann and Xishun Zhao. On Davis-Putnam reductions for minimally unsatisfiable clause-sets
  • Maria Luisa Bonet and Sam Buss. An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
  • Gilles Audemard, Benoît Hoessen, Said Jabbour, Jean-Marie Lagniez and Cédric Piette. Revisiting Clause Exchange in Parallel SAT Solving
  • Nadia Creignou and Heribert Vollmer. Parameterized Complexity of Weighted Satisfiability Problems
  • Adrian Balint and Uwe Schöning. Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break
  • Alexander Nadel, Vadim Ryvchin and Ofer Strichman. Preprocessing in Incremental SAT
  • Matti Järvisalo, Petteri Kaski, Mikko Koivisto and Janne Korhonen. Finding Efficient Circuits for Ensemble Computation
  • Alexandra Goultiaeva and Fahiem Bacchus. Off the trail: re-examining the CDCL algorithm
  • Allen Van Gelder, Samuel Wood and Florian Lonsing. Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
  • Yael Ben-Haim, Alexander Ivrii, Oded Margalit and Arie Matsliah. Perfect Hashing and CNF Encodings of Cardinality Constraints
  • Friedrich Slivovsky and Stefan Szeider. Computing Resolution-Path Dependencies in Linear Time
  • Jian Zhang, Feifei Ma and Zhiqiang Zhang. Faulty Interaction Identification via Constraint Solving and Optimization
  • Tero Laitinen, Tommi Junttila and Ilkka Niemelä. Conflict-Driven XOR-Clause Learning
  • Anders Yeo, Venkatesh Raman, Gregory Gutin, Robert Crowston, Mark Jones and Saket Saurabh. Fixed-parameter tractability of satisfying beyond the number of variables
  • Serge Gaspers and Stefan Szeider. Strong Backdoors to Nested Satisfiability
  • Antonio Morgado, Federico Heras and Joao Marques-Silva. Improvements to Core-Guided Binary Search for MaxSAT
  • Anton Belov, Alexander Ivrii, Joao Marques-Silva and Arie Matsliah. On Efficient Computation of Variable MUSes
  • Mikolas Janota, William Klieber, Joao Marques-Silva and Edmund Clarke. Solving QBF with Counterexample Guided Refinement
  • Uwe Egly. On sequent systems and resolution for quantified Boolean formulas
  • Stefano Ermon, Ronan Le Bras, Carla Gomes and Bart Selman. SMT-Aided Combinatorial Material Discovery
  • Antti Hyvärinen and Norbert Manthey. Designing Scalable Parallel SAT Solvers
  • Carlos Ansótegui, Jesús Giráldez and Jordi Levy. The Community Structure of SAT Formulas
  • Dimitris Achlioptas and Ricardo Menchaca-Mendez. Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas
  • Vijay Ganesh, Charles W. O'Donnell, Armando Solar-Lezama, Srini Devadas, Mate Soos and Martin Rinard. Lynx: A Programmatic SAT Solver for the RNA-folding Problem
  • Nikolaj Bjorner and Krystof Hoder. Generalized Property Directed Reachability
  • Georg Weissenbacher. Interpolant Strength Revisited
  • Lin Xu, Frank Hutter, Holger Hoos and Kevin Leyton-Brown. Evaluating Component Solver Contributions in Portfolio-based Algorithm Selectors
  • Valeriy Balabanov, Hui-Ju Katherine Chiang and Jie-Hong Roland Jiang. Henkin Quantifiers and Boolean Formulae

 

Tool Presentations

  • Thomas Hugel. SATLab: X-Raying Random k-SAT (Tool Presentation)
  • Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl and Armin Biere. Resolution-Based Certificate Extraction for QBF (Tool Presentation)
  • Norbert Manthey. Coprocessor 2.0 – A flexible CNF Simplifier (Tool Presentation)
  • Florian Corzilius, Ulrich Loup, Erika Abraham and Sebastian Junges. SMT-RAT: An SMT-Compliant Non-Linear Real Arithmetic Toolbox (Tool Presentation)
  • Michael Kaufmann, Stephan Kottler, Paul Seitz and Christian Zielke. Exploring recurring patterns in conflict analysis of CDCL SAT-Solvers (Tool Presentation)
  • Tomoya Tanjo, Naoyuki Tamura and Mutsunori Banbara. Azucar: A SAT-based CSP solver using the compact order encoding (Tool Presentation)
  • Bard Bloom, David Grove, Benjamin Herta, Vijay Saraswat, Ashish Sabharwal and Horst Samulowitz. SatX10: A Scalable Plug&Play Parallel SAT Framework (Tool Presentation)

 

Poster Presentations

  • Ashutosh Gupta. Improved Single Pass Algorithms for Resolution Proof Reduction (Poster Presentation)
  • Sebastian Burg, Stephan Kottler and Michael Kaufmann. Creating Industrial-Like SAT Instances by clustering and reconstruction (Poster Presentation)
  • Paolo Marin, Christian Miller and Bernd Becker. Incremental QBF Preprocessing for Partial Design Verification (Poster Presentation)
  • Peter van der Tak, Marijn Heule and Armin Biere. Concurrent Cube-and-Conquer (Poster Presentation)
  • Chu Min Li and Yu Li. Satisfying versus falsifying in local search for satisfiability (Poster Presentation)
  • Chu-Min Li, Wanxia Wei and Yu Li. Exploiting historical relationships of clauses and variables in local search for satisfiability (Poster Presentation)
  • Alejandro Arbelaez and Philippe Codognet. Towards Massively Parallel Local Search for SAT (Poster Presentation)
  • Markus Iser, Mana Taghdiri and Carsten Sinz. Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod (Poster presentation)
  • Mark Liffiton and Jordyn Maglalang. A Cardinality Solver: More Expressive Constraints for Free (Poster Presentation)
  • Sam Bayless and Alan Hu. Single-Solver Algorithms for 2QBF (Poster Presentation)
  • Emir Demirović and Haris Gavranović. An Efficient Method for Solving UNSAT 3-SAT and Similar Instances Via Static Decomposition (Poster Presentation)
  • Said Jabbour, Jerry Lonlac and Lakhdar Sais. Intensification Search in Modern SAT Solvers (Poster Presentation)
  • Iago Abal, Alcino Cunha, Joe Hurd and Jorge Sousa Pinto. Using Term Rewriting to Solve Bit-Vector Arithmetic Problems (Poster Presentation)
  • George Katsirelos and Laurent Simon. Learning Polynomials over GF(2) in a SAT Solver (Poster Presentation)
  • Ashish Sabharwal, Horst Samulowitz and Meinolf Sellmann. Learning Back-Clauses in SAT (Poster Presentation)
  • Arie Matsliah, Ashish Sabharwal and Horst Samulowitz. Augmenting Clause Learning with Implied Literals (Poster Presentation)