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