13th Pragmatics of SAT international workshop

a workshop of the 25th International Conference on Theory and Applications of Satisfiability Testing

part of the Federated Logic Conference (FLoC) 2022

August 1, 2022, Haifa, Israel

August 8, 2022: Added links to software, data, slides and preprint when applicable.
July 18, 2022: Programme unveiled.
May 16, 2022: Due to the collision with extended SAT competition deadlines, the abstract and paper submission deadlines and authors notification date have been extended.
February 14, 2022: Programme Committee unveiled.
December 22, 2021: Web site is up.

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 twelfth edition was mostly virtual for the same reason.

The 2022 edition is thus the thirteenth edition of the workshop dedicated to the practical aspects of SAT research, the fourth edition running during FLoC.

Topics

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

Programme/Venue

The workshop will take place on August 1, 2022.

The detailed programme is also available using easy chair smart program.

8:50am-9:00am Opening
9:00am-10:30am Applications
9:00am-9:30am
Towards an Efficient CNF Encoding of Block Ciphers by Daniel Waszkiewicz and Konstanty Junosza-Szaniawski work in progress

SAT-solvers are one of the primary tools to assess the security of block ciphers automatically. Common CNF encodings of s-boxes are based on algebraic representations (finding low-degree polynomials) or symbolic execution of considered function implementation. However, those methods are not strictly connected with algorithms used in efficient SAT-solvers. Therefore, we propose an application of minimal propagate complete encodings, which in their definition are tuned for modern satisfiability checking algorithms.

During the construction of the Boolean formula, there is often the problem of encoding linear XOR equations. The standard procedure includes a greedy shortening algorithm to decrease the size of the resulting encoding. Recently, the problem of a straight-line program has been successfully applied in obtaining efficient implementations of MDS matrices. In this paper, we propose to use the algorithm for finding a short straight-line program as a shortening procedure for a system of linear XOR equations.

As a result, we achieved a 20x speed-up of algebraic cryptanalysis of Small Scale AES block cipher to widely used algebraic representations by combining two approaches.

