July 5, 2021, 3pm-8pm CEST (online event)
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 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.
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.
Main areas of interest include, but are not restricted to:
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.
|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: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:30pm-6:30pm||Invited Talk by Roberto Sebastiani|
|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|
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.
Bio Roberto Sebastiani is Professor of Artificial Intelligence, Automated Reasoning and Formal Methods at Dipartimento di Ingegneria e Scienza dell'Informazione (DISI), Università di Trento, Italy. His main research topics are Automated Reasoning (in particular SAT, SMT and OMT), Formal Verification (in particular, model checking) and their applications. Roberto built his first SAT-based system in 1993, has built various automated reasoning tools for various logics and has been an active member of the creation of the SMT framework. In 2006, he organized with Byron Cook the Pragmatics of Decision Procedures in Automated Reasoning workhop at FLoC, which inspired PoS for the next FLoC in 2010.
Registration for the workshop is available on the main conference web site. Registration is free but mandatory.
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