15th Pragmatics of SAT international workshop

a workshop of the 27th International Conference on Theory and Applications of Satisfiability Testing

August 20, 2024, Pune, India

July 24, 2024: Tentative Programme is available.
July 16, 2024: List of accepted presentations is added.
March 21, 2024: PC and Competition track details are added.
February 21, 2024: Web site is up.

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 two decades 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 paradigms, 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 eighth edition, colocated with CP and ICLP, was organized on a more general topic of ``Pragmatics of Constraint Reasoning". The ninth edition took place during the Federated Logic Conference in Oxford. The decade edition took place in Lisbon. The eleventh edition was fully virtual due to COVID19. The twelfth edition was mostly virtual for the same reason. The thirteenth edition ran for the fourth time during FLoC in Haifa. The fourteenth edition of the workshop was dedicated to the practical aspects of SAT research.

The 2024 edition is the fifteenth edition of the workshop. It takes place before the SAT conference (August 21-24) in Pune.

Topics

Main areas of interest include, but are not restricted to:

Programme/Venue

The workshop will take place on August 20, 2024.

8:50 - 9:00 Opening
9:00-10:30 Session 1
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen and Jakob Nordström Certified MaxSAT Preprocessing
Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian and Dieter Vandesande Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability
Dieter Vandesande, Jordi Coll, Chu-Min Li and Bart Bogaerts Certified Branch-and-Bound MaxSAT Solving
10:30-11:00 Tea & Coffee Break
11:00-12:30 Session 2
Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel and Yong Kiam Tan End-to-End Verification for Subgraph Solving
Daimy Van Caudenberg, Leandro Vendramin and Bart Bogaerts Enumerating Solutions to the Yang-Baxter Equation using SAT Modulo Symmetries
Matthieu Py, Arnauld Tuyaba, Laurent Deroussi, Nathalie Grangeon and Sylvie Norre Application of SAT to the Simple Assembly Line Balancing Problem with Power Peak Minimization
12:30-14:00 Lunch Break
14:00-15:30 Session 3
Florian Pollitt, Mathias Fleury, Carlos Ansótegui, Armin Biere and Supratik Chakraborty Transmuting clauses
Jannick Borowitz, Dominik Schreiber and Peter Sanders An Empirical Study on Learned Clause Overlaps In Distributed SAT Solving
Robin Coutelier To Link or not to Link? That is a Watch List!
15:30-16:00 Tea & Coffee Break
16:00-17:30 Session 4
Dominik Schreiber and Peter Sanders MallobSat: Scalable SAT Solving by Clause Sharing
Ole Lübke IGMaxHS - An Incremental MaxSAT Solver with Support for XOR Clauses
Mazigh Saoudi, Souheib Baarir, Julien Sopena and Thibault Lejemble PL-PRS-BVA-KISSAT in SAT Competition 2024
17:30-17:45 Closing

Registration

Registration to the workshop will be available from the SAT'24 web site.

Submission

The workshop welcomes several categories of submissions:

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 CEURART one column 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.

If enough original and competition solver description papers are accepted to the workshop (6+), we will have the opportunity to publish those papers on CEUR-WS proceedings. The papers will be made available open access under the CC BY 4.0 license after the workshop to allow the authors to take into account the feedback received during the workshop.

Important dates

The deadlines have been decided to allow the authors to get notified by the early registration deadline. One author of each accepted paper is expected to present it at the workshop in person.

Accepted presentations

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability
Florian Pollitt, Mathias Fleury, Carlos Ansótegui, Armin Biere and Supratik Chakraborty. Transmuting clauses
Dieter Vandesande, Jordi Coll, Chu-Min Li and Bart Bogaerts. Certified Branch-and-Bound MaxSAT Solving
Daimy Van Caudenberg, Leandro Vendramin and Bart Bogaerts. Enumerating Solutions to the Yang-Baxter Equation using SAT Modulo Symmetries
Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel and Yong Kiam Tan. End-to-End Verification for Subgraph Solving
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen and Jakob Nordström. Certified MaxSAT Preprocessing
Dominik Schreiber and Peter Sanders. MallobSat: Scalable SAT Solving by Clause Sharing
Robin Coutelier. To Link or not to Link? That is a Watch List!
Ole Lübke. IGMaxHS - An Incremental MaxSAT Solver with Support for XOR Clauses
Matthieu Py, Arnauld Tuyaba, Laurent Deroussi, Nathalie Grangeon and Sylvie Norre. Application of SAT to the Simple Assembly Line Balancing Problem with Power Peak Minimization
Jannick Borowitz, Dominik Schreiber and Peter Sanders. An Empirical Study on Learned Clause Overlaps In Distributed SAT Solving
Mazigh Saoudi, Souheib Baarir, Julien Sopena and Thibault Lejemble. PL-PRS-BVA-KISSAT in SAT Competition 2024 Competition Solver Description

Programme Committee

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.

Alexey Ignatiev                               Katalin Fazekas
Monash University                             TU Wien
Faculty of IT                                 Institute of Logic and Computation
20 Exhibition Walk,                           Favoritenstraße 9–11,
Clayton VIC 3168, Monash, Australia           1040, Vienna, Austria
https://alexeyignatiev.github.io              https://kfazekas.github.io