z3在通过SAT模型解析时伪随机挂起

Question

我正在使用可用的Python Z3 API并使用相当标准的代码打印出SAT模型。

我就离开了多余的比特（Full Example Here），不管这里是一番景象：

for bits in range(HIGH, LOW, -1): 
    var1, var2 ... varn = BitVecs('var1 var2 ... varn', bits) 
    s = Solver(); 
    s.add(...) 
    ... 

    if(s.check() == sat): 
     print "Sat, %d," %(bits), 
     m = s.model() 
     for d in m.decls(): 
      print "%s," % (d.name()), 
     print " " 
     print "ASSIGN, %d," %(bits), 
     for d in m.decls(): 
      print "%s," % (m[d]), 
    else: 
     print "NotSat, %d," %(bits), 
     print " " 
     break 
    print " " 

对此我得到的结果看起来像这样（的95％的时间）：

Sat, HIGH, VAR1, VAR2, VAR3 ... VARn 
ASSIGN, HIGH, VAL1, VAL2, VAL3 ... VALn 
Sat, HIGH-1, VAR1, VAR2, VAR3 ... VARn 
ASSIGN, HIGH-1, VAL1, VAL2, VAL3 ... VALn 
... 
NotSat, SOMEVAL 

但伪随机出现这种情况（这仅发生于特定的问题，但在同一地点每次恰好再次出现）：

Sat, HIGH, VAR1, VAR2, VAR3 ... VARn 
ASSIGN, HIGH, VAL1, VAL2, VAL3 ... VALn 
Sat, HIGH-1, VAR1, VAR2 

在这一点上，python继续无休止地运行。

任何想法或建议，将不胜感激。

Answer 1

您在上面的链接中放置的脚本没有问题。只是很难解决bits=6的情况。 它可能不令人满意，但Z3需要很长时间才能证明它。 我附加了我在帖子末尾获得的输出。 如果输出在您的系统被截断，您可以尝试在每次迭代结束时使用

sys.stdout.flush() 

。它将强制Python将结果刷新到标准输出。 如果在小于x毫秒内无法解决问题，您也可以使用超时来中断Z3。例如，对于设置60秒超时，你应该包括后s = Solver()

s.set("timeout", 60000) 

Z3以下命令将返回unknown而不是unsat达到超时时。您可能会决定将超时解释为“可能”unsat。 您也可以强制Z3显示详细消息。您可以使用它们来检查是否死机。要启用详细的消息，我们应该包括

set_option("verbose", 10) 

Z3会显示很多信息，例如：

​​

这里是你的脚本在我的机器上产生的输出：

