SatZ（http://blog.sciencenet.cn/blog-2322490-991076.html）的作者提供了一个k-SAT实例生成器程序：gencnf+.c，为对SAT问题感兴趣的网友提供一个比较自己和他人工作的工具。

1. To compile under Linux or Unix :

gcc gencnf+.c -O3 -o gencnf+

2. To generate a set of (s2-s1+1) different k-sat instances of n variables, m clauses with seeds from s1 to s2 ：

./gencnf+ n m k s1 s2

For example, to generate a set of 100 3-SAT instances with 100 vars, 425 clauses with seeds from 1 to 100:

./gencnf+ 100 425 3 1 100

The 100 instances are named as:

v100c425L3g1

v100c425L3g2

…

v100c425L3g100

注：实验表明子句数与变元数之比为4.25的实例平均是最难解决的。

gencnf+.c