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
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