Pragmatics of SAT

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

July 5, 2021, 3pm-8pm CEST (online event)

News: May 13, 2021 Date and time set The day and time of the workshop has been decided with the SAT conference and workshops chairs.
News: May 10, 2021 Deadlines shifted by one week The abstract and paper submission deadlines and the notification deadlines have been shifted by one week.
News: March 27, 2021 PoS will be also a virtual event After the success of the fully virtual 2020 edition (more than 70 participants), PoS will also be available online, even if the workshop can be organized physically in Barcelona.

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 2021 edition is thus the twelfth 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 on July 5, 3pm to 8pm CEST, during the SAT conference in Barcelona. It will be an online event, using zoom technology.

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

Technical Programme

2:55pm-3:00pm Introduction to PoS virtual event (rules for speaking, interacting with speaker, etc)
3:00pm-4:00pm Session 1: SAT and applications
3:00pm-3:15pm MatSat: a matrix-based differentiable SAT solver by Taisuke Sato and Ryosuke Kojima
3:15pm-3:30pm Towards CEGAR-based Parallel SAT Solving by Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura and Katsumi Inoue
3:30pm-3:45pm A Study of Divide and Distribute Fixed Weights and its Variants by Cayden Codel and Marijn Heule
3:45pm-4:00pm How to Approximate Leximax-optimal Solutions by Miguel Cabral, Mikoláš Janota and Vasco Manquinho
4:00pm-4:15pm Virtual break
4:15pm-5:15pm Session 2: Pseudo-Boolean solving and certification
4:15pm-4:30pm Certifying CNF Encodings of Pseudo-Boolean Constraints by Stephan Gocht, Ruben Martins and Jakob Nordstrom
4:30pm-4:45pm On Improving the Backjump Level in PB Solvers by Romain Wallon
4:45pm-5:00pm Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs by Stephan Gocht and Jakob Nordstrom
5:00pm-5:15pm Branching strategies for solving pseudo-Boolean optimization problems using Integer-programming solvers by Srinivas Tamvada and Elkafi Hassini
5:15pm-5:30pm Virtual break
5:30pm-6:30pm Invited Talk by Roberto Sebastiani
6:30pm-6:45pm Virtual break
6:45pm-7:45pm Session 3: Core SAT
6:45pm-7:00pm Bipartite Perfect Matching Benchmarks by Cayden Codel, Joseph Reeves, Marijn Heule and Randal Bryant
7:00pm-7:15pm The Impact of Bounded Variable Elimination on Pigeonhole Formulas by Joseph Reeves and Marijn Heule
7:15pm-7:30pm Mining Definitions in Kissat with Kittens by Mathias Fleury and Armin Biere
7:30pm-7:45pm An Experimental Study of Permanently Stored Learned Clauses by Sima Jamali and David Mitchell
7:45pm-8:00pm Session 4: open discussion
8:00pm Closing

Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results by Roberto Sebastiani

Roberto Sebastiani

Invited talk, July 5, 5:30pm-6:30pm CEST Quantum annealers (QAs) are specialized quantum computers that minimize objective functions over discrete variables by physically exploiting quantum effects. Current QA platforms allow for the optimization of quadratic objectives defined over binary variables (qubits), also known as Ising problems. In the last decade, QA systems as implemented by D-Wave have scaled with Moore-like growth. Current architectures provide >5000 sparsely-connected qubits, and continued exponential growth is anticipated, together with increased connectivity. We explore the feasibility of such architectures for solving SAT and MaxSAT problems as QA systems scale. We develop techniques for effectively encoding SAT –and, with some limitations, MaxSAT– into Ising problems compatible with sparse QA architectures. We provide the theoretical foundations for this mapping, and present encoding techniques that combine offline Satisfiability and Optimization Modulo Theories with on-the-fly placement and routing. Preliminary empirical tests on a current generation D-Wave system support the feasibility of the approach for certain SAT and MaxSAT problems.

This invited talk will be based on the material available in the following paper, plus a few more recent developments.

            Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti:
            Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results. Inf.
            Comput. 275: 104609 (2020)
            
Available online at https://doi.org/10.1016/j.ic.2020.104609. Preprint available at the presenter's publication web page.

Registration

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

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