Spotlight

June 19th, 2013

By:Uwe Waldmann

Automated Deduction

Human mathematicians prove a theorem by combining individual computation steps. This is a rather trivial task for a computer program once the necessary steps are known. For automatized processes, however, choosing which steps to execute is similar to looking for a needle in an infinitely large haystack. The research group "Automation of Logic" is one of the world leaders in developing efficient automated theorem provers.


Mission

While the acceleration of hardware has been a landmark of progress in computing technology in the past few decades, the computing enhancements that it provides is dwarfed by the increase in speed, performance, and robustness resulting from new algorithms.

As a point in case, the status of hardware and algorithms in 1970 allowed to compute an optimal tour of a traveling salesman (a classical optimization problem and accepted benchmark for computing power) through 120 cities. Increasing the number of cities from n to n+1 leads to a multiplicative increase of the number of possible tours by a factor of n. Thus, relying only on the increase of hardware speed, with today’s technology, and the algorithms of 1970 we could find optimal tours among only 135 cities. It is the progress in algorithms that, today, enables us to find optimal tours between many thousand of cities. Relying only on progress in hardware this performance would not be achievable in hundreds of years.

The Max-Planck Institute for Informatics is devoted to cutting-edge research in informatics with a focus on algorithms and their applications in a broad sense.

[ more... ]