|||
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的实例平均是最难解决的。
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-12-24 09:42
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社