Video seminars
The video seminars are the more or less informal seminar series
of the Mathematical Insights into Algorithms for Optimization (MIAO)
research group started during the spring of 2020.
These are typically fairly lowkey events, and are usually announced
only locally. In case you want to receive the announcements, please
just let us know by sending an email message to
jakob.nordstrom@cs.lth.se and we will do our best to keep you in the
loop.
Video seminars autumn 2020

Friday Oct 9 at 13:15
Model counting with probabilistic component caching
(Shubham Sharma and Kuldeep S. Meel,
National University of Singapore)
Given a Boolean formula F, the problem of model counting, also
referred to as #SAT, seeks to compute the number of solutions of F.
Model counting is a fundamental problem with a wide variety of
applications ranging from planning, quantified information flow to
probabilistic reasoning and the like. The modern #SAT solvers tend to
be either based on static decomposition, dynamic decomposition, or a
hybrid of the two. Despite dynamic decomposition based #SAT solvers
sharing much of their architecture with SAT solvers, the core design
and heuristics of dynamic decompositionbased #SAT solvers has
remained constant for over a decade. In this paper, we revisit the
architecture of the stateoftheart dynamic decompositionbased #SAT
tool, sharpSAT, and demonstrate that by introducing a new notion of
probabilistic component caching and the usage of universal hashing
for exact model counting along with the development of several new
heuristics can lead to significant performance
improvement over stateoftheart modelcounters. In particular, we
develop GANAK, a new scalable probabilistic exact model counter that
outperforms stateoftheart exact and approximate model counters for
a wide variety of instances.

Friday Sep 25 at 13:15
Manthan: A datadriven approach for Boolean function synthesis
(Priyanka Golia and Kuldeep S. Meel,
National University of Singapore)
Boolean functional synthesis is a fundamental problem in computer
science with wideranging applications and has witnessed a surge of
interest resulting in progressively improved techniques over the past
decade. Despite intense algorithmic development, a large number of
problems remain beyond the reach of the current stateoftheart
techniques. Motivated by the progress in machine learning, we propose
Manthan, a novel datadriven approach to Boolean functional
synthesis. Manthan views functional synthesis as a classification
problem, relying on advances in constrained sampling for data
generation, and advances in automated reasoning for a novel
proofguided refinement and provable verification. On an extensive
and rigorous evaluation over 609 benchmarks, we demonstrate that
Manthan significantly improves upon the current state of the art,
solving 356 benchmarks in comparison to 280, which is the most solved
by a stateoftheart technique; thereby, we demonstrate an increase
of 76 benchmarks over the current state of the art. The significant
performance improvements, along with our detailed analysis, highlights
several interesting avenues of future work at the intersection of
machine learning, constrained sampling, and automated reasoning.

