Networking week: Proof logging and certifying algorithms

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