CNF benchmarks for enumeration by SAT solvers

The CNF formulas tabulated below were generated from Alloy models with manually added and automatically generated symmetry breaking predicates. (For details see the SAT 2003 paper.)

benchmark
size		manualautomatic
file#solsfile#sols
BinaryTree 1 *.cnf 1 *.cnf 1
2 *.cnf 2 *.cnf 2
3 *.cnf 5 *.cnf 5
4 *.cnf 14 *.cnf 17
5 *.cnf 42 *.cnf 75
6 *.cnf 132 *.cnf 357
7 *.cnf 429 *.cnf 1866
8 *.cnf 1430 *.cnf 10286
9 *.cnf 4862 *.cnf 60616
LinkedList 1 *.cnf 1 *.cnf 1
2 *.cnf 2 *.cnf 3
3 *.cnf 5 *.cnf 11
4 *.cnf 15 *.cnf 92
5 *.cnf 52 *.cnf 567
6 *.cnf 203 *.cnf 5975
7 *.cnf 877 *.cnf 52392
8 *.cnf 4140 *.cnf 734296
9 *.cnf 21147 *.cnf memory
TreeMap 1 *.cnf 2 *.cnf 4
2 *.cnf 2 *.cnf 6
3 *.cnf 3 *.cnf 12
4 *.cnf 8 *.cnf 40
5 *.cnf 14 *.cnf 120
6 *.cnf 20 *.cnf 322
7 *.cnf 35 *.cnf 1160
8 *.cnf 64 *.cnf 4185
9 *.cnf 122 *.cnf 16180
HashSet 1 *.cnf 1 *.cnf 1
2 *.cnf 3 *.cnf 3
3 *.cnf 10 *.cnf 10
4 *.cnf 35 *.cnf 39
5 *.cnf 126 *.cnf 156
6 *.cnf 462 *.cnf 693
7 *.cnf 1716 *.cnf 3172
8 *.cnf 6435 *.cnf 15011
9 *.cnf 24310 *.cnf 73519
HeapArray 1 *.cnf 4
2 *.cnf 15
3 *.cnf 66
4 *.cnf 320
5 *.cnf 1919
6 *.cnf 13139
7 *.cnf 117562
8 *.cnf 1005075

This page was last updated on Jul 25, 2003. It is maintained by Sarfraz Khurshid and Darko Marinov.