The Boolean Satisfiability Problem SAT is a core of NPcomplete problems and is central in the theory of computation. Finding challenging benchmarks for the satisfiability problem is not only of significance for the experimental evaluation of SAT algorithms but also of interest to the theoretical computer science community. Identifying new challenging SAT benchmarks is also an important purpose of every years SAT competition where the benchmarks are usually divided into three categories: randomly generated uniform kSAT, applications and crafted. Although there have been a large number and various types of SAT benchmarks available for testing, the benchmarks which are guaranteed to be satisfiable are still in short supply. Recently, we proposed a new method to generate hard satisfiable problem instances.

Website: http://www.nlsde.buaa.edu.cn/~kexu/benchmarks/benchmarks.htm