Pragmatics of SAT 2011
a workshop of the SAT 2011 conference
June 18, 2011, Ann Arbor, USA
Evolution of state-of-the-art SAT solvers since 2002

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, summarized by the above picture, 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 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.

As such, the participants of the SAT, Pseudo-Boolean and MAX-SAT competitions organized in conjunction with the SAT 2011 conference are warmly encouraged to submit the description of their solver or their benchmarks to the workshop. We especially welcome submissions about the new special tracks of the SAT competition, namely the Minimally Unsatisfiable Subset track and the Combined SAT/QBF Certified UNSAT track.

The first edition of that workshop took place last year 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 workshop takes place on June 18, 2011, between the SAT/SMT Summer School @MIT (June 12-17) and the SAT conference (June 19-22). Another workshop of interest follows the SAT conference, for people interested in applications of SAT technology: SAT for Practical Applications. While PoS is mainly designed for people delivering SAT technology, SPA focuses more on people using that technology.

Topics

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

Programme (subject to last-minute changes)

09:00-10:40 Design of SAT and QBF systems

10:40-11:00 coffee break

11:00-11:50 Application to Package Dependency Management

11:50-12:00 JSAT system description requirements discussion

The question of restricting system descriptions to systems available in source only was raised among the PC. The only requirement is currently that the system should be available for research purposes to check performance claims (i.e. binary form is fine). It has also been suggested that the system should be available directly from JSAT. We would like to gather the feedback of the community on those points.

12:00-13:30 lunch

Invited talk by Alexander Nadel (Intel): SAT technology at Intel

Intel has been developing a SAT solver and a SAT-based model checker for almost a decade. These engines are successfully being used for the formal validation of modern Intel designs. In the first part of this talk, we provide an overview of our engines and describe the major Intel Formal Verification tools that use them. In addition, we depict the guidelines we developed while designing and maintaining an industrial SAT solver. In the second part of the talk, we describe the main results of our SAT-related research that might be of potential interest for a variety of applications of SAT (not necessarily at Intel). In particular, we describe a number of extensions to the basic functionality of a SAT solver, including: (1) Simultaneous satisfiability: the ability to reason about multiple properties in a single SAT solver invocation; (2) High-level unsatisfiable core extraction: the ability to extract unsatisfiable cores in terms of user-given constraints rather than clauses; (3) Multiple diverse solution (model) generation. In addition, we describe our approach to understanding the functionality of a modern SAT solver, based on the notion of a parent resolution derivation rather than on that of an implication graph. We show how it is possible to enhance conflict clause recording based on our approach, and discuss some ideas for future research. (presentation, pdf)

14:30-14:45 coffee break

14:45-16:00 On the design of Parallel SAT solvers

16:00-16:15 brief break

16:15-17:30 SAT related tools

Registration

Registration to the workshop is managed during the SAT conference registration. Registration fee for regular/student registration is 100/50 USD for early registration (until April 30, 2011) and 150/90 USD for late registration.

If you missed the registration to PoS when registering to the SAT conference, you can still register on site the day of the workshop. In that case, we would appreciate that you drop us a line to tell us that you plan to attend the workshop, for organizational purpose.

Submission

There are two possible type of submissions for the workshop. The papers are supposed to be submitted electronically through EasyChair as a PDF file using the LNCS style (the same as the SAT conference).

The final format of the paper will be different: system descriptions will be published as a 6 page JSAT style while regular papers 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.

The system description category especially targets the authors of the systems that enter the SAT 2011 conference competitive events (SAT, Pseudo-Boolean and MAX-SAT competitions). 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. System descriptions are expected to describe briefly but precisely the main features of the system, in a specific version.

Regular papers provide more space to describe in detail a full system or application, provide experimental results, etc.

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