# A sample CNF collection
### Corner cases
If you try to build your SAT solver from scratch, they are corner cases you have to pay attention.
- [empty-clause.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/empty-clause.cnf)
- [empty-form.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/empty-form.cnf)
### Basic examples
If you think to complete CDCL algorithm, check with them.
- [sample.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/sample.cnf)
- [unsat.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unsat.cnf)
- [uf8.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf8.cnf)
- [uf20-01.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf20-01.cnf)
### Midde scale problems
And you think your solver is great, try them. 3-SAT problems (N=360) are hard. But your solver must solve them.
- [uf100-010.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf100-010.cnf)
- [uf250-02.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf250-02.cnf)
- [unif-k3-r4.25-v360-c1530-S1028159446-096.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf)
- [unif-k3-r4.25-v360-c1530-S1293537826-039.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf)
### Problems from the real competition
If you catched up the implementations of modern solvers and reasech trend, try it.
- [a_rphp035_05.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/a_rphp035_05.cnf)