The success of solver technologies for declarative languages, such as SAT, in the last decade 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, among others the SAT competitions, QBF evaluations, MaxSAT evaluations, SMT evaluations, and ASP and CP competitions, 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 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 counter- parts, to meet, communicate, and discuss latest results. In particular, a central goal 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.

The year 2018 marks the 9th edition (PoS-18) of the Pragmatics of SAT workshop series, this time being affiliated with the Federated Logic Conference (FLoC). PoS-18 welcomed submissions falling into one of three categories: original, describing original work on a topic of the workshop, with the possibility of having a paper formally published in a volume of EasyChair Proceedings dedicated to PoS-18; work in progress, describing less mature work on a topic of the workshop to gather feedback from the community; and presentation only, describing work on a topic within the PoS-18 focus areas recently accepted or published to another conference.

Based on an open call for papers, the workshop received a total of 12 submissions, including eight into the original category, one as work-in-progress, and three for presentation only. All papers submitted as original work or as work in progress received at least three reviews, and furthermore, all submissions received at least two reviews. The presentation-only papers were mainly lightly reviewed for suitability and interest in terms of the PoS-18 audience. Based on the reviews provided by the PoS-18 program committee and the following PC discussion, the PC decided to accept six of the submissions as original papers:

• Competitive Sorter-based Encoding of PB-Constraints into SAT
  by Michal Karpinśki and Marek Piotrów,

• CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
  by Anastasia Leventi-Peetz, Oliver Zendel, Werner Lennartz and Kai Weber,

• Two flavors of DRAT
  by Adrian Rebola Pardo and Armin Biere,

• The Effect of Scrambling CNFs
  by Armin Biere and Marijn Heule,

• Tuning Parallel SAT Solvers
  by Thorsten Ehlers and Dirk Nowotka, and

• A Problem Meta-Data Library for Research in SAT
  by Markus Iser and Carsten Sinz,

as well as six submissions for presentation at the workshop:

• Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution- Based Phase Saving
  by Emir Demirovíc and Peter J. Stuckey (work in progress),

• Pseudo-Random Number Generators for Multi-Threaded Stochastic Local Search
  by Ali Asgar Sohanghpurwala and Peter Athanas (work in progress),

• Stedman and Erin Triples encoded as a SAT Problem
  by Andrew Johnson (work in progress),

• MLIC: A MaxSAT-Based framework for learning interpretable classification rules
  by Dmitry Malioutov and Kuldeep S. Meel (work submitted elsewhere),

• Divide and Conquer: Towards Faster Pseudo-Boolean Solving
  by Jan Elffers and Jakob Nordström (published at IJCAI'18), and

• Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
  by Jan Elffers, Jesus Giráldez-Cru, Stephan Gocht, Jakob Nordström and Laurent Simon (published at IJCAI'18).

Finally, as the PC Chairs of PoS-18, we would like to thank the PoS-18 program committee members for their timely and constructive reviewing work and the following discussions: Mario Alviano, Armin Biere, Bart Bogaerts, Vijay Ganesh, Marijn Heule, Antti Hyv ̈arinen, Alexey Ignatiev, Florian Lonsing, Ruben Martins, Nina Narodytska, and Olivier Roussel.