a workshop of the 23nd International Conference on Theory and Applications of Satisfiability Testing
July 5 July 3, 2020, Alghero ,Italy in the cyberspace
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.
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.
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.
Main areas of interest include, but are not restricted to:
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|
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
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
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|
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
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.
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
questions, detailed issues related to PoS, ads on recent work, etc. Please send your slides to
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.
The workshop welcomes three categories of papers:
Each submission will be reviewed by at least three members of the programme committee.
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.
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