SAT 2015

18th International Conference on Theory
and Applications of Satisfiability Testing

September 24-27, 2015 · Austin, Texas, USA

NEW: Springer Conference Proceedings


The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. Aside from plain propositional satisfiability, the scope of the meeting includes Boolean optimization (including MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning.

Many hard combinatorial problems can be tackled using SAT-based techniques, including problems that arise in Formal Verification, Artificial Intelligence, Operations Research, Computational Biology, Cryptology, Data Mining, Machine Learning, Mathematics, et cetera. Indeed, the theoretical and practical advances in SAT research over the past twenty years have contributed to making SAT technology an indispensable tool in a variety of domains.

SAT 2015 invites scientific contributions addressing different aspects of SAT interpreted in a broad sense, including (but not restricted to) theoretical advances (including exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, applications (including both novel applications domains and improvements to existing approaches), as well as case studies and reports on findings based on rigorous experimentation.

SAT 2015 will be co-located with the FMCAD and MEMOCODE conferences, and with the POS, QBF, DIFTS, and ACL2 workshops. The conference program will include, in addition to regular paper presentations, tutorials by Isil Dillig (UT Austin), Priyank Kalla (Utah), Andre Platzer (CMU), and Roderick Bloem (TU Graz); new editions of SAT Race, the Max-SAT Evaluation, and the Pseudo-Boolean Evaluation. The keynote speakers are Dimitris Achlioptas (UC Santa Cruz), Anna Slobodova (Centaur Technology), and Aaron Tomb (Galois, Inc.). SAT 2015 is organized at the computer science department of The University of Texas at Austin under the auspices of SAT Association.


All deadlines are at 23:59 UTC-12 ("anywhere in the world").

Abstract submission deadline: April 22 April 29, 2015 (closed)
Paper submission deadline:April 29 May 6, 2015 (closed)

Author response period: June 10-12 June 17-19, 2015
Author notification: June 28, 2015
Camera-ready versions of papers due:      July 26, 2015

Pre-conference workshops: September 23, 2015
Main conference: September 24-27, 2015


Program Committee Chairs contact using

Marijn HeuleThe University of Texas at Austin, United States
Sean WeaverTrusted Systems Research Group, Department of Defense, United States

Workshop Chair

Albert OliverasTechnical University of Catalonia

Program Committee

Fahiem BacchusUniversity of Toronto
Olaf BeyersdorffUniversity of Leeds
Armin BiereJohannes Kepler University
Leonardo De MouraMicrosoft Research
Uwe EglyVienna University of Technology
John FrancoUniversity of Cincinnati
Enrico GiunchigliaUniversity of Genova
Youssef HamadiMicrosoft Research
Holger HoosUniversity of British Colombia
Alexander IvriiIBM
Matti JärvisaloUniversity of Helsinki
Jie-Hong Roland JiangNational Taiwan University
Oliver KullmannSwansea University
Daniel Le BerreUniversité d'Artois
Ines LynceUniversity of Lisbon
Sharad MalikPrinceton University
Panagiotis ManoliosNortheastern University
Norbert MantheyTechnische Universität Dresden
Joao Marques-SilvaUniversity College Dublin
Alexander NadelIntel
Nina NarodytskaCarnegie Mellon University
Jakob NordströmKTH Royal Institude of Technology
Albert OliverasTechnical University of Catalonia
Karem SakallahAnn Arbor, Michigan
Roberto SebastianiUniversity of Trento
Martina SeidlJohannes Kepler University
Bart SelmanCornell University
Laurent SimonBordeaux Institute of Technology
Carsten SinzKarlsruhe Institute of Technology
Stefan SzeiderVienna University of Technology
Xishun ZhaoSun Yat-Sen University


Pragmatics of Satisfiability
The success of SAT technology in the last decade is mainly due to both the availability of numerous efficient SAT solvers and to the growing number of problems that can efficiently be solved through a translation into SAT. If the main application in the early 2000 was bounded model checking, the current applications range from formal verification (in both software and hardware) to bioinformatics. The benefit of the incredible improvements in the design of efficient SAT solvers those recent years is now reaching our lives: The Intel Core7 processor for instance has been designed with the help of SAT technology, while the device drivers of Windows 7 are being certified thanks to an SMT solver (based on a SAT solver).

The aim of the pragmatics of SAT workshop is to allow researchers concerned with the design of efficient SAT solvers at large or SAT encodings to meet and discuss about their latest results. The workshop is also the place for users of SAT technology to present their applications.

July 24th 2015 (abstract)
July 31st 2015 (paper)

Organizers: Daniel Leberre and Allen van Gelder

Workshop on Quantified Boolean Formulas

The goal of the International Workshop on Quantified Boolean Formulas (QBF) is to bring together researchers working on theoretical and practical aspects of QBF solving and applications. It provides an interactive platform for discussing recent advancements in QBF research. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term challenges.

Deadline: July 15 2015
Organizers: Florian Lonsing and Martina Seidl




All accepted papers have been published in the proceedings of the conference, Lecture Notes in Computer Science volume 9360 by Springer.

Accepted papers

Shaowei Cai, Chuan Luo and Kaile SuCCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
Peter Steinke and Tobias PhilippPBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
Alexander Ivrii and Valeriy BalabanovSpeeding up MUS Extraction with Preprocessing and Chunking
Ruiwen Chen and Rahul SanthanamImproved Algorithms for Sparse MAX-SAT and MAX-k-CSP
Jan Burchard, Tobias Schubert and Bernd BeckerLaissez-Faire Caching for Parallel #SAT Solving
Zack Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister and Krzysztof CzarneckiSATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
Jonathan Kalechstain, Vadim Ryvchin and Nachum DershowitzHints Revealed
Alexander Ivrii, Vadim Ryvchin and Ofer StrichmanMining Backbone Literals In Incremental SAT
Adam Douglass, Andrew King and Jack RaymondConstructing SAT filters with a quantum annealer
Rehan Abdul Aziz, Geoffrey Chu, Christian Muise and Peter J. StuckeyProjected Model Counting
Oliver Kullmann and Joao Marques-SilvaComputing maximal autarkies with few and simple oracle queries
Tomáš Balyo, Peter Sanders and Carsten SinzHordeSat: A Massively Parallel Portfolio SAT Solver
Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl and Bernd BeckerPreprocessing for DQBF
Florian Lonsing and Uwe EglyIncrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Simone Bova, Florent Capelli, Stefan Mengel and Friedrich SlivovskyOn Compiling CNFs into Structured Deterministic DNNFs
Stefan Falkner, Marius Lindauer and Frank HutterSpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Robert Ganian and Stefan SzeiderCommunity Structure Inspired Algorithms for SAT and #SAT
Carlos Ansótegui, Jesus Giráldez-Cru, Jordi Levy and Laurent SimonUsing Community Structure to Detect Relevant Learnt Clauses
Markus Iser, Carsten Sinz and Norbert MantheyRecognition of Nested Gates in CNF Formulas
Miguel Neves, Ruben Martins, Mikolas Janota, Ines Lynce and Vasco ManquinhoExploiting Resolution-based Representations for MaxSAT Solving
Alexey Ignatiev, Alessandro Previti and Joao Marques-SilvaSAT-Based Formula Simplification
Ravi Mangal, Xin Zhang, Mayur Naik and Aditya NoriVolt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
Chanseok OhBetween SAT and UNSAT: The Fundamental Difference in CDCL SAT
M. Fareed Arif, Carlos Mencía and Joao Marques-SilvaEfficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
Kuan-Hua Tu, Tzu-Chien Hsu and Jie-Hong Roland JiangQELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp and Erika AbrahamSMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Antti E. J. Hyvärinen, Matteo Marescotti and Natasha SharyginaSearch-Space Partitioning for Parallelizing SMT Solvers
Christian Zielke and Michael KaufmannA New Approach to Partial MUS Enumeration
Armin Biere and Andreas FröhlichEvaluating CDCL Variable Scoring Schemes
Carlos Mencía, Alessandro Previti and Joao Marques-SilvaSAT-Based Horn Least Upper Bounds


Submissions must be made electronically in PDF format through the webpage at:

If you do not already have an EasyChair account, you will need to sign up for one.

Important Dates

See the Important Dates section.


SAT 2015 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), as well as Constraint Satisfaction Problems (CSP). Topics include (but are not restricted to):

  • Theoretical advances (including exact algorithms, proof complexity, and other complexity issues)
  • Practical search algorithms
  • Knowledge compilation
  • Implementation-level details of SAT solving tools and SAT-based systems
  • Problem encodings and reformulations
  • Applications (including both novel applications domains and improvements to existing approaches)
  • Case studies and reports on insightful findings based on rigorous experimentation

Out of Scope

Papers claiming to resolve a major long-standing open theoretical question in Mathematics or Computer Science (such as those for which a Millennium Prize is offered), are outside the scope of the conference because of insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal.

Paper Categories

Submissions to SAT 2015 are solicited in three paper categories, describing original contributions:

REGULAR PAPERS (9 to 15 pages, excluding references)
Regular papers should contain original research, with sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data and implementations available with their submission. Submissions reporting on case studies are also encouraged, and should describe details, weaknesses, and strengths in sufficient depth.

SHORT PAPERS (up to 8 pages, excluding references)
The same evaluation criteria apply to short papers as to regular papers. They will be reviewed to the same standards of quality as regular papers, but will naturally contain less quantity of new material. Short papers will have the same status as regular papers and be eligible for the same awards (to be announced later).

TOOL PAPERS (up to 6 pages, excluding references)
A tool paper should describe the implemented tool and its novel features. Here "tools" are interpreted in a broad sense, including descriptions of implemented solvers, preprocessors, etc., as well as systems that utilize SAT solvers or their extensions to solve interesting problem domains. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented previously are expected to contain significant and clear enhancements to the tool.

For all paper categories, the page limits stated above do not include references, but do include all other material intended to appear in the conference proceedings. Submissions should use the Springer LNCS style (without space-squeezing modifications), and be written in English.

Regular papers and short papers may be considered for a best paper award. If the main author is a student, both in terms of work and writing, the paper may be considered for a best student-paper award. Use the supplement to the submission to state (in a brief cover letter) if the paper qualifies as a student paper.

Besides the paper itself, authors may submit a supplement consisting of one file in the format of a gzipped tarball (.tar.gz or .tgz) or a gzipped file (.gz) or a zip archive (.zip). Authors are encouraged to submit a supplement when it will help reviewers evaluate the paper. Supplements will be treated with the same degree of confidentiality as the paper itself. For example, the supplement might contain detailed proofs, examples, software, detailed experimental data, or other material related to the submission. Individual reviewers may or may not consult the supplementary material; the paper itself should be self-contained.


Registration and Fees

To register for SAT 2015 and the affiliated workshops, please click here.
Early registration ends on August 23, 2015. The fees, both for conference and workshops, include lunches and coffee breaks.

Conference $450$550
Pragmatics of SAT (full day) $90$90
QBF Workshop (half day)$60$60

Conference $225$275
Pragmatics of SAT (full day) $45$45
QBF Workshop (half day)$30$30

Student Grants

A limited number of student travel support grants of up to 600 Euro per person are available from the SAT Association. Applicants should acquire a letter of support from their advisor and prepare a statement detailing why the travel support is needed. This information should be emailed to the SAT'15 conference chairs at by August 31st, 2015. Determinations will be made shortly thereafter.


Conference Location

SAT 2015 will be held at the AVAYA Auditorium, room 2.302 of the POB building, on the campus of The University of Texas at Austin.

The Pragmatics of SAT (PoS) and the QBF workshops will take place in the Gates Dell Complex (GDC) building on the UT Austin campus. PoS will be in room 6.516 (6th floor of the north wing) and QBF will be in room 7.808 (7th floor of the south wing). The image below shows the location of these rooms. The registration desk is located on the ground (second) floor of the POB building in the lobby. This location is also shown on the map. The coffee break in the morning is shared between the workshops and will be just outside the PoS room. The shared lunch will be in the POB lobby close to the registration desk.


Limited availability; book soon!

A block of rooms has been set aside at the DoubleTree Hotel, Austin Folk House Bed and Breakfast, and Star of Texas Inn. All of them are within walking distance of the conference venue at the University of Texas. Here are details, where room rates do not include taxes.

DoubleTree Hotel: $179 per night
Bed and Breakfast: $105 per night up till September 24 and $180 on September 25 and 26.

The DoubleTree Hotel can be booked via this link. The Bed and Breakfast locations can only be booked via email or phone 866-472-6700 .

Getting to Austin

From most major US cities there are direct flights to Austin-Bergstorm International Airport. The most convinient way to travel to Austin from Europe is the direct flight from London Heathrow by British Airways. The direct flight allows you to do the immigration in Austin which requires only five minutes, while immigration in other cities requires typically an hour.

The easiest way from the Austin airport to downtown and the university is a cab ($30) or Uber ($20). Bus 100 is a cheap alternative ($2) and drives twice an hour from the airport to downtown and the university.