News: presentations are now available.
Purpose
The aim of the Pragmatics of SAT (PoS) workshop is to allow researchers concerned with the design of efficient SAT and CP
solvers at large or SAT encodings/CP formulation to meet and discuss about their latest results. The workshop is also
the place for users of SAT and CP technology to present their applications. The collocation of CP, ICLP and SAT this year is
a unique opportunity to enlarge the audience of the workshop to the whole constraint community, thus the specific name ``Pragmatics
of Constraint Reasoning".
Background
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. There are also numerous
CP systems available today, in various languages, some of them hybridizing CP and SAT. Designing efficient solvers requires
both a good theoretical knowledge about the design of those solvers, i.e. how are interacting all its components, and
a deep practical knowledge about how to implement efficiently such components. The CP community organizes regularly competitive
events (SAT competition or SAT Races, QBF Evaluation, MAXSAT evaluation, Minizinc Challenge, etc.) to evaluate available
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. The aim of the workshop is to allow researchers to share some gory technical details about their
systems that they cannot usually share within the main SAT or CP conference.
History
The first workshops dedicated to the practical aspects of constraint programming were organized under the series TRICS: Techniques
foR Implementing Constraint programming Systems. The workshops were organized in 2000 (Singapore), 2002 (Ithaca), 2010
(St Andrews) and
2013 (Uppsala). The first edition of PoS took place during
FLoC 2010. The second edition took place before SAT 2011, in Ann Arbor. The third edition took place on June 16, 2012,
between the second SAT/SMT Summer School (June 12 to 15) and the SAT conference (June 17-20). The fourth edition took
place on July 8, once again between the SAT/SMT summer school and the SAT conference. The fifth edition took place during
the Vienna Summer of Logic, just before the SAT conference. The sixth edition took place before the SAT conference, in
Austin. The last edition took place before the SAT conference, in Bordeaux.
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 constraint-based technologies
- new use cases of constraint-based technologies
- system/library description
- SAT/SMT/CP/LP solver API
The workshop will take place at the Melbourne Convention and Exhibition Centre, in Room 107. See the conference booklet for details to locate the room.
All technical presentations have a 30 minute slot including questions. All invited talks (competitive events) have a one hour slot including questions.
| 9h Opening |
|---|
| 9h-10h Session 1: Cutting Planes |
|---|
| Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob Nordström
| In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (slides PDF) |
| Jan Elffers, Jesús Giráldez-Crú, Jakob Nordström and Marc Vinyals
| Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (slides PDF) |
| 10h00-10h30 Coffee Break |
|---|
| 10h30-12h Session 2: Back to SAT |
|---|
| Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Liang, Krzysztof Czarnecki and Vijay Ganesh | Empirically Relating Complexity-theoretic Parameters with SAT Solver Performance (slides PPTX) |
| Tom van Dijk, Rüdiger Ehlers and Armin Biere | Revisiting Decision Diagrams for SAT (slides PDF) |
| Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail
| A SAT-Based Approach for Solving the Minimal S5-Satisfiability Problem (slides PDF) |
| 12h-13h30 Lunch (not provided) |
|---|
| 13h30-15h30 Session 3: competitive event discussions |
|---|
| Luca Pulina | QBF-Eval (slides PDF) |
| Christophe Lecoutre | Structure Preserved by XCSP3: an Interesting Feature for Competitions (slides PDF) |
| 15h30-16h Coffee Break |
|---|
| 16h-16h30 PoS/PoCR @ FLoC 18 |
|---|
| 16h30 Closing |
|---|
There is no specific registration for PoCR. Registration for the workshops day is available on from one of the conference hosting conference (SAT, CP, ICLP) and allows to attend any workshop that day.
The workshop welcomes three categories of papers:
- Regular papers describing original work on a topic of the workshop, whose focus
is too narrow to be published in a conference.
- Work in progress papers describing less mature work on a topic of the workshop,
to gather feedback from the community. Those papers will be distributed to the audience of the workshop only.
- Presentation papers describing a work on a topic of the workshop published recently
to another conference, but that the community may have missed. Those papers will only be evaluated on their relevance
to the workshop, and will not be distributed to the audience (a link to the original paper will be given).
Each submission will be reviewed by at least three members of the programme committee.
The papers must be submitted electronically through EasyChair
as a PDF file using the EasyChair proceedings style. Each submission is limited to 14 pages, plus references.
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.
- Abstract submission deadline: June 23 28, 2017
- Paper submission deadline: June 28, 2017
- Notification to authors: July 14, 2017
- Final version due: August 18, 2017
- Workshop: August 28, 2017
- Armin Biere, Johannes Kepler University Linz
- Mats Carlsson, SICS
- Daniel Le Berre, CNRS - Université d'Artois
- Joao Marques-Silva, University of Lisbon
- Ruben Martins, University of Texas at Austin
- Laurent Michel, University of Connecticut
- Laurent Perron, Google France
- Charles Prud'Homme, TASC (CNRS/INRIA), Mines Nantes
- Luca Pulina, POLCOMING - University of Sassari
- Jean-Charles Regin, University Nice-Sophia Antipolis / I3S / CNRS
- Olivier Roussel, CNRS - Université d'Artois
- Torsten Schaub, University of Potsdam
- Pierre Schaus, UC Louvain
- Takehide Soh, Information Science and Technology Center, Kobe University
For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to pocr at pragmaticsofsat.org.
Daniel Le Berre Pierre Schaus
Universite d'Artois UC Louvain
CNRS ICTeam institute
Rue Jean Souvraz SP 18 62307 Lens FRANCE Place Sainte Barbe 2, 1348 Louvain-la-Neuve
http://www.cril.fr/~leberre https://www.info.ucl.ac.be/~pschaus/