Pragmatics of SAT

a workshop of the 23nd International Conference on Theory and Applications of Satisfiability Testing

July 5 July 3, 2020, Alghero ,Italy in the cyberspace

News: July 4, 2020 Recordings of the presentations are now available.
News: July 3, 2020 74 participants to the first session, 64 for the second session.
News: June 17, 2020 Programme online.
News: June 7, 2020 workshop date change Since the event is virtual, the date of the workshop is no longer taking place the Sunday just before the conference but the previous working day, i.e. Friday July 3. To meet the SAT conference schedule, the workshop will take place between 4pm and 8pm CEST.
News: May 8, 2020 deadlines collision with FMCAD We have been told that the new abstract and paper deadlines were now colliding with FMCAD 2020 deadlines (which have been shifted by one month). We will thus accept papers until May 22. Please however submit your abstract as soon as possible to allow bidding by the PC.
News: April 29, 2020 deadlines extended We shifted the deadlines by one week. Note that informal proceedings will be made available to the attendees as usual and we are looking for a live streaming solution enabling live discussions.
News: April 27, 2020 PoS will be a virtual event PoS will definitely be a virtual event. We are still working out the details (date, organization, etc). So please consider submitting your work. The lively discussions you like during PoS will take place despite COVID19.
News: April 7, 2020 COVID19 Notice We are together with the conference organizers monitoring the COVID-19 situation. We will update this page as soon as a decision is made regarding the format of the conference and affiliated workshops (e.g. virtual event).

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:

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
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
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
  • CDF vs Cactus plots by Armin Biere
Video Work in progress SAT practitioner manifesto (github project, feel free to contribute with issues or pull requests)

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:

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

Programme Committee

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