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$VariablesClauses
bibd1n.cnf773318337028
bibd1y.cnf7733183310080
bibd2n.cnf610532126013650
bibd2y.cnf610532126021745
bibd3n.cnf714632264640418
bibd3y.cnf714632264679093
bibd4n.cnf912431270036756
bibd4y.cnf912431270071865
bibd5n.cnf814743364058520
bibd5y.cnf8147433640109284

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
bibd5y.cnf cnf
bibd5n.cnf cnf
bibd4y.cnf cnf
bibd4n.cnf cnf
bibd3y.cnf cnf
bibd3n.cnf cnf
bibd2y.cnf cnf
bibd2n.cnf cnf
bibd1y.cnf cnf
bibd1n.cnf cnf
choco.txt txt