Pragmatics of SAT 2012
a workshop of the SAT 2012 conference
June 16, 2012, Trento, Italy
Evolution of state-of-the-art SAT solvers since 2002 on application benchmarks

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 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 takes place on June 16, 2012, between the second SAT/SMT Summer School (June 12 to 15) and the SAT conference (June 17-20). We would like to take that unique opportunity to make PoS a bridge between SAT and SMT system developers. It appeared pretty clearly during the first SAT/SMT school @MIT that there was a need for a better integration of SAT and SMT technology: SMT solvers are currently built on top of custom SAT solvers and as such do not take advantage of reusing off-the-shelves state-of-the-art SAT solvers. The test cases also often involves solving very quickly thousands of small SAT problems instead of batch solving huge instances. We would like to discuss about those new usage of SAT solvers and the ways to provide an SMT friendly API for SAT solvers.

Topics

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

Programme (tentative)

9h-10h30 SAT

  • Peter Van Der Tak, Marijn Heule and Armin Biere. Concurrent Cube-and-Conquer (slides)
  • Oliver Gableske. The Effect of Clause Elimination on SLS for SAT (slides)
  • Tomohiro Sonobe and Mary Inaba. Division and Alternation of Decision Variables

    • 10h30-11h Coffee break

    11h-12h30 Beyond SAT SD

  • Norbert Manthey and Peter Steinke. npSolver – a SAT based Solver for Optimization Problems (slides)
  • Wolfgang Dvorak, Matti Järvisalo, Johannes Peter Wallner and Stefan Woltran. CEGARTIX: A SAT-Based Argumentation System
  • Anton Belov and Joao Marques-Silva. MUSer2: An Efficient MUS Extractor (slides)

    • Lunch (on site)

    14h-15h30 SAT SD

  • Norbert Manthey and Robert Stelzmann. The SAT Solver Framework priss (slides)
  • Daniel Le Berre and Stephanie Roussel. Sat4j 2.3.2: on the fly solver configuration, System Description (slides)
  • Gilles Audemard and Laurent Simon. GLUCOSE 2.1: Aggressive – but Reactive – Clause Database Management, Dynamic Restarts (slides)

    • 15h30-16h Break

    16h-17h QBF

  • Andreas Fröhlich, Gergely Kovásznai and Armin Biere. A DPLL Approach for Solving DQBF (slides)
  • Allen Van Gelder. Pure Literal Rules and QU-resolution in QBF Search-Based Solvers (slides)

    • 17h-18h SMT

  • Milan Banković. ArgoSMTExpression: an SMT-LIB 2.0 compliant expression library
  • Panel Reusing SAT solvers in SMT solvers

    • Registration

    Registration is available through the SAT conference web site. Registration fee is 60€, reduced to 40€ for students. Registration includes coffee break and lunch.

    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 PoS system description category is especially designed for authors of the systems that enter the SAT 2012 conference competitive events (SAT, Pseudo-Boolean, MAX-SAT and QBF competitions), but is not limited to such systems. 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