Chers collègues,
Pour la première fois en 19 éditions, la conférence internationale
annuelle dédiée au problème SAT (SAT 2016) va se dérouler à Bordeaux, au
LaBRI, du 5 au 8 juillet 2016.
Une journée d’ateliers précède la conférence le lundi 4 juillet, et une
journée spécifique pour les utilisateurs de la technologie suit la
conférence.
La dernière journée de la conférence est dédiée aux applications de SAT
et aux diverses compétitions organisées par la communauté scientifique.
Nous espérons que ce programme permettre à ceux qui souhaitent en savoir
plus sur le sujet de satisfaire leur curiosité.
*La date limite pour le tarif d’inscription préférentiel est demain,
vendredi 27 mai.*
Cordialement,
Daniel Le Berre
———————————————————————-
CALL FOR PARTICIPATION
« The SAT week »
Bordeaux, France, July 4-9, 2016
including
Nineteenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
— SAT 2016 —
July 5-8, 2016
SAT 2016 affiliated workshops
July 4, 2016
« Solve it with SAT! » Industrial day
July 9, 2016
———————————————————————–
The International Conference on Theory and Applications of
Satisfiability Testing (SAT) is the premier annual meeting for
researchers focusing on the theory and applications of the propositional
satisfiability problem, broadly construed. In addition to plain
propositional satisfiability, it also includes Boolean optimization
(such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean
Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint
Programming (CP) for problems with clear connections to Boolean-level
reasoning.
Many hard combinatorial problems can be tackled using SAT-based
techniques including problems that arise in Formal Verification,
Artificial Intelligence, Operations Research, Computational Biology,
Cryptography, Data Mining, Machine Learning, Mathematics, et cetera.
Indeed, the theoretical and practical advances in SAT research over the
past twenty years have contributed to making SAT technology an
indispensable tool in a variety of domains.
SAT 2016 aims to further advance the field by soliciting original
theoretical and practical contributions in these areas with a clear
connection to Satisfiability. Specifically, SAT 2016 invites scientific
contributions addressing different aspects of SAT interpreted in a broad
sense, including (but not restricted to) theoretical advances (such as
exact algorithms, proof complexity, and other complexity issues),
practical search algorithms, knowledge compilation, implementation-level
details of SAT solvers and SAT-based systems, problem encodings and
reformulations, applications (including both novel application domains
and improvements to existing approaches), as well as case studies and
reports on findings based on rigorous experimentation.
SAT 2016 takes place in the nice city of Bordeaux, which is located in
the South West of France. Bordeaux is well-known to be the world wine
capital, and also ranked UNESCO town.
PROGRAMME
=========
INVITED SPEAKERS
—————-
We are honored to announce the following invited speakers at SAT’16:
– Phokion Kolaitis, Santa Cruz, USA: Coping with Inconsistent
Databases: Semantics, Algorithms, and Complexity
– David Monniaux, Grenoble, France: Satisfiability Testing, a
Disruptive Technology in Program Verification
– Torsten Schaub, Postdam, Germany (EurAI-sponsored invited talk):
From SAT to ASP and back!?
siteØ](http://sat2016.labri.fr).
TECHNICAL PROGRAMME
——————-
The list of accepted papers is [available
online](http://sat2016.labri.fr/#accepted).
A tentative schedule is available through [EasyChair Smart
Program](http://easychair.org/smart-program/SAT2016/).
As in previous years, the SAT conference hosts several competitive
events which run before the conference and whose results are disclosed
during the conference.
This year, the following competitive events will be organized:
– [SAT competition](http://baldur.iti.kit.edu/sat-competition-2016/)
– [MAXSAT evaluation](http://www.maxsat.udl.cat)
– [QBF evaluation](http://www.qbflib.org/qbfeval16.php)
– [PB Competition](http://www.cril.univ-artois.fr//PB16/)
WORKSHOPS (July 4)
==================
The day before the conference, Monday July 4th, will be a workshop day.
– [Seventh Pragmatics of SAT international
workshop](http://www.pragmaticsofsat.org/2016/)
– [International Workshop on Quantified Boolean Formulas
(QBF’16)](http://www.satlive.org/2015/12/22/qbf16.html)
– [Graph Structure and Satisfiability
Testing](https://www.ac.tuwien.ac.at/structsat2016/)
Specific details for each workshop can be found on their respective web
sites.
INDUSTRIAL DAY: SOLVE IT WITH SAT! (July 9)
===========================================
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](http://fmv.jku.at/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](http://fmv.jku.at/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](http://www.cs.utexas.edu/~marijn/) will present the recent
advances in checking UNSAT answers: both the concepts behind unsat
proofs and the tool
[DRAT-trim](http://www.cs.utexas.edu/~marijn/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](http://www.di.fc.ul.pt/~jpms/) 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](http://sat.inesc-id.pt/~mikolas/sw/areqs/), Core Guided
MAXSAT solving as found in
[MSCG](http://logos.ucd.ie/wiki/doku.php?id=mscg) and Minimal
Unsatisfiable Subformula computation as found in
[MUSer](http://logos.ucd.ie/wiki/doku.php?id=muser).
– SAT technology is at the heart of Satisfiability Modulo Theories
(SMT) [Roberto Sebastiani](http://disi.unitn.it/rseba/) will present
some simple useful theories and how to encode interesting problems
into SMT with [MathSAT 5](http://mathsat.fbk.eu).
– 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](http://aad.informatik.uni-freiburg.de/people/lindauer/index.html)
will introduce the [Sequential Model-based Algorithm Configuration
(SMAC)](http://www.ml4aad.org/algorithm-configuration/smac/) tool, a
state-of-the-art algorithm configuration optimizer.
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.
REGISTRATION
============
are available on the conference website.
Note that:
– Registration rate (in Euros) depends of the status of the
participant: student/academic/other
– Early registration rate (180/350/450) ends on May 27th;
– Late registration rate (250/420/520) ends on June 21st;
– On-site registration will be possible (300/480/590).
Attendance to the workshops or to the industrial day requires an
additional fee of 50€ per day before the conference, or 80€ on site.
ORGANIZATION
============
PROGRAM CHAIRS
————–
– Nadia Creignou Aix-Marseille Université, LIF-CNRS France
– Daniel Le Berre Université d’Artois, CRIL-CNRS France
LOCAL CHAIR
———–
– Laurent Simon Bordeaux INP, University of Bordeaux, LaBRI-CNRS,
France
PROGRAM COMMITTEE
—————–
– Fahiem Bacchus University of Toronto
– Yael Ben-Haim IBM Research
– Olaf Beyersdorff University of Leeds
– Armin Biere Johannes Kepler University
– Nikolaj Bjorner Microsoft Research
– Maria Luisa Bonet Universitat Politecnica de Catalunya
– Sam Buss UCSD
– Nadia Creignou Aix-Marseille Université, LIF-CNRS
– Uwe Egly TU Wien
– John Franco University of Cincinnati
– Djamal Habet Aix-Marseille Université, LSIS-CNRS
– Marijn Heule The University of Texas at Austin
– Holger Hoos University of British Columbia
– Frank Hutter University of Freiburg
– Mikolas Janota Microsoft Research
– Matti Järvisalo University of Helsinki
– Hans Kleine Büning University of Paderborn
– Daniel Le Berre Université d’Artois, CRIL-CNRS
– Ines Lynce INESC-ID/IST, University of Lisbon
– Marco Maratea DIBRIS, University of Genova
– Joao Marques-Silva Faculty of Science, University of Lisbon
– Stefan Mengel CRIL-CNRS
– Alexander Nadel Intel
– Nina Narodytska Samsung Research America
– Jakob Nordström KTH
– Albert Oliveras Technical University of Catalonia
– Roberto Sebastiani DISI, University of Trento
– Martina Seidl Johannes Kepler University Linz
– Yuping Shen Institute of Logic and Cognition, Sun Yat-sen University
– Laurent Simon Bordeaux INP, University of Bordeaux, LaBRI-CNRS
– Takehide Soh Information Science and Technology Center, Kobe
University
– Stefan Szeider TU Wien
– Allen Van Gelder University of California, Santa Cruz
CONTACT
=======
sat2016@easychair.org
———————————————————————
Desinscription: envoyez un message a: bull-ia-unsubscribe@gdria.fr
Pour obtenir de l’aide, ecrivez a: bull-ia-help@gdria.fr