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, colocated 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.

The 2023 edition is thus the fourteenth edition of the workshop dedicated to the practical aspects of SAT research.

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
• constraint solving and machine learning
• scaling using multi-core or distributed technology

Programme/Venue

The workshop will take place on July 4, 2023.

The post-proceedings of the workshop are published by CEURS-WS in Volume 3545

8:30 Opening
8:30-10:30 Optimization session
Tobias Paxian and Armin Biere	Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging Paper Software Data Slides
Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel and Dieter Vandesande	Certified Core-Guided MaxSAT Solving Slides
Gioni Mexi, Timo Berthold, Ambros Gleixner and Jakob Nordström	Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning Slides
Shunji Nishimura	Approximate-At-Most-k Encoding of SAT for Soft Constraints Software Slides
10:30-11:00 Coffee Break
11am-1pm Empirical session
Benjamin Kaiser , Robert Clausecker and Michael Mavroskoufis	Prioritised Unit Propagation by Partitioning the Watch Lists Paper Slides
Yoichiro Iida, Tomohiro Sonobe and Mary Inaba	An Empirical Study of the Effect of Learnt Clause on the Structural Measures of SAT problems Paper Slides
Vincent Vallade, Julien Sopena and Souheib Baarir	Enhancing State-of-the-Art Parallel SAT Solvers Through Optimized Sharing Policies Paper Slides
Alexander Hoen, Ambros Gleixner and Jakob Nordström	On Performance Variability in Pseudo-Boolean Solving and the Impact of Trivial Model Simplifications Slides
2pm-3:30pm Misc SAT session
Julian Danner, Bernhard Andraschko and Martin Kreuzer	Towards Efficient SAT Solving using XOR-OR-AND Normal Forms Slides
Sebastiaan Brand, Tim Coopmans and Alfons Laarman	Quantum graph-state transformation with SAT Paper Data Slides
Anthony Blomme, Daniel Le Berre , Anne Parrain and Olivier Roussel	Compressing UNSAT Search Trees with Caching: an update Slides
15:30-16:00 Coffee Break
4pm-6pm: position papers
Jan Gorzny	Towards Satisfactory Web3 Software Engineering Slides
Mathias Fleury and Daniela Kaufmann	Lifespan of SAT techniques Slides
Armin Biere , Mathias Fleury , Nils Froleyks and Marijn Heule	The SAT Museum Paper Slides
Jakob Nordstrom	A one-size-fits-all proof logging system? Slides
6pm Closing

Registration

Registration to the workshop will be available from SAT'23 web site.

Submission

The workshop welcomes several categories of submissions:

• Original papers describing original work on a topic of the workshop, including papers whose focus might be too narrow to be published in a conference. Short original papers, approximately 6-8 pages in length, including system descriptions of SAT and related solver technologies are also welcome.
• Work-in-progress papers describing less mature work on a topic of the workshop, to gather feedback from the community. It may include papers submitted to conferences or journals, which should be clearly stated in the paper.
• Presentation-only papers describing a work on a topic of the workshop recently accepted or published to another conference or a journal, but that the community may have missed (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.
• Position papers focused on 'looking back' from the present to the past on key developments in applied SAT research.
• Position talks looking from the present to the future, identifying some of the next major research challenges and promising directions for applied SAT research (abstract only).

Each submission will be reviewed by at least three members of the programme committee.

The papers must be submitted electronically through EasyChair as a PDF file using the CEURART one column style.

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.

This year, considering the very tight schedule between the main SAT conference authors notification (May 15) and the workshop (July 4), we will allow a SAT fast track for original papers, i.e. papers that do not make it to SAT on topics related to PoS will have the opportunity to be submitted late to PoS as original papers. In this case, reviewing for PoS will mostly be focused on the SAT reviews.

Important dates

The deadlines have been decided to allow the authors to get notified by the early registration deadline. Note that Alghero is a highly demanded venue during summer so it is important to book both travel and stay as early as possible.

• Abstract submission deadline: April 27, 2023 (all submissions except SAT fast track)
• Paper submission deadline: May 4 May 9, 2023
• SAT fast track paper submission deadline: May 18, 2023 (no separate abstract registration)
• Notification to authors: May 25, 2023
• Revised version due: June 21, 2023
• Workshop: July 4, 2023
• Post-proceedings deadline (if applicable): August 31, 2023

Accepted presentations

Programme Committee

• Armin Biere, University of Freiburg
• Katalin Fazekas, TU Wien
• Marijn Heule, Carnegie Mellon University
• Alexey Ignatiev, Monash University
• Mikoláš Janota, Czech Technical University in Prague
• Matti Jarvisalo, University of Helsinki chair
• Daniel Le Berre, University of Artois - CNRS chair
• Hidetomo Nabeshima, University of Yamanashi
• Aina Niemetz, Stanford University
• Tobias Paxian, University of Freiburg
• Olivier Roussel, University of Artois - CNRS
• Mate Soos

Sponsor

Pragmatics of SAT 2023 is supported by CEUR-WS.org which published its proceedings.

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.

Matti Järvisalo                               Daniel Le Berre
University of Helsinki                        Universite d'Artois
Department of Computer Science / HIIT         CNRS
P.O. Box 68, FI-00014, Finland                Rue Jean Souvraz SP 18 62307 Lens FRANCE
https://www.cs.helsinki.fi/u/mjarvisa/        http://www.cril.fr/~leberre