Pragmatics of SAT decade edition

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

July 8, 2019, Lisbon, Portugal

News: July 19, 2019 All slides are now available.

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 2019 edition is thus the tenth edition of the workshop, marking a decade of meetings dedicated to the practical aspects of SAT research.

Topics

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

Programme/Venue

SAT: Disruption, Demise and Resurgence by Joao Marques-Silva

Joao Marques-Silva

Decade invited talk When assessing the evolution of SAT research over the last two decades, two rather different perspectives can be offered. On the one hand, some would argue that progress in SAT solvers has mostly stalled, with the most significant progress observed around two decades ago. This talk offers the other perspective, and contends that SAT has become a mature area of research, with endless and far-reaching opportunities. The talk highlights the remarkable progress enabled by SAT reasoners over the last decade, covering an ever-increasing range of application areas. Concrete examples include solving optimization, quantification and enumeration problems, targeting first-order, modal and description logics, devising novel techniques for analyzing inconsistency and, more recently, applying SAT-inspired algorithms in explainable AI.

Schedule

8:50 Welcome
9:00-10:30 Pseudo-Boolean Reasoning
Jan Elffers and Jakob Nordström. On-the-fly cardinality detection (WIP, slides PDF)
Daniel Le Berre, Pierre Marquis, Stefan Mengel and Romain Wallon. On Irrelevant Literals in Pseudo-Boolean Constraint Learning (WIP, slides PDF)
Stephan Gocht, Jakob Nordstrom and Amir Yehudayoff. On Division Versus Saturation in Pseudo-Boolean Solving (IJCAI'19 paper presentation, slides PDF)
10:30-11:00 Coffee break
11:00-12:30 SAT Solving
Vadim Ryvchin and Alexander Nadel. Flipped Recording (slides PDF)
Jan Elffers and Jakob Nordström. Visualizing CDCL VSIDS and phase values (WIP, slides PDF)
Katalin Fazekas, Daniela Kaufmann and Armin Biere. Ranking Robustness under Sub-Sampling for the SAT Competition 2018 (slides PDF)
12:30-14:00 Lunch
14:00-15:30 Invited talk
Joao Marques-Silva. SAT: Disruption, Demise and Resurgence (slides PDF)
15:30-16:00 Coffee break
16:00-17:30 Parallel and Hybrid Solving
Marc Hartung and Florian Schintke. Learned Clause Minimization in Parallel SAT Solvers (paper, slides PDF)
Johannes K. Fichte, Markus Hecher and Markus Zisser. gpusat2 – An Improved GPU Model Counter (paper, slides PDF)
Jo Devriendt, Jan Elffers, Ambros Gleixner and Jakob Nordström. Leveraging LP solving for PB solving (WIP, slides PDF)
17:30-18:00 Summary / discussion
18:00 Closing

Registration

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

Registration fee for the worshop is 40€ before June 30, 60€ on site.

Registration fee includes coffee breaks.

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.

Instead, 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 (updated)

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