Implementation of an Automated Proof for an Algorithm Solving the Maximum
Independent Set Problem

Michael Nett

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.