Friday Aug 28 at 13:15
Tuning Sat4j PB solvers for decision problems
(Romain Wallon,
Université d'Artois)
During the last decades, many improvements in CDCL SAT solvers have made possible to solve efficiently large problems containing millions of variables and clauses.
Despite this practical efficiency, some instances remain out of reach for such solvers.
This is particularly true when the input formula requires an exponential size refutation proof in the resolution proof system (as for pigeonhole formulae).
This observation motivated the development of another kind of solvers, known as pseudoBoolean (PB) solvers.
These solvers take as inputs a conjunction of PB constraints (integral linear inequations over Boolean variables) and benefit from the cutting planes proof system, which is (in theory) stronger than the resolution proof system.
To implement this proof system, current PB solvers follow the direction of modern SAT solvers, by implementing a conflict analysis procedure relying on the application of cutting planes rules.
However, adapting the CDCL architecture to take into account PB constraints is not as straightforward as it may look.
In particular, many CDCL invariants and properties do not hold anymore as long as PB constraints are considered.
While some of them may be safely ignored (e.g., when they affect the decision heuristic, the deletion strategy or the restart policy), some others must be fixed to ensure the soundness of the solver (e.g., by ensuring to preserve the conflict during its analysis).
In this talk, we will give an overview of the main differences between PB solving and classical SAT solving, and present different approaches that have been designed to take these differences into account to extend the CDCL architecture to PB problems.
We will in particular discuss the pros and cons of these approaches, and we will explain how they can be enhanced to improve the practical performance of PB solvers.

Friday Aug 21 at 10:15
Using proofs to analyze SAT solvers
(Janne Kokkala,
Lund University and University of Copenhagen)
The main idea of this seminar is to give an overview of what
one can ask and what one can learn about SAT solvers when
analyzing the proof to estimate what part of the work was
useful. I will start by giving a 17ish minute alpha test run
for my presentation for our CP paper [1]. After that, I will
discuss earlier works that use the same or a similar idea for
general insights [2], analyzing VSIDS usefulness [3], and
clause exchange for parallel solvers [4,5]. To conclude, we
can discuss how this approach could be used for pseudoBoolean
solvers.
[1] J. I. Kokkala, J. Nordström.
Using Resolution Proofs to
Analyse CDCL SAT solvers.
[2] L. Simon.
Post Mortem Analysis of SAT Solver Proofs.
[3] S. Malik, V. Ying.
On the efficiency of the VSIDS decision heuristic.
(Workshop presentation.)
[4] G. Audemard, L. Simon.
Lazy
clause exchange policy for parallel SAT solvers.
[5] G. Katsirelos, A. Sabharwal, H. Samulowitz, L. Simon.
Resolution and parallelizability: Barriers to the efficient
parallelization of SAT solvers.

Wednesday Aug 19 at 13:15
On computational aspects of the antibandwidth problem
(Markus Sinnl,
Johannes Kepler University Linz)
In this talk, we consider the antibandwidth problem, also
known as dual bandwidth problem, separation problem and
maximum differential coloring problem. Given a labeled graph
(i.e., a numbering of the vertices of a graph), the
antibandwidth of a node is defined as the minimum absolute
difference of its labeling to the labeling of all its adjacent
vertices. The goal in the antibandwidth problem is to find a
labeling maximizing the antibandwidth. The problem is NPhard
in general graphs and has applications in diverse areas like
scheduling, radio frequency assignment, obnoxious facility
location and mapcoloring.
There has been much work on deriving theoretical bounds for
the problem and also in the design of metaheuristics in recent
years. However, the optimality gaps between the best known
solution values and reported upper bounds for the
HarwellBoeing Matrixinstances, which are the commonly used
benchmark instances for this problem, were often very large
(e.g., up to 577%).
We present new mixedinteger programming approaches for the
problem, including one approach, which does not directly
formulate the problem as optimization problem, but as a series
of feasibility problems. We also discuss how these feasibility
problems can be encoded with various SATencodings, including
a new and specialised encoding which exploits a certain
staircasestructure occuring in the problem formulation. We
present computational results for all the algorithms,
including a comparison of the MIP and SATapproaches. Our
developed approaches allow to find the proven optimal solution
for eight instances from literature, where the optimal
solution was unknown and also provide reduced gaps for eleven
additional instances, including improved solution values for
seven instances, the largest optimality gap is now
46%. Instances based on the problem were submitted to the SAT
Competition 2020.
Video seminars spring 2020

Wednesday Jul 15 at 15:00
Naïve algorithm selection for SAT solving
(Stephan Gocht,
Lund University and University of Copenhagen)
Although solving propositional formulas is an NPcomplete
problem, stateoftheart SAT solvers are able to solve formulas
with millions of variables. To obtain good performance it is
necessary to configure parameters for heuristic
decisions. However, there is no single parameter configuration
that is perfect for all formulas, and choosing the parameters is
a difficult task. The standard approach is to evaluate different
configurations on some formulas and to choose the single
configuration, that performs best overall. This configuration,
which is called single best solver, is then used to solve new
unseen formulas. In this paper we demonstrate how random forests
can be used to choose a configuration dynamically based on
simple features of the formula. The evaluation shows that our
approach is able to outperform the single best solver on
formulas that are similar to the training set, but not on
formulas from completely new domains.

Friday Jun 26 at 10:00
Behind the scenes of chronological CDCL
(Sibylle Möhle and Armin Biere,
Johannes Kepler University Linz)
Combining conflictdriven clause learning (CDCL) with
chronological backtracking is challenging: Multiple invariants
considered crucial in modern SAT solvers are violated, if
after conflict analysis the solver does not jump to the
assertion level but to a higher decision level instead. In
their SAT'18 paper "Chronological Backtracking", Alexander
Nadel and Vadim Ryvchim provide a fix to this issue. Moreover,
their SAT solver implementing chronological backtracking won
the main track of the SAT Competition 2018. In our SAT'19
paper, "Backing Backtracking", we present a formalization and
generalization of this method. We prove its correctness and
provide an independent implementation.
In this seminar, we demonstrate the working of chronological
CDCL by means of an example. In this example, after a conflict
the conflicting clause contains only one literal at conflict
level. It is therefore used as a reason for backtracking, thus
saving the effort of conflict analysis. We further show which
invariants are violated and present new ones followed by a
discussion of the rules of our formal framework. We also shed
light onto implementation details, including those which are
not mentioned in our SAT'19 paper.

Monday Jun 22 at 13:30
McSplit: A partitioning algorithm for maximum common subgraph
problems
(Ciaran McCreesh and James Trimble,
University of Glasgow)
We will give a short introduction to McSplit, an algorithm for
the maximum common (connected) subgraph problem coauthored
with Patrick Prosser and presented at IJCAI 2017. McSplit
resembles a forwardchecking constraint programming algorithm,
but uses a partitioning data structure to store domains which
greatly reduces memory use and time per search node. We will
also present our recent work with Stephan Gocht and Jakob
Nordström on adding proof logging to the algorithm, turning
McSplit into a certifying algorithm whose outputs can be
independently verified.

Thursday Jun 18 at 20:30
A pseudoBoolean approach to nonlinear verification
(Vincent Liew,
University of Washington)
We discuss some new experimental results showing the promise
of using pseudoBoolean solvers, rather than SAT solvers, to
verify bitvector problems containing multiplication. We use
this approach to efficiently verify the commutativity of a
multiplier output bit by output bit. We also give some examples
of simple bitvector inequalities where the pseudoBoolean
approach significantly outperformed SAT solvers and even
bitvector solvers. Finally, we give some of our observations on
the strengths and weaknesses of different methods of conflict
analysis used by pseudoBoolean solvers.

Friday May 8 at 13:15
PseudoBoolean solvers for answer set programming
(Bart Bogaerts, Vrije Universiteit Brussel)
Answer set programming (ASP) is a wellestablished knowledge
representation formalism. Most ASP solvers are based on
(extensions of) technology from Boolean satisfiability
solving. While these solvers have shown to be very successful in
many practical applications, their strength is limited by their
underlying proof system, resolution. In this research, we
present a new tool LP2PB that translates ASP programs into
pseudoBoolean theories, for which solvers based on the
(stronger) cutting plane proof system exist. We evaluate our
tool, and the potential of cuttingplanebased solving for ASP
on traditional ASP benchmarks as well as benchmarks from
pseudoBoolean solving. Our results are mixed: overall,
traditional ASP solvers still outperform our translational
approach, but several benchmark families are identified where
the balance shifts the other way, thereby suggesting that
further investigation into a stronger proof system for ASP is
valuable.
