Tuesday, August 28 |
07:30 - 09:00 |
Breakfast (Restaurant at your assigned hotel) |
09:00 - 10:00 |
Jakob Nordstrom: Towards Faster Conflict-Driven Pseudo-Boolean Solving ↓ The last 20 years have seen dramatic improvements in the performance
of algorithms for Boolean satisfiability---so-called SAT solvers---and
today conflict-driven clause learning (CDCL) solvers are routinely
used in a wide range of application areas. One serious short-coming
of CDCL, however, is that the underlying method of reasoning is quite
weak. A tantalizing solution is to instead use stronger
pseudo-Boolean (PB) reasoning (a.k.a. 0-1 integer linear programming),
but so far the promise of exponential gains in performance has mostly
failed to materialize---the increased theoretical strength seems hard
to harness algorithmically, and in many applications CDCL-based
methods are still superior.
In this talk, we will discuss conflict-driven search and how to lift
it from clauses to pseudo-Boolean linear constraints. We will survey
the "classic" method in [Chai and Kuehlmann '05] based on saturation,
and then describe a relatively new approach from [Elffers and
Nordström '18] instead using division. We will also try to highlight
some of the obstacles that remain along the path to truly efficient
pseudo-Boolean solvers. (Conference Room San Felipe) |
10:00 - 11:00 |
Fahiem Bacchus: MaxSat, successful solution techniques and some questions they raise. ↓ MaxSat is an optimization version of SAT. In particular, the clauses of a CNF are divided into hard and soft clauses where each soft clause has a finite and positive weight. MaxSat is the problem of finding a truth assignment that satisfies a maximum weight of soft clauses while also satisfying all of the hard clauses.
In this talk I will discuss the two most successful approaches to solving MaxSat: using SAT to solve a sequence of SAT formulas derived from the original MaxSat formula and the implicit hitting set approach which uses both SAT and Integer Programming solvers in a hybrid approach. Both approaches utilize the notion of cores which are subsets of soft clauses that are unsat when conjoined with the hard clauses. In the sequence of SAT approaches, discovered cores are used to reformulate the SAT formula that admits models falsifying more soft clauses of the original MaxSat formula. In the most successful of such methods extra variables are introduced into the formula and these play an essential role in the efficiency of the method. In the implicit hitting set approach, in contrast, the original MaxSat formula is unchanged. Instead cores are extracted from it, and hitting sets of the set of extracted cores are computed using integer programming solving. We will contrast the relative strengths of these two approaches, and try to draw some insights into what their relative successes say about the underlying problem. We will also attempt to highlight some further theoretical questions arising from these approaches. (Conference Room San Felipe) |
11:00 - 11:30 |
Coffee Break (Conference Room San Felipe) |
11:30 - 12:30 |
Nikolaj Bjorner: SMT solving - foundations and directions ↓This talk provides a survey of SMT solving with an emphasis on recent developments and directions.
- Integrating Theory Solvers.
Fundamental to SMT is a method for integrating
theory reasoners. The basic approach, based on
the Nelson-Oppen combination, has been the backbone
of mainstream SMT solvers. It works for signature
disjoint theories and an important research direction
has been how to tune it, notably for non-convex theories.
Integrating theories with shared signatues (such as the
theory of lists with a length function) has also received
attention, but is not integral to mainstream SMT solvers,
yet. The talk will revisit a few of these methods.
- Linear arithmetic and beyond.
A significant set of SMT use cases require some
reasoning about arithmetic. We summarize some highlights
in their approaches to solving classes of arithmetical
formulas, including linear real, integer, linear real with ReLu,
polynomial real, and with recent advances in handling non-linear
integer, polynomial GF, and transcendental functions.
- Strings and sequences.
An active area in the SMT community is in formulating formats
for string constraint solving. Several solvers have emerged in
the past few years. We touch on the basics of sequence solving
from the vantage point of the SMT and logic communities.
- Constrained Horn Clauses (CHC)
We illustrate how symbolic model checking over push-down systems
can be directly reduced to checking satisfiability of constrained
Horn clauses, that can be expressed as SMT formulas. Several
new approaches for solving CHCs are currently being developed by
different groups.
(Conference Room San Felipe) |
12:30 - 13:30 |
Ambros Gleixner: Computational Mixed-Integer Programming ↓ We will give a general introduction into the algorithms and
techniques implemented and successfully used in mixed-integer
programming solvers and try to point out connections to satisfiability
solving. One prime example are interactions between classical diving
heuristics and conflict analysis. Diving heuristics exhibit the
property that they either succeed in producing a feasible primal
solution or return a dual certificate of infeasibility subject to the
variable fixings. Although aimed at success, the failure certificates
can be analyzed to extract globally valid inequalities that help to
reduce the size of the remaining search tree in a very similar fashion
as in (UN)SAT solvers. (Conference Room San Felipe) |
13:30 - 14:30 |
Lunch (Restaurant Hotel Hacienda Los Laureles) |
14:30 - 16:00 |
Siesta (Conference Room San Felipe) |
16:00 - 16:30 |
Coffee Break (Conference Room San Felipe) |
16:30 - 17:00 |
Joao Marques-Silva: Towards MaxSAT-Based Proof Systems ↓ Inspired by the success of CDCL SAT solvers, recent years have witnessed
remarkable progress in Maximum Satisfiability (MaxSAT) solving. Modern
MaxSAT engines implement different approaches for exploiting SAT solvers as
oracles for NP. Concrete examples include core-guided MaxSAT, but also
MaxSAT using Minimum Hitting Sets (MHSes). Recent work has shown that, with
a so-called dual rail problem transformation, encodings of the PHP principle
can be solved in polynomial time with different MaxSAT solvers. Based on
this dual rail encoding and MaxSAT solving, more recent work devised proof
systems that were shown to p-simulate Resolution. This talk provides an
overview of some of the above results, but also surveys the original
practical motivation for developing proof systems exploiting the dual rail
encoding and MaxSAT. Finally, the talk summarizes ongoing research
directions. (Conference Room San Felipe) |
17:00 - 17:30 |
Nina Narodytska: Formal Analysis of Deep Binarized Neural Networks ↓ Understanding properties of deep neural networks is an important
challenge in deep learning. Deep learning networks are among the most
successful artificial intelligence technologies that is making impact
in a variety of practical applications. However, many concerns were
raised about `magical' power of these networks. It is disturbing that
we are really lacking of understanding of the decision making process
behind this technology. Therefore, a natural question is whether we
can trust decisions that neural networks make. One way to address this
issue is to define properties that we want a neural network to
satisfy. Verifying whether a neural network fulfills these properties
sheds light on the properties of the function that it represents. In
this work, we take the verification approach. Our goal is to design a
framework for analysis of properties of neural networks. We start by
defining a set of interesting properties to analyze. Then we focus on
Binarized Neural Networks that can be represented and analyzed using
well-developed means of Boolean Satisfiability and Integer Linear
Programming. One of our main results is an exact representation of a
binarized neural network as a Boolean formula. We also discuss how we
can take advantage of the structure of neural networks in the search
procedure. (Conference Room San Felipe) |
17:30 - 18:00 |
Daniel Le Berre: Pseudo-Boolean Optimization ↓ Very often, problems modeled using pseudo-Boolean constraints are optimization problems, not satisfaction problems.
Because of the very efficient SAT solvers available, many of those optimization problems can be solved by reusing those solvers as black boxes. In this talk, we will provide some insights about the reason of the success of the black box approaches, some of their limitations, and raise open problems to design more efficient Boolean optimizers. (Conference Room San Felipe) |
18:00 - 18:30 |
Marc Vinyals: Proof Systems for Pseudo-Boolean Solving ↓ Pseudo-Boolean solvers that generalize the CDCL algorithm and reason
within the cutting planes proof system can have a theoretical
advantage with respect to solvers that just translate the problem and
apply the standard CDCL algorithm, which is limited to resolution. In
practice, however, results are mixed. Do we need a better theory,
better solvers, or both?
One key observation is that implementation constraints limit solvers
to a subset of inference rules. In this talk we identify subsystems of
cutting planes that arise from these limited rules and we classify
them, showing in particular that pseudo-Boolean solvers are limited to
resolution if their input is encoded adversarially.
Guided by these theoretical insights we craft formulas that lie within
the limits of pseudo-Boolean solvers and test them in practice. Alas,
current solvers perform terribly on these benchmarks, but we can at
least extract concrete obstacles for upcoming solvers to overcome.
Joint work with Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and
Jakob Nordström. (Conference Room San Felipe) |
18:30 - 19:00 |
Sam Buss: The (un)reasonable (in)effectiveness of theory for Sat solvers ↓ There is an increasing interplay between practical implementations of Sat Solvers and theoretical results about proof complexity. In some cases, theory can be useful for understanding or designing Sat solvers, but the connections are not as strong as might be wished for. This talk will discuss these issues, and make some suggestions for further research directions both for theoreticians and for practitioners. (Conference Room San Felipe) |
19:00 - 20:30 |
Dinner (Restaurant Hotel Hacienda Los Laureles) |
20:30 - 22:00 |
Demo session, discussion on empirical evaluation ↓ Practical research on Satisfiability Solving requires tools. This session is dedicated to present the tools used by the participants (solvers, benchmarks generators, frameworks, visualization of experimental results, etc) and discuss the good practices of empirical evaluation in Satisfiability Solving.
Programme
- PySAT: Joao Marques Silva
- Testing and debugging solvers: Mathias Preiner
- CDCL insights from theory benchmarks website: Stephan Gocht
- Presentation of MIPLIB: Ambros Gleixner (Conference Room San Felipe) |