a workshop of the
29th International Conference on Theory and Applications of Satisfiability Testing
and the Federated Logic Conference 2026
July 19, 2026, Lisbon, Portugal
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.
The success of solver technology for declarative languages, such as SAT, in the last 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 a good theoretical knowledge about the design of those solvers, i.e., how all its components interact, and a deep practical knowledge about how to implement such components efficiently.
The SAT community organizes regularly competitive events (SAT competition or SAT Races, QBF Evaluation, MaxSAT evaluation, PB Evaluation, etc.) to evaluate available solvers on a wide range of problems. The winners of those events set regularly new standards in the area. However, even 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. An important aim of the workshop is to allow researchers to share some gory technical details about their systems that they usually cannot share within a main conference.
The workshop also fosters discussion and dissemination of many further practical aspects surrounding SAT, including but not limited to solving interfaces, monitoring and debugging of solvers, methodological considerations, and meta topics such as the past and future of applied SAT research itself.
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,
collocated 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, Israel.
The fourteenth edition of the workshop was dedicated to the practical aspects of SAT research.
The fourteenth edition of the workshop was dedicated to the practical aspects of SAT research.
The fifteenth edition took place before the SAT conference in Pune, India.
The sixteenth edition took place before the SAT and CP conferences in Glasgow, Scotland.
The 2026 edition is the seventeenth edition of the workshop. It takes place during the Federated Logic Conference in Lisbon.
Main areas of interest include, but are not restricted to:
The workshop will take place in July 19, 2026 (exact date and place TBD).
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.
We plan to publish the proceedings of the workshop via CEUR-WS proceedings, possibly by joining forces with another, related FLoC workshop.
Registration to the workshop will be available from the FLoC'26 website.
The workshop welcomes several categories of submissions:
Each submission will be reviewed by at least three members of the program committee.
The papers must be submitted as a PDF file using the CEURART one column style.
The papers must be submitted electronically through HotCRP.
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.
The deadlines are unified across all PoS tracks. They have been decided to allow the authors to submit rejected papers from FLoC conferences such as SAT and to get notified before the FLoC early registration deadline. One author of each accepted paper is expected to present it at the workshop in person.
For any questions related to the workshop, the preferred solution to contact the organizers is to send
an email to pos at pragmaticsofsat.org.
Bart Bogaerts Dominik Schreiber Declarative Languages and Artificial Intelligence section Scalable Automated Reasoning Department of Computer Science Institute of Information Security and Dependability KU Leuven Karlsruhe Institute of Technology Celestijnenlaan 200A, room 01.14 Room 208, Am Fasanengarten 5 B-3001 Heverlee 76131 Karlsruhe, Germany