Recently, Dr. Xiaoyu Song and a group of researchers including myself did some work to reduce Board Level Routing Problem (BLRP) to boolean satisfiability.
From this page, you can download a set of benchmarks generated for our paper, as well as the Windows executables of the benchmark generator and the BLRP to CNF convertor. The generator produces benchmarks in an easy-to-interpret BLRP problem format (see an example below). The convertor takes the problem specification in the BLRP format and outputs a set of clauses in the DIMACS CNF format, which can be used as an input to any of the available SAT solvers. For a summary of command-line options, run the above executables without arguments.
The BLRP is defined as follows: "Given P chips, each chip having K types of pins and M pins of each type, route N nets connecting chips in such a way that nets join pins of the same type".
An illustrative example of the BLRP is the following: "Given three chips,
with two pin types, and two pins of each type, route six nets, connecting
chips pair-wise, with two nets between each pair of chips." Two approaches
to solving this problem (one leading to an impasse; another to a valid
solution) are given in the picture below:
The BLRP problem description for this benchmark is as follows:
----- file "test.blrp" -------
# comment line
.p 3
.k 2
.m 2
.n 6
0 1
0 1
1 2
1 2
0 2
0 2
.e
------------------------------
Alan Mishchenko's Home Page