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.
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.
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.
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
Original papers describing original work
on a topic of the workshop, including papers whose focus might be too narrow to be published in
a conference. Short original papers, approximately 6-8 pages in length, including system
descriptions of SAT and related solver technologies are also welcome.
Work-in-progress papers describing less
mature work on a topic of the workshop, to gather feedback from the community. It may include papers
submitted to conferences or journals, which should be clearly stated in the paper.
Presentation-only papers describing a work
on a topic of the workshop recently accepted or published to another conference or a journal, but that
the
community may have missed (including, e.g., domain-specific applications of declarative solvers
at the respective domain-specific conferences). Submissions to this category will be evaluated
only on their relevance to the workshop.
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 early editions, there will be no workshop proceedings.
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
Benchmarks
Slides
Software
Data
DATE'22 paper