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, 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 2025 edition is the sixteenth edition of the workshop. It takes place before the SAT conference (August 11, 2025) in Glasgow.

Topics

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

• efficient data structures
• techniques for debugging or certifying solvers
• visualisation of benchmarks structure
• monitoring solver behaviour
• evaluation of solvers
• domain specific encodings
• domain specific heuristics
• solver API
• system/library description
• new (successful) application of constraint-based technologies
• new (potential) use cases of constraint-based technologies
• application of machine learning in constraint solving
• scaling using multi-core or distributed technology
• reflection on past and projection of future of applied SAT research (position papers and talks are both welcome)

Programme/Venue

The workshop will take place on August 11, 2025 in Room BO LT2.

The proceedings of the workshop are published as joint proceedings together with the SMT'25 workshop by CEUR in Volume 4008.

Registration

Registration to the workshop will be available from the SAT'25 website.

Submission

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.
• 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.
• 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.
• SAT/CP Fast Track Original papers on topics related to PoS that did do not make it to SAT 2025 and CP 2025 will have the opportunity to be submitted late, as original papers. In this case, reviewing for PoS will also consider the SAT/CP reviews. Submissions in this category should be accompanied with the reviews received from SAT/CP.

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 EasyChair.

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

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.

• Abstract submission deadline: May 5, 2025 May 12, 2025 (all submissions except SAT/CP Fast Track)
• Paper submission deadline: May 12, 2025 May 19, 2025
• SAT/CP Fast Track submission deadline: May 30, 2025 June 1, 2025 (no separate abstract registration is needed)
• Notification to authors: June 20, 2025
• Workshop: August 11, 2025

Accepted presentations

Programme Committee

• Gilles Audemard, Université d'Artois
• Armin Biere, University of Freiburg
• Jip Dekker, Monash University
• Leroy Chew, TU Vienna
• Katalin Fazekas, TU Wien
• Marijn Heule, Carnegie Mellon University
• Alexey Ignatiev, Monash University
• Mikoláš Janota, Czech Technical University in Prague chair
• Vasco Manquinho, INESC-ID / IST, Universidade de Lisboa
• Alexander Nadel, NVIDIA and Technion
• Nina Narodytska, VMWare
• Aina Niemetz, Stanford University chair
• Mathias Preiner, Stanford University
• Mate Soos, Ethereum Foundation and National University of Singapore
• Peter Stuckey, Monash University

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.

Mikoláš Janota                                                        Aina Niemetz
Czech Technical University in Prague                                  Stanford University
Czech Institute of Informatics, Robotics and Cybernetics              Department of Computer Science
Jugoslávských partyzánů 1580/3                                        CoDa W348
160 00 Prague 6, Czechia                                              Stanford, CA 94305, USA
https://people.ciirc.cvut.cz/~janotmik/                               https://cs.stanford.edu/~niemetz/