These are the first five BIBD generation problems listed in Colbourn et al., encoded as described in Prestwich using the standard DIMACS format (readable by most current SAT solvers). The files are:
| File name | $v$ | $b$ | $r$ | $k$ | $\lambda$ | Variables | Clauses |
| bibd1n.cnf | 7 | 7 | 3 | 3 | 1 | 833 | 7028 |
| bibd1y.cnf | 7 | 7 | 3 | 3 | 1 | 833 | 10080 |
| bibd2n.cnf | 6 | 10 | 5 | 3 | 2 | 1260 | 13650 |
| bibd2y.cnf | 6 | 10 | 5 | 3 | 2 | 1260 | 21745 |
| bibd3n.cnf | 7 | 14 | 6 | 3 | 2 | 2646 | 40418 |
| bibd3y.cnf | 7 | 14 | 6 | 3 | 2 | 2646 | 79093 |
| bibd4n.cnf | 9 | 12 | 4 | 3 | 1 | 2700 | 36756 |
| bibd4y.cnf | 9 | 12 | 4 | 3 | 1 | 2700 | 71865 |
| bibd5n.cnf | 8 | 14 | 7 | 4 | 3 | 3640 | 58520 |
| bibd5y.cnf | 8 | 14 | 7 | 4 | 3 | 3640 | 109284 |
All ten instances are satisfiable. Each instance has two versions: the “n” version has no symmetry breaking clauses, and the “y” version has added clauses corresponding to “symmetry breaking level 3” in Prestwich.
Direct BIBD algorithms can solve these five problems very quickly Meseguer et al.. However, they turn out to be hard for current SAT solvers, and several algorithms were unable to solve instance 5 within a few minutes Prestwich.
There is some Choco code by Patrick Prosser.
| File | Type | Notes |
|---|---|---|
| bibd5y.cnf | cnf | |
| bibd5n.cnf | cnf | |
| bibd3y.cnf | cnf | |
| bibd4y.cnf | cnf | |
| bibd4n.cnf | cnf | |
| bibd1y.cnf | cnf | |
| bibd2y.cnf | cnf | |
| bibd3n.cnf | cnf | |
| bibd2n.cnf | cnf | |
| bibd1n.cnf | cnf | |
| choco.txt | txt |