Benchmarks Slides
9:30am-10:00am
Calculating Sufficient Reasons for Random Forest Classifiers by Markus Iser work in progress
In this paper, we formalize the implementations of decision tree and random forest classifiers of the Python Scikit-learn package, and we present a CNF encoding which can be used to calculate sufficient reasons a.k.a. prime implicants for them. Our decision tree encoding resembles a monotonic combinational circuit with pure input variables, of which we take advantage in our method for incremental enumeration of its prime implicants. Encoding the combination of several decision trees in a random forest would add a non-monotonic evaluation function to the root of the encoded circuit. In our approach, we solve an auxiliary SAT problem for enumerating valid leaf-node combinations of the random forest. Each valid leaf-node combination is used to incrementally update the original monotonic circuit encoding by extending the DNF at its root with a new term. Preliminary results show that enumeration of prime implicants by incrementally updating the encoding is by order of magnitudes faster than one-shot solving of the monolithic formula. We present preliminary runtime data, and some initial data about the size and number of samples found when translating the prime implicants back into database queries.
Slides
10:00am-10:30am
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification by Daniela Kaufmann, Paul Beame, Armin Biere and Jakob Nordstrom DATE'22 paper presentation
Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this work that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.
Software Data DATE'22 paper Slides
10:30am-11:00am Coffee Break
11:00am-12:30am SAT and Parallel Solving
11:00am-11:30am
Dinosat: A SAT Solver with Native DNF Support by Thomas Bartel, Tomas Balyo and Markus Iser work in progress
In this paper we report our preliminary results with a new kind of SAT solver called Dinosat. Dinosat's input is a conjunction of clauses, at-most-one constraints and disjunctive normal form (DNF) formulas. The native support for DNF formulas is motivated by the application domain of SAT based product configuration. A DNF formula can also be viewed as a generalization of a clause, i.e., a clause (disjunction of literals) is special case of a DNF formula, where each term (conjunction of literals) has exactly one literal. Similarly, we can generalize the classical resolution rule and use it to resolve two DNF formulas. Based on that, the CDCL algorithm can be modified to work with DNF formulas instead of just clauses. Using randomly generated formulas (with DNFs) we experimentally show, that in certain relevant scenarios, it is more efficient to solve these formulas with Dinosat than translate them to CNF and use a state-of-the-art SAT solver. Another contribution of this paper is identifying the phase transition points for such formulas.
Slides
11:30am-12:00am
DPS: A Framework for Deterministic Parallel SAT Solvers by Hidetomo Nabeshima, Tsubasa Fukiage, Yuto Obitsu, Xiao-Nan Lu and Katsumi Inoue original work
In this study, we propose a new framework for easily constructing efficient deterministic parallel SAT solvers, providing the delayed clause exchange technique introduced in ManyGlucose. This framework allows existing sequential SAT solvers to be parallelized with just as little effort as in the non-deterministic parallel solver framework such as PaInleSS. We show experimentally that parallel solvers built using this framework have performance comparable to state-of-the-art non-deterministic parallel SAT solvers while ensuring reproducible behavior.
Software Data Paper (preprint) Slides
12:00am-12:30am
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses by Mathias Fleury and Armin Biereoriginal work
We give a first account of our new parallel SAT solver Gimsatul. Its key feature is to share clauses physically in memory instead of copying them, which is the method of other state-of-the-art multi-threaded SAT solvers to share clauses logically. Our approach keeps information about which literals are watched in a clause local to a solving thread but shares the actual immutable literals of a clause globally among all solving threads. This design gives quiet remarkable parallel scalability, allows aggressive clause sharing while keeping memory usage low and produces more compact proofs.
Software Paper (preprint) Slides
12:30am-2:00pm Lunch break
2:00pm-3:30pm Proofs I
2:00pm-2:30pm
TBUDDY: A Proof-Generating BDD Package by Randal Bryant work in progress
The TBUDDY library enables the construction and manipulation of reduced, ordered binary decision diagrams (BDDs). It extends the capabilities of the BUDDY BDD package to support trusted BDDs, where the generated BDDs are accompanied by proofs of their logical properties. These proofs are expressed in a standard clausal framework, for which a variety of proof checkers are available. Building on TBUDDY via its application-program interface (API) enables developers to implement automated reasoning tools that generate correctness proofs for their outcomes. In some cases, BDDs serve as the core reasoning mechanism for the tool, while in other cases they provide a bridge from the core reasoner to proof generation. A Boolean satisfiability (SAT) solver based on TBUDDY can achieve polynomial scaling when generating unsatisfiability proofs for a number of problems that yield exponentially-sized proofs with standard solvers. It performs particularly well for formulas containing parity constraints, where it can employ Gaussian elimination to systematically simplify the constraints.
Software, Benchmarks, Tools Paper (preprint) FMCAD'22 paper Slides
2:30pm-3:00pm
Combining CDCL, Gauss-Jordan Elimination, and Proof Generation by Randal Bryant and Mate Soos original work
Traditional Boolean satisfiability (SAT) solvers based on the conflict-driven clause-learning (CDCL) framework fare poorly on formulas involving large numbers of parity constraints. The CryptoMiniSat solver augments CDCL with Gauss-Jordan elimination to greatly improve performance on these formulas. Integrating the TBUDDY proof-generating BDD library into CryptoMiniSat enables it to generate unsatisfiability proofs when using Gauss-Jordan elimination. These proofs are compatible with standard, clausal proof frameworks.
Benchmarks Paper (preprint)
3:00pm-3:30pm
Towards the shortest DRAT proof of the Pigeonhole Principle by Isaac Grosof, Naifeng Zhang and Marijn Heule original work
The Pigeonhole Principle (PHP) has been heavily studied in automated reasoning, both theoretically and in practice. Most solvers have exponential runtime and proof length, while some specialized techniques achieve polynomial runtime and proof length. Several decades ago, Cook manually constructed O(n^4) extended resolution proofs, where n denotes the number of pigeons. Existing automated techniques only surpass Cook's proofs in similar proof systems for large n. We construct the shortest known proofs of PHP in the standard proof format of modern SAT solving, DRAT. Using auxiliary variables and by recursively decomposing the original program into smaller sizes, we manually obtain proofs having length O(n^3) and leading coefficient 5/2.
3:30pm-4:00pm Coffee break
4:00pm-5:00pm Proof II
4:00pm-4:30pm
SATViz: Real-Time Visualization of Clausal Proofs by Tim Holzenkamp, Kevin Kuryshev, Thomas Oltmann, Lucas Wäldele, Johann Zuber, Tobias Heuer and Markus Iser original work
Visual layouts of graphs representing SAT instances can highlight the community structure of SAT instances. The community structure of SAT instances has been associated with both instance hardness and known clause quality heuristics. Our tool SATViz visualizes CNF formulas using the variable interaction graph and a force-directed layout algorithm. With SATViz, clause proofs can be animated to continuously highlight variables that occur in a moving window of recently learned clauses. If needed, SATViz can also create new layouts of the variable interaction graph with the adjusted edge weights. In this paper, we describe the structure and feature set of SATViz. We also present some interesting visualizations created with SATViz.
Software Slides
4:30pm-5:00pm
Certified Symmetry and Dominance Breaking for Combinatorial Optimisation by Bart Bogaerts, Stephan Gocht, Ciaran McCreesh and Jakob Nordstrom AAAI'22 distinguished paper award presentation
Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes XOR and cardinality reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.
Software (BreakID) Software (VeriPB) AAAI'22 paper Slides
5:00pm-5:30pm Discussion on topical aspects
5:30pm Closing

Registration

Registration to the workshop will be available from FLoC web site.

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 early 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