## SAT encodings

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.

## Choco model

There is some Choco code by Patrick Prosser.

## Files

File Type Notes
bibd1n.cnf cnf
bibd1y.cnf cnf
bibd2n.cnf cnf
bibd2y.cnf cnf
bibd3n.cnf cnf
bibd3y.cnf cnf
bibd4n.cnf cnf
bibd4y.cnf cnf
bibd5n.cnf cnf
bibd5y.cnf cnf
BIBD.essence Essence
bibd.mzn MiniZinc
Bibd.py Numberjack
sicstus_csplib028.pl SICStus Prolog
choco.txt txt