| proposed by | Steven Prestwich s.prestwich@cs.ucc.ie |
These are the first five BIBD generation problems listed in [1],
encoded as described in [3] using the standard DIMACS format (readable
by most current SAT solvers). The files are:
filename: 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 [3].
Direct BIBD algorithms can solve these five problems very quickly [2].
However, they turn out to be hard for current SAT solvers, and several
algorithms were unable to solve instance 5 within a few minutes [3].