The success of solver technologies for declarative languages, such as Boolean satisfiability (SAT), in the last two decades is mainly due to both the availability of numerous eficient solver implementations and to the growing number of problems that can eficiently be solved through the declarative approach. Designing eficient 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 eficient and robust solvers. Several competitive events are regularly organized for diferent declarative solving paradigms, including SAT competitions, QBF evaluations, MaxSAT evaluations, SMT, ASP and CP competitions, among others, 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 Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying 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. PoS workshops have been by standard been organized in conjunction with the yearly instantiations of International Conferences on Theory and Applications of Satisfiability Testing (SAT). The year 2023 constituted the 14th edition on the Pragmatics of SAT workshop series, following the previous editions that took place in Edinburgh, UK (2010, as part of the Federated Logic Conference FLoC), Ann Arbor, MI, USA (2011), Trento, Italy (2012), Helsinki, Finland (2013), Vienna, Austria (2014, as part of the Federated Logic Conference FLoC and Vienna Summer of Logic) Austin, TX, USA (2015), Bordeaux, France (2016), Melbourne, Australia (2017, co-located with IJCAI, SAT, CP, and ICLP under the title “Pragmatics of Constraint Reasoning”), Oxford, UK (2018, as part of the Federated Logic Conference FLoC), Lisbon, Portugal (2019, celebrating 10 years of PoS), online during the COVID-19 years 2020-2021, and Haifa, Israel (2022, again as part of the Federated Logic Conference FLoC). PoS 2023 took place in Alghero, Italy on July 4. In additional to the standard call for papers, PoS 2023 included a special call for 'Looking 20/30 years back & 20 forward' on SAT Pragmatics, inviting submissions focused on 'looking back' from the present to the past on key developments in applied SAT research, as well as position talks looking from the present to the future, identifying some of the next major research challenges and promising directions for applied SAT research. PoS 2023 received a total of 15 submissions, out of which six (including one position paper answering the special call on 'Looking 20/30 years back & 20 forward') were ifnally selected by the program committee for inclusion in the present CEUR-WS proceedings as regular papers. Two of the included papers were accepted directly after first-round reviews, while the other four were accepted after a second round of reviews after the workshop took place. The authors of all papers had the opportunity to revise the submitted versions after the workshop based on reviewer comments and
feedback received at the workshop. The papers cover a range of topics concerning pragmatics of SAT: SAT encodings for graph transformations motivated by quantum computing, implementation of unit propagation, parallel SAT solving, impact of clause learning on problem structure, testing and debugging of MaxSAT solvers, and evaluation of historical progress in SAT solvers.
The PoS 2023 program committee consisted of • Armin Biere (University of Freiburg, Germany), • Katalin Fazekas (TU Wien, Austria), • Marijn Heule (Carnegie Mellon University, USA), • Alexey Ignatiev (Monash University, Australia), • Mikolas Janota (Czech Technical University in Prague, Czech Republic), • Matti Ja¨rvisalo (University of Helsinki, Finland — PC Chair), • Daniel Le Berre (University of Artois - CNRS, France — PC Chair), • Hidetomo Nabeshima (University of Yamanashi, Japan), • Aina Niemetz (Stanford University, USA), • Tobias Paxian (University of Freiburg, Germany), • Olivier Roussel (University of Artois - CNRS, France), • Mate Soos.
We thank the PC for their valuable work on making PoS yet again a success.