July 4th, 2016, Bordeaux, France
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 took place on July 8, 2013, between the third SAT/SMT school and the SAT 2013 conference. The workshop attracted about 50 participants. The fifth edition took place the day before the SAT 2014 conference and the workshop attracted about 30 participants. The sixth edition took place the day before the SAT 2015 conference and the workshop attracted about 30 participants.
The seventh edition is taking place the day before the SAT 2016 conference.
Remember that work in progress (WIP) papers are only distributed to the audience of the workshop.
|09:30-10:30||Session 2A: Solvers presentations|
|09:30||Beans and Eggs - Proteins for Glucose 3.0 (Markus Iser) [slides]|
|09:45||Splatz (Armin Biere) [slides]|
|10:00||Sub-Stochastic Monte Carlo (SSMC) (Brad Lackey, Stephen Jordan and Michael Jarret) [slides]|
|10:15||Tie break (Seongsoo Moon) [slides]|
|11:00-12:30||Session 3A: Presentations I|
|11:00||REG A Study on Implied Constraints in a MaxSAT Approach to B2B Problems (Miquel Bofill, Marc Garcia, Jesús Giráldez-Cru and Mateu Villaret) [slides]|
|11:30||WIP Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions (Saeed Nejati, Jia Liang, Vijay Ganesh, Catherine Gebotys and Krzysztof Czarnecki) [slides]|
|12:00||WIP Approximate History Map for Massively Parallel Environments (Seongsoo Moon and Mary Inaba) [slides]|
|14:00-15:00||Session 4A: Invited Talk|
|Title Lessons learnt - Seven years of CryptoMiniSat (Mate Soos)|
|Abstract CryptoMiniSat has been around since 2009, with only a single paper effectively talking about its internals. In this presentation I will try to explain the architecture and all the major trade-offs in CryptoMiniSat. I will try to go into some of the more interesting parts of CryptoMiniSat that makes it unique among the other solvers, including its history and current status. CryptoMiniSat is having a relatively successful time in the cryptographic scene. I will explain some of its use-cases and find some reasons for why so many (~180) papers used it in (mostly) that domain. I will also showcase a number of tools developed around the solver that others may find useful such as a comprehensive fuzz harness and a cloud computing-based performance test setup that rivals the size of some SAT solvers.|
|Author's bio Mate Soos is a security consultant working at Gotham Digital Science.
He received his Masters diploma from BUTE, and has done his PhD in the PLANETE team of INRIA Rhone-Alpes under the supervision of Claude Castelluccia, conducting research on RFID security and low-complexity cryptography. He has also done one year of Post-Doctoral study under the supervision of Jean-Charles Faugere.
He worked in Pantel for about 1.5 years in total, where he wrote a MySQL-based telephone-call matching system.
|15:30-17:00||Session 5A: Presentations II|
|15:30||REG Better Evaluations by Analyzing Benchmark Structure (Norbert Manthey and Sibylle Moehle) [slides]|
|16:00||WIP Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (Jan Elffers, Jakob Nordstrom, Laurent Simon and Karem A. Sakallah) [slides]|
|16:30||WIP The Clashing-Neighbor Relation for Propositional Formulas (Allen Van Gelder) [slides]|
|19:30-22:00||SAT 2016 welcome reception (location: Palais de la bourse)|
Main areas of interest include, but are not restricted to:
The workshop welcomes three categories of papers:
Each submission will be reviewed by at least three members of the programme committee.
The papers must be submitted electronically through EasyChair as a PDF file using the EasyChair proceedings style. Each submission is limited to 14 pages, plus references. Accepted regular and work in progress papers will be available to the audience of the workshop and regular papers will be published in a volume of EasyChair in Computing electronic proceedings.
The SAT conference is now accepting tool papers, so there is no need to the push system descriptions as it has been done in the past. We welcome however 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, at any time.
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 SAT 2016 competitive events to consider submitting a description of their solver to PoS, especially if they did not submit a tool paper to the main conferences.
For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to
pos at pragmaticsofsat.org.
Olivier Roussel Allen Van Gelder Université d'Artois University of California at Santa Cruz CNRS School of Engineering Rue de l'Université SP16 62307 Lens FRANCE 1156 High St, Santa Cruz, CA 95064, USA http://www.cril.univ-artois.fr/~roussel/ http://www.cse.ucsc.edu/~avg/