AIB 2009-09: Implementation of an Automated Proof for an Algorithm Solving the Maximum Independent Set Problem

[Carsten Fuhs]

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Implementation of an Automated Proof for an Algorithm Solving the
Maximum Independent Set Problem
Michael Nett
AIB 2009-09

Kneis, Langer, and Rossmanith proposed an algorithm that solves the
maximum independent set problem for graphs with $n$ vertices in
$O^*(1.2132^n)$. This bound is obtained by precisely analyzing
all cases that the algorithm may encounter during execution. Since
the number of cases exceeds several millions, a computer aided proof
is used to generate and evaluate all cases. In this paper, we present
a program that fulfills this task and give a detailed description of
the principles underlying our method. Moreover, we prove that the set
of generated cases includes all relevant cases.