Networking week: Proof logging and certifying algorithms
From May 20-24 MIAO Research Group will host a networking week dedicated to proof logging and certifying algorithms for combinatorial solving and optimization. This is a rapidly developing area where applied research on algorithms for real-world problems comes together with in-depth theoretical study in computational complexity theory in quite intriguing ways.
There will be a couple of longer seminars on combinatorial solving on Tuesday and Wednesday, and on Thursday and Friday MIAO Reserach Group will run the 1st International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (yielding the acronym WHOOPS, reflecting the fairly spontaneous nature of the event). The WHOOPS webpage contains more information about all of this including a schedule for the workshop.
All talks will be streamed on Zoom (contact the organizers to get the link). Feel free to check out earlier works on the MIAO Research YouTube channel.
For more information please view the program below or visit the event page.
Title
Efficient algorithms for symmetry detection
Speaker
Markus Anders, Technische Universität Darmstadt
Date and place
Tuesday May 21 at 10:00 (note the time!) in seminar room N116B, Universitetsparken 1, University of Copenhagen, and on Zoom
Abstract
Exploitation of symmetry has a dramatic impact on the efficiency of algorithms in various fields. Before symmetries of a structure can be exploited, one first has to have algorithmic means to find the symmetries efficiently. Typically, this is achieved through modeling said structure as a graph, followed by an application of a practical graph isomorphism solver such as nauty, saucy, bliss, Traces, or dejavu.
In this talk, I will give an overview of recent progress on practical graph isomorphism solvers. I present a theoretical model which captures the backtracking behavior of all state-of-the-art solvers, within which we prove probabilistic strategies to be optimal up to logarithmic factors. Then, I briefly discuss the design of the practical solver dejavu, which is based on a near-optimal probabilistic backtracking strategy.
The material presented is based on joint work with Pascal Schweitzer.
Title
Solving optimization problems by a sequence of decisions
Speaker
Jeremias Berg, University of Helsinki
Date and place
Wednesday May 22 at 14:00 in seminar room N116A&B, Universitetsparken 1, University of Copenhagen, and on Zoom
Abstract
Computationally challenging optimization problems are common in artificial intelligence and other real-world settings. Among the several approaches to optimization problems that have been developed, the declarative approach is arguably one of the most promising ones in terms of allowing reasonable effectiveness and strong guarantees of the trustworthiness of the solutions obtained, e.g., via proof-logging. In the declarative approach, an instance of the optimization problem of interest is first represented as a set of mathematical constraints and an objective function. Afterward, an automated reasoning procedure (a solver) is invoked in order to compute an optimal solution to the constraints. Finally, a solution to the original problems is obtained from the solution to the constraint instance.
Most state-of-the-art approaches to computing optimal solutions of constraint instances reduce the optimization problem into a sequence of decision problems, which are in turn tackled with decision procedures for the constraint language being employed. A natural example is the so-called solution-improving approach, which iteratively queries a decision procedure for solutions of increasing quality until no such solutions can be found. Other central examples are the core-guided and implicit-hitting-set-based approaches that refine the optimization instance based on small sources of inconsistency (known as unsatisfiable cores) until a solution that relaxes all inconsistencies in a cost-optimal way is found. The solution-improving search, core-guided, and implicit hitting-set-based, algorithms currently represent the state-of-the-art in Maximum Satisfiability and pseudo-boolean Optimization. The algorithms have also been successfully applied in Constraint Programming and SMT.
In this seminar, I will present our recent work on a framework that allows us to view solution-improving, core-guided, and implicit-hitting-set-based search in a unified way. The framework provides new insight into the relationship between the three types of algorithms and also allows for a unified way of proving the correctness of virtually all instantiations of them that we are aware of. The constraint-agnostic framework can be used to analyze MaxSAT, PBO, and (some of the) CP algorithms that exist today. I will also highlight some interesting work, such as the potential of using the framework as the basis of a unified way of proof-logging optimization algorithms in various paradigms.
Program
Time | Activity |
09:45-10:00 | Welcome and presentation of participants |
10:00-11:00 | A one-size-fits-all proof logging system? Jakob Nordström |
11:00-12:00 | Certified symmetry breaking with VeriPB Bart Bogaerts |
12:00-13:30 | Lunch |
13:30-14:30 | Pseudo-Boolean proof logging for things that don't look pseudo-Boolean Ciaran McCreesh |
14:30-15:30 | Proof logging for some interesting constraint propagation algorithms Matthew McIlree |
15:30-16:00 | Break |
16:00-17:00 | Proof logging for MaxCDCL and BDDs Dieter Vandersande |
17:00-18:00 | Pitches and discussions about future directions and feature requests |
18:15 | Leave for workshop dinner at Madklubben Østerbro at Østerbrogade 79 |
Time | Activity |
10:00-11:00 | Proof logging for MaxSAT preprocessing with Hannes Ihalainen |
11:00-11:30 | Break |
11:30-12:00 | Certifying MIP-based presolve reductions for 0–1 integer linear programs with Andy Oertel |
12:00-12:30 | Symmetry breaking in the subgraph isomorphism problem with Joe Loughney |
12:30-13:00 | Pseudo-Boolean proof trimming with Arthur Gontier |
13:00 | Lunch and end of formal workshop |