Scientific context

Purpose

The aim of the Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying Boolean satisfiability (SAT) solvers and related solver technologies, including but not restricting to satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP) as well as their optimization counterparts, to meet, communicate, and discuss latest results.

Background

The success of solver technologies for declarative languages, such as SAT, in the last decade is mainly due to both the availability of numerous efficient solver implementations and to the growing number of problems that can efficiently be solved through the declarative approach. Designing efficient solvers requires both understanding of the fundamental algorithms underlying the solvers, as well as in-depth insights into how to implement the algorithms for obtaining efficient and robust solvers.

Several competitive events are regularly organized for different declarative solving paradignms, including SAT competitions QBF evaluations, MaxSAT evaluations, SMT, ASP and CP competitions, etc., to evaluate available solvers on a wide range of problems. The winners of such 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 both fundamental theoretical insights into practical solvers, as well as new implementation-level insights and 'gory' technical details about their systems that may at times be difficult to publish in the main conferences on the declarative solving paradigms.

History

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 seventh edition took place before the SAT conference, in Bordeaux. The last edition, colocated with CP and ICLP, was organized on a more general topic of ``Pragmatics of Constraint Reasoning".

Topics

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
• solver API

Programme/Venue

The detailed programme of the workshop is available from Easychair.

The workshop will take place at the Mathematical Institute, Oxford.

The proceedings of the workshop are now available in the Easychair Proceedings in Computing series.

Registration

Registration to the workshop is made from FLoC 2018 web page

Submission

The workshop welcomes three categories of papers:

• Original papers describing original work on a topic of the workshop, including papers whose focus might be too narrow to be published in a conference. If the number of accepted original papers warrants this, the accepted papers in this category will be formally published as a volume in the EasyChair Proceedings in Computing series (to be confirmed).
• 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-only papers describing a work on a topic of the workshop recently accepted or published to another conference, but that the community may have missed (including, e.g., domain-specific applications of declarative solvers at the respective domain-specific conferences). Submissions to this category will be evaluated only 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.

Important dates

• Abstract submission deadline: April 8 April 15, 2018
• Paper submission deadline: April 15 April 20, 2018
• Notification to authors: May 15, 2018
• Final version due: May 25, 2018
• Workshop: July 7, 2018

Programme Committee

• Mario Alviano, University of Calabria
• Armin Biere, Johannes Kepler University Linz
• Bart Bogaerts, KU Leuven
• Vijay Ganesh, University of Waterloo
• Marijn Heule, The University of Texas at Austin
• Antti Hyvärinen, University of Lugano
• Alexey Ignatiev, University of Lisbon
• Matti Jarvisalo, University of Helsinki chair
• Daniel Le Berre, University of Artois - CNRS chair
• Florian Lonsing, Vienna University of Technology
• Ruben Martins, CMU
• Nina Narodytska, VMWARE Research
• Olivier Roussel, University of Artois - CNRS

Contact

For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to pos at pragmaticsofsat.org.

Matti Järvisalo                               Daniel Le Berre
University of Helsinki                        Universite d'Artois
Department of Computer Science / HIIT         CNRS
P.O. Box 68, FI-00014, Finland                Rue Jean Souvraz SP 18 62307 Lens FRANCE
https://www.cs.helsinki.fi/u/mjarvisa/        http://www.cril.fr/~leberre