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 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.
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,
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.
The workshop will take place in July 19, 2026 as a part of FLoC 2026 (exact place/room TBA).
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.
The workshop welcomes several categories of submissions:
Original papers
are expected to describe original work on a topic of the
workshop.
This includes papers whose focus might be too narrow to be
published in a conference.
Both short original papers (up to 8 pages, excl. references)
and long original papers (8-15 pages, excl. references),
including system descriptions of SAT and related solver
technologies are welcome.
For paper submissions that have originally been submitted to a main conference of FLoC'26 (such as SAT) but did do not make it,
we may be able to consider the original reviews received from the FLoC conference for PoS reviewing.
We ask authors who want to submit such a paper to approach us; depending on the conference, we may request the authors to attach the reviews.
Please do not attach any reviews from another conference without a prior agreement.
Work-in-progress papers
are expected to describe less mature work on a topic of the
workshop with the purpose of gathering feedback from the community.
This may include papers already submitted to conferences or
journals, which should be clearly stated in the paper.
Submissions in this category are allowed to lack certain qualities that would usually be considered required for a complete paper (e.g., convincing experiments), but they should still have sufficient substance to allow for a meaningful (lightweight) peer reviewing process.
Presentation-only papers
are expected to describe work on a topic of the workshop that was
recently accepted or published to another conference or a
journal but may have been missed by the community (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.
Each submission will be reviewed by at least three members of the program committee.
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.
All deadlines are AOE and unified across all PoS tracks. They have been decided to allow the authors to submit rejected papers from FLoC conferences such as SAT.
One author of each accepted paper is expected to present it at the workshop in person.
Abstract submission deadline: May 7, 2026
Paper submission deadline: May 7, 2026May 10, 2026 (extended, final)
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