Networking week: Proof logging and certifying algorithms

MIAO Graphic

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