SAT 2016

As in previous years, the SAT conference hosts several competitive events which run before the conference and whose results are disclosed during the conference.

Competitive Events

This year, the following competitive events will be organized:

• SAT competition
• MAXSAT evaluation
• QBF evaluation
• PB Competition

Workshops

The day before the conference, Monday July 4th, will be a workshop day. For the moment, the workshops having been organized for a while with the SAT conference has been reconducted this year.

• Seventh Pragmatics of SAT international workshop (POS'16)
• International Workshop on Quantified Boolean Formulas (QBF'16)
• 6th International Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT'16)
• Graph Structure and Satisfiability Testing

Industrial Day: How to solve it with SAT?
Saturday, 9th

Using SAT solvers to tackle industrial problems led to several success stories, the most visible one being the quick adoption of SAT technology in formal verification companies.

The research community has provided in the past 15 years a wide range of tools (solvers) which can be used in companies. However, having access to efficient solvers is often not sufficient to be able to tackle a specific problem with SAT technology. A specific expertise is needed for instance to translate the original problem to feed the solver, the choice of the solver may also be of crucial importance.

Furthermore, SAT technology empowers a wide range of tools and methods to solve both optimization problems (pseudo-Boolean optimization, MAXSAT) or problems strictly more complex that SAT (MUS, QBF).

The aim of the Industrial day is to allow current or prospective practitionners of SAT technology from companies to meet bleeding edge practitionners from academia to help them apply state of the art SAT practices.

• Armin Biere will explain how to efficiently translate the domain problem into a set of clauses, the input taken by the SAT solvers. The presentation will emphasize the importance of the encoding and present some preprocessing techniques available in the SAT solver Lingeling.
• In many cases, one cannot take the answer of the SAT solver for granted: the answer provided by the SAT solver should be validated by an independent tool. Marijn Heule will present the recent advances in checking UNSAT answers: both the concepts behind unsat proofs and the tool DRAT-trim will be presented.
• SAT solvers can be a specific part of a SAT based pipeline used to solve problems strictly hard that SAT. Joao Marques Silva will present the architecture of such "SAT-based" pipeline and will present three use cases: Counter Example Guided Abstraction Refinement (CEGAR) based QBF solving as found in the tool RaReQS, Core Guided MAXSAT solving as found in MSCG and Minimal Unsatisfiable Subformula computation as found in MUSer.
• SAT technology is at the heart of Satisfiability Modulo Theories (SMT) Roberto Sebastiani will present some simple useful theories and how to encode interesting problems into SMT with MathSAT 5.
• Solvers are usually parameterized, and different settings can lead to quite different behavior in practice. As such, a tedious task for the user is to optimize the settings of the solver for his particular needs (input). Experts (aka solvers designers) have usually enough knowledge about the solvers internals to provide settings good enough for a class of problems they are familiar with. This task is much more challenging for simple users of the solvers or experts on arbitrary problems. Fortunately, there exists now software to help the latter in that task. Marius Lindauer will introduce the Sequential Model-based Algorithm Configuration (SMAC) tool, a state-of-the-art algorithm configuration optimizer.

Other practitionners from the SAT community have already confirmed their attendance:

• Gilles Audemard and Laurent Simon (Glucose)
• Daniel Le Berre (Sat4j)
• ...

The event is meant to allow attendees to test the tools presented during the day. As such, people are warmly encouraged to bring their own laptop. Most of the presented software are available as Linux binaries. VirtualBox vitual machines with a flavor of Linux will be available on site for people using another operating system.

The participants of the "Industrial day" are also encoureaged and welcome to attend the sessions of the last day of the conference, on July 8, dedicated to applications and competitive events. That way, they could also get a taste of the brand new applications and bleeding edge solvers techniques.

SAT/SMT/AR summer school

Since 2011, a SAT/SMT summer school is organized each year to train students on recent topics of SAT and Satisfiability Modulo Theory. This year, the SAT/SMT summer school joins forces with the automated reasoning community to propose a SAT/SMT/AR summer school right before IJCAR. The summer school will take place from June 22 to June 25 in Lisbon, Portugal. IJCAR is taking place in Coimbra, Portugal, from June 27 to July 2. More information can be found on the summer school web site/