Abstract:
An increasing number of results in graph theory, combinatorics and theoretical computer science is obtained with the help of computers, e.g. the proof of the Four Colours Theorem or the computation of certain Ramsey numbers. Binary decision diagrams, known as tools in hardware verification and computer-aided design, are used here for the solution of counting and other combinatorial problems. The basic results about the appropriate variants of binary decision diagrams are presented. In order to prove the usefulness of the approach the number of knight's tours on an 8x8 chessboard is computed for the first time as well as the number of cycle coverings. Moreover, bounds on the asymptotic number of knight's tours are discussed.