Pragmatics of SAT 2013

a workshop of the SAT 2013 conference

July 8, 2013, Helsinki, Finland

August 28, 2014: Link to Easychair proceedings in computing Volume 29 added.

Scientific context

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).

Designing efficient SAT solvers requires both a good theoretical knowledge about the design of SAT solvers, i.e. how are interacting all its components, and a deep practical knowledge about how to implement efficiently such components.

The SAT community organizes regularly SAT competitive events (SAT competition or SAT Races) to evaluate available SAT solvers on a wide range of problems. The winners of those events set regularly new standards in the area.

If the systems themselves are widely spread, many details on their design or in their implementation can only be found in the source code of the systems. This is also true for the encoding of some constraints. It is usually the case that system descriptions provided for the competitive events are not detailed and that the SAT conference publishes very few system descriptions since 2005 (before that, the post proceedings could contain the system description of the competition winners, e.g. Minisat for SAT'03 and Chaff 2004 for SAT'04).

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.

The first edition of that workshop took place during FLoC 2010. It ended up to be a great success, with more than 30 participants highly interested in the practical aspects of SAT and related problems. The second edition took place before SAT 2011, in Ann Arbor. It attracted also around 30 participants, and broadened the scope of the initial workshop to several applications (ATPG, software dependency management, etc). The third edition took place on June 16, 2012, between the second SAT/SMT Summer School (June 12 to 15) and the SAT conference (June 17-20). The workshop was a success (around 60 participants), many of them coming from the SMT summer school.

The fourth edition is taking place the day before the SAT conference.

Topics

Main areas of interest include, but are not restricted to:

techniques for debugging or certifying solvers
visualisation of benchmarks structure
monitoring solver behaviour
evaluation of solvers
efficient data structures
domain specific encodings
taking into account multi-core technology
domain specific heuristics
new application of sat technology
new use cases of sat technology
system/library description
SAT/SMT solver API

Programme/Venue

PoS 13 will take place at the University of Helsinki, on the third floor, room 5: see SAT'13 venue webpage for details.

Registration desk is located on the fourth floor of the same building. Please consider showing up early at the registration desk to avoid queuing!

All presentations have a 20 minutes slot followed by 5 minutes of questions.

The archival proceedings of the workshop are available as Easychair proceedings in computing Volume 29

9h	Opening
9h-10h30	SAT solvers
Adrian Balint and Norbert Manthey	Boosting the Performance of SLS and CDCL Solvers by Preprocessor Tuning
Daniel Le Berre and Emmanuel Lonca	Reusing or adapting SAT solvers for boolean optimization
Oliver Gableske, Sven Mueelich and Daniel Diepold	On the Performance of CDCL based Message Passing Inspired Decimation using rho-sigma-PMP-i
10h30-11h	Coffee Break
11h-12h30	SAT encodings
Valentin Mayer-Eichberger and Toby Walsh	SAT Encodings for the Car Sequencing Problem
Michael Codish, Yoav Fekete and Amit Metodi	Compiling Finite Domain Constraints to SAT with BEE
Naoyuki Tamura, Mutsunori Banbara and Takehide Soh	PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding
12h-30-14h	Lunch
14h-15h	Applications and tools for SAT
Antti Hyttinen, Patrik Hoyer, Frederick Eberhardt and Matti Järvisalo	Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure
Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre and Stéphanie Roussel	System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems
15h-15h30	Coffee Break
15h30-17h	Parallelism in SAT solving
Martin Aigner, Armin Biere, Christoph Kirsch, Aina Niemetz and Mathias Preiner	Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures
Norbert Manthey, Davide Lanti and Ahmed Irfan	Modern Cooperative Parallel SAT Solving
Norbert Manthey and Kilian Gebhardt	Parallel Variable Elimination on CNF Formulas
17h	Closing

Registration

Registration is performed through the main SAT conference registration system. Note that registration to the main conference includes the access to all workshops, thus PoS. The following registration fees apply for people willing to register only to the workshops.

Early rate (applies until May 27): Student 60 €, Regular 90 €.
Late and very late rate (applies until July 8): Student 90 €, Regular 120 €.

Submission

The papers are supposed to be submitted electronically through EasyChair as a PDF file using the LNCS style (the same as the SAT conference). Unlike previous years, we will only accept one kind of submission (up to 14 pages). Accepted papers will be available on the conference USB stick and published either on the workshop web site or in the EasyChair electronic proceedings.

The SAT conference is now accepting tool papers, so there is no need to the push system description as it has been done in the past. Wep welcome extended versions of tool papers for detailed presentation during the workshop.

Note that it is still possible to submit system descriptions to the JSAT journal.

The final format of the paper will be different: it will use the EasyChair proceedings style.

Authors should provide enough information and/or data for reviewers to confirm any performance claims. This includes links to a runnable system, access to benchmarks, reference to a public performance results, etc.

We warmly encourage the authors of the systems that enter the SAT 2013 conference competitive events (SAT, MAX-SAT, QBF Gallery and SMT competitions) to consider submitting a description of their solver to PoS, especially if they did not submit a tool paper to the main conference. The aim of this workshop is to push forward peer-reviewed published system descriptions as a means to spread technical information regarding the design of solvers.

Important dates

Submission deadlines:
- Abstracts are due by April 14 April 20, 2013
- Papers are due by April 21 April 24, 2013
Authors notification: May 22, 2013.
Final version due: June 16, 2013.
The workshop will take place on July 8th, 2013.

Programme Committee

Contact

For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to pos at satcompetition.org.

Daniel Le Berre                               Allen Van Gelder                                                 
Universite d'Artois                           University of California at Santa Cruz       
CRIL - CNRS UMR 8188                          School of Engineering                        
Rue Jean Souvraz SP 18 62307 Lens FRANCE      1156 High St, Santa Cruz, CA 95064, USA      
http://www.cril.fr/~leberre                   http://www.cse.ucsc.edu/~avg