Sat, 28, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 28, 1194488, 2, 138352652, 27828345, 8323715, 255074345, 148059146, 45669120, 59311259, 36160098, 43520123, 171745797, 20100107, 55836791, 87065373, 174311427, 325679, 44106461, 17417102, 146868180, 120734802, 3190244, 68039782, 159445796, 61293076, 17065817, 207814763, 50496350, 
Sat, 27, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 27, 127374544, 2292862, 99672473, 2675455, 109553908, 31909971, 59861451, 41730414, 54510094, 63370004, 130863, 98670875, 52005358, 117596054, 103086442, 102094768, 85953361, 12855291, 113728523, 132186876, 133366378, 112477583, 20121855, 8079423, 95241842, 15701556, 108466982, 15861679, 
Sat, 26, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 26, 3948768, 14692617, 19776512, 120332, 24121729, 17236013, 34409608, 59052072, 34681936, 1114895, 13634601, 57705476, 2457863, 389249, 33615106, 34546177, 24264721, 21889794, 1217858, 34496580, 50476161, 50346252, 3080465, 34345251, 6372864, 42188865, 18025490, 5243087, 
Sat, 25, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 25, 21548816, 14681017, 11618883, 6687600, 17326840, 22114504, 25792662, 12517432, 12183, 20008097, 18027047, 324389, 17106676, 16967429, 29899522, 5050707, 29494411, 3188854, 11813403, 22317095, 3749937, 3097638, 741939, 21964992, 838083, 13687553, 33226832, 3673677, 
Sat, 24, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 24, 16510219, 16682171, 15519598, 10477281, 10481616, 11514364, 15334059, 14871548, 12107387, 14782459, 196543, 3931864, 12516875, 15925188, 15121231, 15631351, 3145572, 258039, 5197787, 3799546, 9433947, 785909, 1699323, 1569788, 9158599, 3662718, 3407842, 16662241, 
Sat, 23, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 23, 4337951, 7815728, 1113412, 31704, 1209944, 2591336, 857041, 1035016, 117610, 582206, 6597155, 6615137, 8129736, 5134355, 3227767, 471536, 3937363, 5257644, 6411017, 3152566, 1937690, 728177, 2962482, 4215659, 56802, 5118725, 6276097, 257728, 
Sat, 22, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 22, 312133, 421384, 1109512, 2098659, 1835070, 2388161, 1193540, 3289102, 3752454, 503811, 1012736, 3020290, 1313415, 77903, 3160288, 14050, 1852864, 281355, 3023648, 1089598, 1967040, 819952, 1753640, 21149, 487472, 1878019, 1197319, 1262740, 
Sat, 21, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 21, 64995, 390953, 1700562, 1302766, 1187453, 1314795, 842519, 1785696, 1988188, 1849171, 1571340, 1862031, 28668, 193211, 1179395, 1040004, 1226595, 1545878, 1328063, 2093106, 1139447, 799486, 383535, 2040975, 687303, 1112985, 1388153, 1241406, 
Sat, 20, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 20, 93862, 686853, 903880, 373532, 698796, 985932, 43949, 858080, 174578, 47915, 130848, 963016, 918415, 306040, 64325, 905514, 989578, 176359, 258604, 409504, 749645, 111586, 142798, 137078, 109451, 983229, 191657, 593861, 
Sat, 19, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 19, 339712, 331803, 160304, 13928, 53404, 107824, 136717, 102988, 67639, 319526, 265153, 132127, 145954, 156321, 86314, 284993, 343104, 8659, 329392, 25444, 20229, 52880, 73837, 251, 337296, 319499, 394354, 312610, 
Sat, 18, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 18, 69753, 52231, 229778, 3667, 247041, 206608, 53302, 208400, 61705, 69959, 3025, 43654, 181002, 65024, 53554, 78001, 160066, 90892, 213698, 188612, 1009, 74179, 90761, 127744, 78897, 78371, 200264, 258052, 
Sat, 17, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 17, 94080, 86358, 31782, 34292, 13221, 59266, 21383, 83749, 36259, 46854, 69743, 19914, 49596, 99267, 90828, 117346, 47637, 81456, 35700, 61188, 106663, 95584, 9133, 36216, 99132, 99996, 53923, 45459, 
Sat, 16, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 16, 40904, 29469, 60171, 20719, 15453, 46111, 50767, 7759, 63596, 21475, 63057, 52579, 60569, 19687, 24401, 31907, 64588, 56560, 49885, 62755, 48930, 7981, 62356, 48325, 32394, 3919, 57407, 58322, 
Sat, 15, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 15, 32194, 19956, 13227, 25303, 17374, 10815, 24304, 5607, 24348, 32193, 1918, 11934, 15820, 25935, 11118, 4074, 8702, 22939, 24402, 32200, 4028, 29086, 30003, 32530, 29046, 29372, 29790, 29925, 
Sat, 14, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 14, 1889, 9448, 3378, 8787, 4316, 2520, 711, 1008, 4875, 12380, 4810, 12690, 1714, 5968, 9034, 411, 811, 5646, 7224, 7685, 7944, 15440, 461, 7104, 14418, 4840, 4217, 3040, 
Sat, 13, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 13, 6647, 5951, 7359, 7805, 3069, 6007, 7119, 7791, 1023, 5879, 2943, 7023, 8051, 1791, 7925, 8079, 6071, 4607, 2015, 6651, 7667, 2815, 7487, 7421, 6847, 5883, 5999, 8118, 
Sat, 12, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 12, 1823, 1788, 3064, 3727, 1271, 3309, 3546, 3790, 955, 3562, 3825, 1499, 2287, 2539, 1767, 3869, 3419, 2934, 4017, 3495, 3050, 1655, 2033, 1532, 2686, 2877, 3036, 1935, 
Sat, 11, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 11, 1973, 751, 1782, 1771, 1523, 983, 1913, 735, 2019, 1963, 1991, 507, 958, 1018, 1275, 1659, 2003, 1263, 1343, 1847, 1375, 2034, 1907, 1899, 1532, 1463, 503, 1011, 
Sat, 10, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 10, 132, 9, 66, 40, 320, 5, 33, 136, 260, 96, 3, 20, 258, 130, 264, 17, 36, 129, 528, 10, 48, 384, 288, 65, 544, 514, 12, 80, 
Sat, 9, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 9, 416, 37, 388, 208, 22, 352, 274, 322, 112, 268, 193, 104, 196, 266, 385, 146, 296, 56, 11, 70, 69, 138, 336, 448, 324, 35, 261, 176, 
Sat, 8, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 8, 197, 46, 105, 225, 201, 60, 99, 92, 15, 150, 113, 149, 51, 27, 210, 53, 172, 163, 184, 54, 23, 57, 216, 240, 156, 43, 178, 29, 
Sat, 7, st14, st20, st9, st17_n, st3, st6_n, st15, st10, st15_n, st1, st11, st18, st19, st4_n, st5, st9_n, st8, st2, st2_n, st16, st6, st17, st13, st16_n, st4, st7, st12, st19_n, 
ASSIGN, 7, 46, 45, 15, 77, 78, 114, 57, 83, 108, 51, 106, 113, 23, 120, 43, 54, 92, 105, 60, 30, 71, 102, 53, 75, 29, 27, 89, 58,