众所周知SAT问题（SAtisfiability Problem）是逻辑学的一个基本问题，也是算法理论的一个核心问题，众多学者已经为此做出了大量的工作，开发出许多算法程序，称“SAT求解器（SAT solver）”（https://en.wikipedia.org/wiki/Category:SAT_solvers），这里介绍其中的一个完备算法的程序－SatZ，供感兴趣的网友运行测试实例，以开阔自己的视野。

1，介绍SatZ的文章

Chu Min LI & Anbulagan, "Heuristics based on unit propagation for satisfiability problems", in proceedings of 15th International Joint Conference on Artificial Interlligence (IJCAI'97), Morgan Kaufmann Publishers, ISBN 1-55860-480-4, Page 366-371, Japon, 1997.

IJCAI97Anbulagan.pdf

2，程序satz215.c

编译程序命令：gcc satz215.c -O3 -o satz215

注：在Linux或Unix环境下编译。若编译结果出现“warning”信息，不影响运行。

3，实例

这里给出二个实例：v200c850g1，v300c1275g1

实例文件格式说明：v300c1275g1

c germe 1

p cnf 300 1275// 300个变元，1275个子句

-99 -212 -219 0// 子句1： ¬x99 v ¬x212 v ¬x219

109 -137 -162 0// 子句2：x109 v ¬x137 v ¬x167

…

更多的实例见：http://www.satlib.org。

4，执行程序

在“Mac(2.8 Ghz Intel Core i5) OS X”机器上运行的结果：

执行程序：satz215 v300c1275g1

****the instance is unsatisfiable *****

NB_MONO= 2423, NB_UNIT= 483701, NB_BRANCHE= 11889, NB_BACK= 6071

Program terminated in 1.030 seconds.

satz215 v300c1275g1 1.030 11889 6071 698039 104683 0 300 1275 108 352806 61652

执行程序：satz215 v200c850g1

****the instance is satisfiable *****

****verification of solution is OK****

NB_MONO= 104, NB_UNIT= 8159, NB_BRANCHE= 251, NB_BACK= 123

Program terminated in 0.020 seconds.

satz215 v200c850g1 0.020 251 123 25822 2071 1 200 850 97 7276 1220

显示可满足实例（v200c850g1）的解：more satx.sol

-1 -2 3 -4 5 6 7 8 -9 -10 -11 12 -13 14 -15 -16 17 18 19 20 21 22 -23 -24 -25 -26 27 -28 -29 30 31 32 -33 -34 -35 36 -37 -38 39 -40 41 -42 43 44 -45 46 -47 48 49 -50 -51 52 -53 -54 55 -56 57 -58 59 -60 -61 62 -63 64 -65 -66 -67 -68 -69 70 -71 -72 -73 74 75 -76 77 -78 79 -80 81 -82 -83 84 85 -86 87 88 89 90 91 -92 93 94 95 -96 97 -98 99 -100 101 102 103 -104 -105 106 107 -108 109 110 -111 112 113 114 115 116 -117 118 -119 -120 121 -122 123 124 -125 126 -127 128 129 130 131 132 133 -134 -135 136 137 -138 139 140 141 -142 143 -144 -145 146 -147 148 149 150 -151 -152 153 -154 -155 -156 -157 158 -159 -160 161 162 -163 164 -165 -166 167 -168 -169 -170 171 -172 173 174 -175 -176 177 178 179 180 181 182 183 184 -185 186 187 188 189 -190 191 -192 -193 -194 195 -196 197 198 199 200    

解的说明：x1=0, x2=0, x3=1, x4=0, …

satz215.c  v300c1275g1 v200c850g1