NEW: Springer Conference Proceedings

ABOUT SAT 2015

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.

ORGANIZATION

Program Committee Chairs contact using sat2015@easychair.org

Marijn Heule	The University of Texas at Austin, United States
Sean Weaver	Trusted Systems Research Group, Department of Defense, United States

Workshop Chair

Albert Oliveras

Technical University of Catalonia

Program Committee

Fahiem Bacchus	University of Toronto
Olaf Beyersdorff	University of Leeds
Armin Biere	Johannes Kepler University
Leonardo De Moura	Microsoft Research
Uwe Egly	Vienna University of Technology
John Franco	University of Cincinnati
Enrico Giunchiglia	University of Genova
Youssef Hamadi	Microsoft Research
Holger Hoos	University of British Colombia
Alexander Ivrii	IBM
Matti Järvisalo	University of Helsinki
Jie-Hong Roland Jiang	National Taiwan University
Oliver Kullmann	Swansea University
Daniel Le Berre	Université d'Artois
Ines Lynce	University of Lisbon
Sharad Malik	Princeton University
Panagiotis Manolios	Northeastern University
Norbert Manthey	Technische Universität Dresden
Joao Marques-Silva	University College Dublin
Alexander Nadel	Intel
Nina Narodytska	Carnegie Mellon University
Jakob Nordström	KTH Royal Institude of Technology
Albert Oliveras	Technical University of Catalonia
Karem Sakallah	Ann Arbor, Michigan
Roberto Sebastiani	University of Trento
Martina Seidl	Johannes Kepler University
Bart Selman	Cornell University
Laurent Simon	Bordeaux Institute of Technology
Carsten Sinz	Karlsruhe Institute of Technology
Stefan Szeider	Vienna University of Technology
Xishun Zhao	Sun Yat-Sen University

WORKSHOPS

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.

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

Webpage: http://www.pragmaticsofsat.org/2015/
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
Webpage: http://fmv.jku.at/qbf15/
Organizers: Florian Lonsing and Martina Seidl

PAPERS

Proceedings

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 Su	CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
Peter Steinke and Tobias Philipp	PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
Alexander Ivrii and Valeriy Balabanov	Speeding up MUS Extraction with Preprocessing and Chunking
Ruiwen Chen and Rahul Santhanam	Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
Jan Burchard, Tobias Schubert and Bernd Becker	Laissez-Faire Caching for Parallel #SAT Solving
Zack Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister and Krzysztof Czarnecki	SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
Jonathan Kalechstain, Vadim Ryvchin and Nachum Dershowitz	Hints Revealed
Alexander Ivrii, Vadim Ryvchin and Ofer Strichman	Mining Backbone Literals In Incremental SAT
Adam Douglass, Andrew King and Jack Raymond	Constructing SAT filters with a quantum annealer
Rehan Abdul Aziz, Geoffrey Chu, Christian Muise and Peter J. Stuckey	Projected Model Counting
Oliver Kullmann and Joao Marques-Silva	Computing maximal autarkies with few and simple oracle queries
Tomáš Balyo, Peter Sanders and Carsten Sinz	HordeSat: A Massively Parallel Portfolio SAT Solver
Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl and Bernd Becker	Preprocessing for DQBF
Florian Lonsing and Uwe Egly	Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Simone Bova, Florent Capelli, Stefan Mengel and Friedrich Slivovsky	On Compiling CNFs into Structured Deterministic DNNFs
Stefan Falkner, Marius Lindauer and Frank Hutter	SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Robert Ganian and Stefan Szeider	Community Structure Inspired Algorithms for SAT and #SAT
Carlos Ansótegui, Jesus Giráldez-Cru, Jordi Levy and Laurent Simon	Using Community Structure to Detect Relevant Learnt Clauses
Markus Iser, Carsten Sinz and Norbert Manthey	Recognition of Nested Gates in CNF Formulas
Miguel Neves, Ruben Martins, Mikolas Janota, Ines Lynce and Vasco Manquinho	Exploiting Resolution-based Representations for MaxSAT Solving
Alexey Ignatiev, Alessandro Previti and Joao Marques-Silva	SAT-Based Formula Simplification
Ravi Mangal, Xin Zhang, Mayur Naik and Aditya Nori	Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
Chanseok Oh	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
M. Fareed Arif, Carlos Mencía and Joao Marques-Silva	Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
Kuan-Hua Tu, Tzu-Chien Hsu and Jie-Hong Roland Jiang	QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp and Erika Abraham	SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Antti E. J. Hyvärinen, Matteo Marescotti and Natasha Sharygina	Search-Space Partitioning for Parallelizing SMT Solvers
Christian Zielke and Michael Kaufmann	A New Approach to Partial MUS Enumeration
Armin Biere and Andreas Fröhlich	Evaluating CDCL Variable Scoring Schemes
Carlos Mencía, Alessandro Previti and Joao Marques-Silva	SAT-Based Horn Least Upper Bounds

Submission

Submissions must be made electronically in PDF format through the webpage at: https://easychair.org/conferences/?conf=sat2015

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

Important Dates

See the Important Dates section.

Scope

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

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.

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

Student	Early	Late
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 sat2015@easychair.org by August 31st, 2015. Determinations will be made shortly thereafter.

VENUE

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.

Lodging

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 austinbandb@gmail.com 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.


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

SAT 2015