We propose a new approach to SAT solving which solves SAT problems in
vector spaces as cost minimization of a differentiable cost function
J^{sat}. In our approach, a solution, satisfying assignment, of a SAT
problem in n variables is represented by a binary vector u in {0,1} such
that J^{sat}(u) = 0. We search for such u in a vector space R^n by cost
minimization, i.e., starting from an initial u0, we minimize J^{sat} to
zero while iteratively updating u by Newton's method.
We implemented our approach as an incomplete matrix-based differentiable
SAT solver MatSat. Although existing mainstream SAT solvers decide each
bit of a solution assignment one by one, be they of conflict driven
clause learning (CDCL) type or of stochastic local search (SLS) type,
MatSat fundamentally differs from them in that it changes all variables
at once and continuously approaches a solution in a vector space. We
conducted experiments to measure the scalability of MatSat with a random
3-SAT problem. In these experiments, we showed that MatSat implemented
for GPU can solve the problem with n = 3x10^5 variables, demonstrating
the possibility of further acceleration of MatSat by hardware
acceleration. We also compared MatSat with nine state-of-the-art CDCL
and SLS SAT solvers in terms of execution time by conducting experiments
with several random and non-random data sets. In the case of easy random
SAT, the performance of MatSat comes between the SLS solvers and the
CDCL solvers but is ranked 1st on the difficult one. Similarly,
concerning non-random SAT, it shows poor performance for easy cases but
outperforms all nine solvers in the difficult case.
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: August 9, 2022
Added links to preprint or papers published at SAT'22.
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:
- techniques for debugging or certifying solvers
- visualisation of benchmarks structure
- monitoring solver behaviour
- evaluation of solvers
- efficient data structures
- domain specific encodings
- taking into account multi-core technology
- domain specific heuristics
- new application of constraint-based technologies
- new use cases of constraint-based technologies
- system/library description
- solver API
- constraint solving and machine learning
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 |
|
| 3:15pm-3:30pm |
SAT-based methods consist of two steps:
(i) encoding step that translates a given problem into a SAT instance, and
(ii) solving step that computes a solution using SAT solvers.
When speed-up SAT-based methods using parallelization,
the use of parallel SAT solvers is promising for improving the step (ii).
However, there are sometimes constraints that require a huge number of clauses to encode.
Such constraints slow down the step (ii) or abort the SAT-based method at the step (i).
In this case, we need a parallelization that takes care of both of the step (i) and (ii).
In this paper, we propose a parallel SAT solving based on
counterexample guided abstraction refinement (CEGAR).
CEGAR is a technique that solves a given problem by iteratively solving
abstracted problems that have fewer constraints.
The idea is the launch of multiple CEGAR processes and their cooperation by sharing
counterexamples.
Using Hamiltonian cycle problems as a case study,
we show a preliminary result that demonstrates the effectiveness of the proposed
parallelization.
|
| 3:30pm-3:45pm |
Divide and Distribute Fixed Weights (DDFW) is a stochastic local search Boolean
satisfiability (SAT) solver that has achieved a high level of performance on select problem
instances, including the Pythagorean triples instance for n = 7824. Yet despite its success,
DDFW has received little research interest, and its initial results are out of date with
respect to more modern SAT benchmarks. To address both those research needs, we examine DDFW
in depth and propose modifications to the algorithm based off of ideas from similar SAT
solvers such as ProbSAT and SAPS. We then take these modifications and test DDFW against a
set of modern hard benchmarks. We present two main findings. The first is a confirmation
that a greedy variable selection process in focused search is optimal for DDFW. The second
is that it is more effective for unsatisfied clauses to borrow clause weight from its entire
neighborhood rather than a singular clause in local minima, as it does in the original
algorithm. Using this new strategy, DDFW performs 50% than the original, and this strategy
indicates a promising new research direction to investigate for this class of SLS
algorithms.
|
| 3:45pm-4:00pm |
Many real-world problems can be modelled as Multi-Objective Combinatorial Optimisation
(MOCO) problems. In the multi-objective case, there is not a single optimum value but a set
of optima known as Pareto-optima. However, the number of Pareto-optima can be too large to
enumerate. Instead, one can compute a minimum Pareto-optimum according to an order. The
leximax order selects a Pareto-optimum such that the objective functions with the worst
values are penalised the least. Unlike other orders, such as the lexicographic order or the
weighted sum order, the leximax order does not favour any objective function at the expense
of others. Also, the leximax-optimum has a guaranteed small trade-off between the objective
functions.
In some real-world MOCO problems, the time to find a solution may be limited and computing a
leximax-optimal solution may take too long. In such problems, we search for solutions that
can be computed in the given admissible amount of time and that are as close to the
leximax-optimum as possible. In other words, we approximate the leximax-optimum.
In this paper, we present and evaluate SAT-based algorithms and heuristics for approximating
the leximax-optimum of Multi-Objective Boolean Satisfiability problems.
The evaluation is performed in the context of the package upgradeability problem,
on the set of benchmarks from the Mancoosi International
Solver Competition, with combinations of up to five different objective
functions.
|
| 4:00pm-4:15pm | Virtual break |
| 4:15pm-5:15pm | Session 2: Pseudo-Boolean solving and certification |
| 4:15pm-4:30pm |
The dramatic improvements in Boolean satisfiability (SAT) solving
since the turn of the millennium have made it possible to leverage
state-of-the-art conflict-driven clause learning (CDCL) solvers for
many combinatorial problems in academia and industry, and the use of
proof logging has played a crucial role in increasing the confidence
that the results these solvers produce are correct. However, the
conjunctive normal form (CNF) format used for SAT proof logging means
that it is hard to extend the method to other, stronger, solving
paradigms for combinatorial problems.
We show how to instead leverage the cutting planes proof system to
provide proof logging for pseudo-Boolean solvers that translate
pseudo-Boolean problems (a.k.a 0-1 integer linear programs) to CNF and
run CDCL. We are hopeful that this is just a first step towards
providing a unified proof logging approach that will also extend to
maximum satisfiability (MaxSAT) solving and pseudo-Boolean
optimization in general.
|
| 4:30pm-4:45pm |
Current PB solvers implement many techniques inspired by the CDCL
architecture of modern SAT solvers, so as to benefit from its practical
efficiency.
However, they also need to deal with the fact that many of the properties
leveraged by this architecture are no longer true when considering PB
constraints.
In this paper, we focus on one of these properties, namely the optimality
of the so-called first unique implication point (1-UIP).
While it is well known that learning the first assertive clause produced
during conflict analysis ensures to perform the highest possible backjump
in a SAT solver, we show that there is no such guarantee in the presence
of PB constraints.
We also introduce and evaluate different approaches designed to improve the
backjump level identified during conflict analysis by allowing to continue
the analysis after reaching the 1-UIP.
Our experiments show that sub-optimal backjumps are fairly common in PB
solvers, even though their impact on the solver is not clear.
|
| 4:45pm-5:00pm |
The dramatic improvements in Boolean satisfiability (SAT) solving
since the turn of the millennium have made it possible to leverage
state-of-the-art conflict-driven clause learning (CDCL) solvers for
many combinatorial problems in academia and industry, and the use of
proof logging has played a crucial role in increasing the confidence
that the results these solvers produce are correct. However, the
conjunctive normal form (CNF) format used for SAT proof logging means
that it is hard to extend the method to other, stronger, solving
paradigms for combinatorial problems.
We show how to instead leverage the cutting planes proof system to
provide proof logging for pseudo-Boolean solvers that translate
pseudo-Boolean problems (a.k.a 0-1 integer linear programs) to CNF and
run CDCL. We are hopeful that this is just a first step towards
providing a unified proof logging approach that will also extend to
maximum satisfiability (MaxSAT) solving and pseudo-Boolean
optimization in general.
|
| 5:00pm-5:15pm |
Pseudo-Boolean Optimization problems (PBOs) are an important class of Integer Lin-
ear Programming (ILP) problems that arise frequently in industrial applications. While
specialized solvers exist for PBOs, ILP solvers can be useful for solving hard PBOs to
within a certain integrality gap. This paper incorporates popular PBO branching heuristics
into a commercial ILP solver. A novel heuristic called Trigger Equivalence and Domination is
developed for speeding up look-ahead based branching. Experiments with hard-to-solve
instances indicate that the proposed heuristics are an attractive alternative to
conventional strong branching. Testing results from an industrial application are also
presented.
|
| 5:15pm-5:30pm | Virtual break |
| 5:30pm-6:30pm |
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.
|
| 6:30pm-6:45pm | Virtual break |
| 6:45pm-7:45pm | Session 3: Core SAT |
| 6:45pm-7:00pm |
The pigeonhole and mutilated chessboard problems are challenging benchmarks for most SAT
solvers. Although some solvers employ special techniques that efficiently solve the
canonical versions of these two problems, these techniques may fail with even slight problem
variations. To evaluate and improve the robustness of SAT solvers, we designed a benchmark
family of perfect matching problems on bipartite graphs that generalizes the pigeonhole and
mutilated chessboard problems. Our benchmark generator supports various encodings and
randomized constructions. Experimental results show that different variations degrade the
performance of solvers in unexpected ways. As such, the benchmark family, taken as a whole,
provides a good way to reveal the fragility of fine-tuned solving techniques. Tuning against
it will encourage more robust solver implementations. We also studied the effect that adding
symmetry-breaking clauses has on solver performance. We found that general solvers perform
better with additional symmetry-breaking clauses, while some solvers that rely on special
solving techniques perform worse.
|
| 7:00pm-7:15pm |
Variable elimination is arguably the most important pre- and in-processing technique in
state-of-the-art SAT solvers. There are hardly any problems for which variable elimination
by substitution, as presented by Eén and Biere in 2005, hurts performance. However, during
an experimental study, we observed that variable elimination resulted in substantial
slowdowns of the 2020 SAT Competition winner Kissat on pigeonhole formulas. In this paper we
evaluated the impact of different variable elimination orderings on solving pigeonhole
formulas using recent SAT competition winners. The results show that some solvers are more
stable than others, while the formulas obtained by some elimination orderings are
consistently more difficult to solve. Further, we implemented static variable decision
heuristics in the solver CaDiCaL that outperformed all other solvers.
|
| 7:15pm-7:30pm |
Bounded variable elimination is one of the most important preprocessing techniques in SAT
solving.
It benefits from discovering functional dependencies in the form of definitions encoded in
the CNF.
While the original approach relied on syntactic pattern matching our new approach uses cores
produced by an embedded SAT solver. In contrast to a similar semantic approach in Lingeling
based on
BDD algorithms, our new approach is able to generate DRAT proofs. We further discuss design
choices
for our embedded SAT solver Kitten. Experiments with Kissat show the effectiveness of this
approach.
|
| 7:30pm-7:45pm |
Modern CDCL SAT solvers learn clauses rapidly, and an important heuristic is the clause
deletion scheme. Most current solvers have two (or more) stores of clauses. One has
``valuable'' clauses which are never deleted. Most learned clauses are added
to the other, with an aggressive deletion strategy to restrict its size.
Recent solvers in the MapleSAT family, have comparatively complex deletion scheme, and
perform well. Many solvers store only binary clauses permanently, but MapleSAT family of
solvers store clauses with small LBD permanently. We report an experimental study of the
permanent clause store in MapleLCMDistChronoBT.
We observe that this store can get quite large, but several methods for limiting its size
reduced performance.
We also show that alternate size and LBD based criteria improve performance, while still
having large permanent stores.
In particular, saving clauses up to size 8, and adding small numbers of high-centrality
clauses, both improved performance, with the best improvement using both methods.
|
| 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
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 workshop at FLoC, which inspired PoS for the next FLoC in 2010.
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:
- 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.
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
- Abstract submission deadline: May 9 16, 2021 (soft, submit ASAP)
- Paper submission deadline: May 16 23, 2021
- Notification to authors: June 6 13, 2021
- Final version due: June 27, 2021
- Workshop: July 5, 2021
Programme Committee
- Jeremias Berg, University of Helsinki / HIIT
- Armin Biere, Johannes Kepler University Linz
- Marijn Heule, Carnegie Mellon University
- Hidetomo Nabeshima, University of Yamanashi
- Alexey Ignatiev, Monash University
- Matti Jarvisalo, University of Helsinki chair
- Daniel Le Berre, University of Artois - CNRS chair
- Kuldeep Meel, National University of Singapore
- Aina Niemetz, Stanford University
- Olivier Roussel, University of Artois - CNRS
- Romain Wallon, École Polytechnique
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