Pragmatics of SAT 2014

a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic

July 13, 2014, Vienna, Austria

Proceedings available! The Easychair Proceedings in Computing Volume 27 are now available.

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 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 is taking place the day before the SAT conference.

Topics

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

Programme/Venue

Tutorial by Armin Biere

Armin Biere

Title Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling

Abstract One of the design principles of the state-of-the-art SAT solver Lingeling is to use as compact data structures as possible. These reduce memory usage, increase cache efficiency and thus improve run-time, particularly, when using multiple solver instances on multi-core machines, as in our parallel portfolio solver Plingeling and our cube and conquer solver Treengeling. The scheduler of a dozen inprocessing algorithms is an important aspect of Lingeling as well. In this talk we explain these design and implementation aspects of Lingeling and discuss new direction of solver design.

Author's bio Since 2004 Prof. Armin Biere is a Full Professor for Computer Science at the Johannes Kepler University in Linz, Austria, and chairs the Institute for Formal Models and Verification. Between 2000 and 2004 he held a position as Assistant Professor within the Department of Computer Science at ETH Zürich, Switzerland. In 1999 Biere was working for a start-up company in electronic design automation after one year as Post-Doc with Edmund Clarke at CMU, Pittsburgh, USA. In 1997 Biere received a Ph.D. in Computer Science from the University of Karlsruhe, Germany. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking, propositional and related techniques. He is the author and co-author of more than 100 papers and served on the program committee of more than 80 international workshops and conferences. His most influential work is his contribution to Bounded Model Checking for which he received in 2014 an award for the most influencial paper in the 20 years of TACAS. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top of many international competitions.

Armin Biere designed numerous solvers based on the Conflict Driven Clause Learning architecture, namely Limmat (2002), Compsat (2003), NanoSAT (2004), Picosat (since 2007), Precosat (2009) and Lingeling (since 2010).

Technical programme

The technical programme is available on the workshop web page on VSL 2014 web site.

The archival proceedings of the workshop is available as Easychair Proceedings in Computing Volume 27.

Registration

Registration is done via the Vienna Summer of Logic registration procedure. Early rate (100 €) applies until June 8, 2014. Late registration (120 €) applies until June 30, 2012. Else on-site rate (130 €) applies. USB stick is not included for people registering only for workshops. The USB stick is available at an additional fee of 25 €. Note that the same registration rate applies for student and non-student.

Submission

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 FLoC 2014 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 conferences.

Important dates

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 pragmaticsofsat.org. 

Daniel Le Berre                               Allen Van Gelder                                                 
Universite d'Artois                           University of California at Santa Cruz       
CNRS                                          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