swe flag På svenska
bild
School of
Electrical Engineering
and Computer Science
KTH / EECS / TCS / Jakob Nordström / Video seminars

I have moved to the Department of Computer Science (DIKU) at the University of Copenhagen and also have a part-time affiliation with the Department of Computer Science at Lund University. For now, my webpages still reside at KTH, and are being updated here, but this should change during 2020.

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 low-key events, and are usually announced only locally. In case you want to receive the announcements, please just let us know by sending an e-mail message to jakob.nordstrom@cs.lth.se and we will do our best to keep you in the loop.

Video seminars autumn 2020

  • 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 NP-hard in general graphs and has applications in diverse areas like scheduling, radio frequency assignment, obnoxious facility location and map-coloring.

    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 Matrix-instances, which are the commonly used benchmark instances for this problem, were often very large (e.g., up to 577%).

    We present new mixed-integer 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 SAT-encodings, including a new and specialised encoding which exploits a certain staircase-structure occuring in the problem formulation. We present computational results for all the algorithms, including a comparison of the MIP and SAT-approaches. 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 NP-complete problem, state-of-the-art 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 conflict-driven 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 forward-checking 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 pseudo-Boolean approach to nonlinear verification
    (Vincent Liew, University of Washington)

    We discuss some new experimental results showing the promise of using pseudo-Boolean solvers, rather than SAT solvers, to verify bit-vector 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 bit-vector inequalities where the pseudo-Boolean approach significantly outperformed SAT solvers and even bit-vector solvers. Finally, we give some of our observations on the strengths and weaknesses of different methods of conflict analysis used by pseudo-Boolean solvers.

  • Friday May 8 at 13:15
    Pseudo-Boolean solvers for answer set programming
    (Bart Bogaerts, Vrije Universiteit Brussel)

    Answer set programming (ASP) is a well-established 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 pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane-based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean 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.

Published by: Jakob Nordström <jakobn~at-sign~kth~dot~se>
Updated 2020-07-15