You have a lot of huge, real-wold (industrial) examples on the website of the SAT 2017 competition. Be careful, however, these files are really huge (zip files

You have a lot of huge, real-wold (industrial) examples on the website of the SAT 2017 competition. Be careful, however, these files are really huge (zip files in Gbytes) and the CNF files come "as is", i.e with no explanation about the underlying problem: https://baldur.iti.kit.edu/sat-competition-2017/benchmarks/ https://baldur.iti.kit.edu/sat-competition-2017/benchmarks/ Classical one-player puzzles can be represented easily, and I'll include a tutorial and generators for those in the short run: sudoku and 8 queens, for instance. There's an article explaining how to represent the sudoku problem here : http://sat.inesc.pt/~ines/publications/aimath06.pdf http://sat.inesc.pt/~ines/publications/aimath06.pdf (section 3). As for pathological problems: the usual testcase for SAT solvers are random problems. They can be generated easily (I'll probably include a generator for them in the repository). You choose a number of variables , n (around n=300 things start to get interesting) and randomly generate n x 4.2 clauses (this is a sweet spot: less clauses and the problem tends to be easily solved, more clauses and it becomes easy to prove it cannot be solved). Those clauses must contain 3 literals, chosen randomly. Those problems are very hard to solve, even with a relatively small number of variables and clauses. But they are not that interesting in practice, because real-world problems are very different, they more structured and easier to solve.