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 paradignms, 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 2020 edition is thus the eleventh edition of the workshop dedicated to the practical aspects of SAT research.

Topics

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

• techniques for debugging or certifying solvers
• visualisation of benchmarks structure
• monitoring solver behaviour
• evaluation of solvers
• efficient data structures
• domain specific encodings
• taking into account multi-core technology
• domain specific heuristics
• new application of constraint-based technologies
• new use cases of constraint-based technologies
• system/library description
• solver API
• constraint solving and machine learning

Programme/Venue

The workshop will take place virtually, using zoom technology. The workshop is open to registered participants (at no charge).

All the information to connect to the session will be sent by mail to registered participants.

The presentations will be live, not pre-recorded, with the possibility to interact with the speaker during the talk.

4pm-4:15pm	Introduction to PoS virtual event (rules for speaking, interacting with speaker, etc)
4:15pm	Slot 1: solvers design
4:15pm-4:40pm	Target Phases by Armin Biere and Mathias Fleury original work We discuss and evaluate the idea of target phases introduced first in CaDiCaL in 2019 and also ported to our latest SAT solver Kissat. Target phases provide a heuristic to choose the value assigned to decision variables. This technique is an extension of phase saving. It extends promising assignments derived by the solver towards full models. Combined with alternatively applying series of Glucose-style and Luby-style restart, the technique is particularly effective on satisfiable instances. Software Data Video Slides JAIR'22 paper
4:45pm-5:10pm	Adapting CDCL Strategies for PB Solvers by Romain Wallon work in progress Current implementations of pseudo-Boolean (PB) solvers are based on the CDCL architecture, which is the central component of modern SAT solvers. In addition to clause learning, this architecture comes with many strategies that help the solver find its way through the search space, either to a solution or to an unsatisfiability proof. Particularly important are the decision heuristic, but also other features like learned clause deletion or restarts. Currently, these strategies are mostly used "as is" in PB solvers, without considering the particular form of the PB constraints they deal with. In this paper, we introduce new ways of adapting these strategies to better take into account the specificities of such constraints, especially regarding their weights and propagation properties. In particular, our experiments show that carefully considering these criteria may have a significant impact on the performance of the solver. Software Video SAT'21 paper SAT'21 preprint
5:15pm-5:40pm	Towards Faster Reasoners by using Transparent Huge Pages by Johannes K. Fichte, Norbert Manthey, Andre Schidler and Julian Stecklina work in progress Various state-of-the-art automated reasoning (AR) tools are widely used as backend tools in research of knowledge representation and reasoning as well as in industrial applications. In testing and verification, those tools often run continuously or nightly. In this work, we present an approach to reduce the runtime of AR tools by 10% on average and up to 20% for long running tasks. Our improvement addresses the high memory usage that comes with the data structures used in AR tools, which are based on conflict driven no-good learning. We establish a general way to enable faster memory access by using the memory cache line of modern hardware more effectively. Therefore, we extend the standard C library (glibc) by dynamically allowing to use a memory management feature called huge pages. Huge pages allow to reduce the overhead that is required to translate memory addresses between the virtual memory of the operating system and the physical memory of the hardware. In that way, we can reduce runtime, which in turn decreases costs of running AR tools and applications with similar memory access patterns simply by linking the tool against this new glibc library when compiling it. In every day industrial applications, runtime savings allow to include more detailed verification tasks or simply save money or energy during nightly software builds. To back up the claimed speed-up, we present experimental results for tools that are commonly used in the AR community, including the domains ASP, BMC, MaxSAT, SAT, and SMT. Software Video Slides
5:40-6pm	virtual coffee break, discussions between attendees
6pm	Slot2: applications and tools
6pm-6:25pm	Determining Affine and Extended Affine Equivalence of Boolean Functions with SAT by Luis Moraes and Rakesh Verma work in progress Many cryptographically desirable properties of Boolean functions are preserved by affine and extended affine equivalence. Thus, being able to determine equivalence between Boolean functions efficiently is useful in cryptography. We present an encoding of affine and extended affine equivalence into SAT. We experiment with different encodings and demonstrate how implicit constraints affect performance. In addition, we draw parallels between known algorithms and these encodings. Benchmarks Video
6:30pm-655pm	Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling by Mate Soos, Stephan Gocht and Kuldeep S. Meel CAV 2020 paper presentation Given a Boolean formula, the problem of counting seeks to estimate the number of solutions of F while the problem of uniform sampling seeks to sample solutions uniformly at random. Counting and uniform sampling are fundamental problems in computer science with a wide range of applications ranging from constrained random simulation, probabilistic inference to network reliability and beyond. Despite intense theoretical and empirical investigations, development of scalable techniques for sampling and counting without sacrificing theoretical guarantees remains the holy grail. The past few years have witnessed the rise of hashing-based approaches that use XOR-based hashing and employ SAT solvers to solve the resulting CNF formulas conjuncted with XOR constraints. Since over 99% of the runtime of hashing-based techniques is spent inside the SAT queries, improving CNF-XOR solvers has emerged as a key challenge. In this paper, we identify the key performance bottlenecks in the recently proposed BIRD architecture, and we focus on overcoming these bottlenecks by accelerating the XOR handling within the SAT solver and on improving the solver integration through a smarter use of (partial) solutions. We integrate BIRD2 with the state of the art approximate model counter, ApproxMC3, and the state of the art almost-uniform model sampler UniGen2. Through an extensive evaluation over a large benchmark set of over 1896 instances, we observe that BIRD2 leads to consistent speed up for both counting and sampling, and in particular, we solve 77 and 51 more instances for counting and sampling respectively. Software Video
7pm-7:25pm	Metrics: Towards a Unified Library for Experimenting Solvers by Thibault Falque, Romain Wallon and Hugues Wattez work in progress When developing a SAT solver, one of the most important parts is to perform experiments so as to evaluate its performance. Most of the time, this process remains the same, so that everybody collects almost the same statistics about the solver execution. However, how many scripts are there to retrieve experimental data and draw scatter or cactus plots? Probably as many as researchers in the domain. Based on this observation, this paper introduces Metrics, a Python library, aiming to unify and make easier the analysis of solver experiments. The ambition of Metrics is to provide a complete toolchain from the execution of the solver to the analysis of its performance. In particular, this library simplifies the retrieval of experimental data from many different inputs (including the solver's output), and provides a nice interface for drawing commonly used plots, computing statistics about the execution of the solver, and effortlessly organizing them (e.g., in Jupyter notebooks). In the end, the main purpose of Metrics is to favor the sharing and reproducibility of experimental results and their analysis. Software Data Video
7:30-8pm	Slot 3: lightning talks
	Two minutes two slides talks to foster discussions. First come first served, topics may include open questions, detailed issues related to PoS, ads on recent work, etc. Please send your slides to pos20@easychair.org by July 2nd A Baby’s Day Out in the SAT World by Kuldeep S. Meel Work in progress SAT practitioner manifesto (github project, feel free to contribute with issues or pull requests) CDF vs Cactus plots by Armin Biere Video

Registration

Registration for the workshop is available on the main conference web site.

Registration for the workshop is free of charge but mandatory for organization purposes.

Submission

The workshop welcomes three categories of papers:

• 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.
• Presentation-only papers describing a work on a topic of the workshop recently accepted or published to another conference, 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.

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 EasyChair proceedings style. Each submission is limited to 14 pages, plus references.

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.

Unlike previous editions, there will be no workshop proceedings.

High-quality original papers will be selected by the PC for fast-track reviewing for potential publication in Journal on Satisfiability, Boolean Modeling and Computation (JSAT), subject to a second formal review process.

Important dates

• Abstract submission deadline: April 30 May 7, 2020 (soft, submit ASAP)
• Paper submission deadline: May 7 May 15 May 22, 2020
• Notification to authors: May 31 June 7, 2020
• Final version due: June 19 June 26, 2020
• Workshop: July 5 July 3, 2020

Programme Committee

• Jeremias Berg, University of Helsinki / HIIT
• Armin Biere, Johannes Kepler University Linz
• Marijn Heule, Carnegie Mellon University
• Hidetomo Nabeshima, University of Yamanashi
• Alexey Ignatiev, Monash University
• Matti Jarvisalo, University of Helsinki chair
• Daniel Le Berre, University of Artois - CNRS chair
• Ines Lynce, INESC-ID/IST, Universidade de Lisboa
• Ruben Martins, Carnegie Mellon University
• Aina Niemetz, Stanford University
• Olivier Roussel, University of Artois - CNRS

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