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.This workshop follows the spirit of Pragmatics of Decision Procedures in Automated Reasoning organized at FLoC 2006.
Main areas of interest include, but are not restricted to:
- techniques for debugging or certifying solvers
- visualisation of benchmarks structure
- monitoring solver behaviour
- evaluation of solvers
- efficient data structures
- domain specific encodings
- taking into account multi-core technology
- domain specific heuristics
- new application of sat technology
- system/library description
09:00-10:00 Tutorial by Youssef Hamadi: From Parallel SAT to Distributed SAT
This tutorial will present an overview of parallelism in SAT. It will start with a presentation of classical divide and conquer techniques, discuss their ancient origin and compare them to more recent portfolio-based algorithms. It will then present the impact of clause-sharing on their performances and discuss various strategies used to control the communication overhead. A particular technique used to control the classical diversification/intensification tradeoff will also be presented. Finally, perspectives will be given which will relate the current parallel SAT technologies to the expected evolution of computational platforms, leading to distributed SAT solving scenarios.[presentation]
10:30-12:30 MAXSAT / Generalized-SAT session
- Adrian Kuegel. Improved Exact Solver for the Weighted MAX-SAT Problem (Regular paper)[presentation]
- Carlos Ansotegui, María Luisa Bonet and Jordi Levy. On Solving MaxSAT Through SAT (Regular paper)[presentation]
- Daniel Le Berre and Anne Parrain. The SAT4J library, Release 2.2, June 2010 (System description)[presentation]
- Mate Soos. Enhanced Gaussian Elimination in DPLL-based SAT Solvers (Regular paper)[presentation]
14:00-15:00 Tooling and monitoring session
- Norbert Manthey and Ari Saptawijaya. Towards Improving the Resource Usage of SAT-solvers (Regular paper)[presentation]
- Adrian Balint, Daniel Gall, Gregor Kapler and Robert Retz. Experiment design and administration for computer clusters for SAT-solvers (EDACC) (System description)[presentation]
15:30-17:00 QBF session
- Florian Lonsing and Armin Biere. DepQBF: A Dependency-Aware QBF Solver (System description)[presentation]
- Luca Pulina and Armando Tacchella. AQME'10 System Description (System description)[presentation]
- Enrico Giunchiglia, Massimo Narizzano and Paolo Marin. QuBE7.0 (System description)[presentation]
Registration to the workshop is done through the general FLoC registration system.
Pricing is as follows:
|Early rate (until May 17)||Regular (until June 30)||Late (from July 1st)|
|General||70 GBP (EUR, USD)||100 GBP (EUR, USD)||115 GBP (EUR, USD)|
|Student||42 GBP (EUR, USD)||60 GBP (EUR, USD)||69 GBP (EUR, USD)|
- Electronic copies of papers from all conferences and workshops on a USB memory stick.
- The right to attend talks in the technical programme of workshops held on July 10: Lococo, HyLo, DCM day 2, LCC, DTP day 2, LSB, PSPL.
- Coffee breaks
Note: Lunch is not included in registration fee.
FLoC 2010 is located in central Edinburgh with numerous restaurants and sandwich shops in the vicinity, including those in the nearby student union facilities. We suggest allowing £5 for a sandwich and drink; £10 for a sit-down lunch; and £20–25 for evening dinner.
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).
- Regular papers (up to 14 pages). Accepted papers will be published in the new EasyChair electronic proceedings.
- System descriptions (up to 6 pages). Accepted papers will be published in the JSAT journal, in the new system description category.
The final format of the paper will be different: system descriptions will be published as a 4 page JSAT style while regular paper will use a specific workshop 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 2010 conference competitive events (SAT Race 2010, PB 2010, MAXSAT 2010, QBFEVAL 2010, ...). 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.
- Submission deadline: March 26, 2010
- Abstracts are due by March 28, 2010
- Papers are due by March 31, 2010
- Authors notification: April 23, 2010.
- Final version due: May 14, 2010.
- The workshop will take place on July 10th, 2010.
- Josep Argelich
- Armin Biere
- Youssef Hamadi
- Daniel Le Berre
- Olivier Roussel
- Carsten Sinz
- Armando Tacchella
- Allen Van Gelder
For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to
pos at satcompetition.org.
Allen Van Gelder Daniel Le Berre University of California at Santa Cruz CRIL - CNRS UMR 8188 School of Engineering Rue Jean Souvraz SP 18 1156 High St, Santa Cruz, CA 95064, USA 62307 Lens Cedex FRANCE avg at cs.ucsc.edu leberre at cril dot fr