trivial empty formula and empty clause formulas:

  true.cnf false.cnf

simple formulas solvable by root-level unit propagation:

  unit1.cnf unit2.cnf unit3.cnf unit4.cnf unit5.cnf unit6.cnf
  unit7.cnf unit8.cnf unit9.cnf

formulas with all clauses of the given number of variables (unsatisfiable):

  full2.cnf full3.cnf full4.cnf

equivalence checking ripple-carry vs propagate-generate adders (unsatisfiable):

  add4.cnf add8.cnf add16.cnf add32.cnf add64.cnf add128.cnf

pigeon hole formulas (all unsat):

  ph2.cnf ph3.cnf ph4.cnf ph5.cnf ph6.cnf

checking whether the given number is prime (all satisifable except last two):

  prime4.cnf prime9.cnf prime25.cnf prime49.cnf prime121.cnf prime169.cnf
  prime289.cnf prime361.cnf prime529.cnf prime841.cnf prime961.cnf
  prime1369.cnf prime1681.cnf prime1849.cnf prime2209.cnf

  prime65537.cnf prime4294967297.cnf

checking whether the number is a square of an integer (all satisfiable):

  sqrt2809.cnf sqrt3481.cnf sqrt3721.cnf sqrt4489.cnf sqrt5041.cnf
  sqrt5329.cnf sqrt6241.cnf sqrt6889.cnf sqrt7921.cnf sqrt9409.cnf
  sqrt10201.cnf sqrt10609.cnf sqrt11449.cnf sqrt11881.cnf sqrt12769.cnf
  sqrt16129.cnf sqrt63001.cnf sqrt259081.cnf sqrt1042441.cnf