POS-10: Editor's Preface

This volume contains the papers presented at Pragmatics of SAT, a workshop of the Federated Logic Conference (FLoC), held on July 9, 2011 in Edinburgh.

There were 9 submissions. Each submission was reviewed by at least 2, and on the average 4.3, program committee members. The committee decided to accept 4 papers and 5 system descriptions, the system descriptions being published separately in Journal on Satisfiability, Boolean Modeling and Computation (JSAT) volume 7. The program also included one invited talk from Youssef Hamadi "From Parallel SAT to Distributed SAT".

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. If the users of SAT solvers were mainly researchers a decade ago, SAT solvers now ship in widely used software, such as SUSE Linux operating system or the open platform Eclipse.

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 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 workshop itself was a big success: with more than 30 participants, interested in SAT, Pseudo-Boolean, Max-SAT and QBF. The discussions after each presentations were quite interesting. In this first edition, it has been possible to have sessions describing in details some solvers participating to the same events for which the results were publicly available: the MAXSAT session described in details solvers submitted to MAXSAT09 and the QBF session described several competitors from QBFEVAL'2010.

We would like to thank EasyChair for providing us both the tooling for managing that workshop within the FLoC conference and the online proceedings.