z3 pseudo-randomly hangs while parsing through a SAT Model

Question

I'm using the available Python Z3 API and using pretty standard code to print out the SAT model(s).

I'll leave out the extraneous bits (Full Example Here), regardless here is the big picture:

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 " "

To which I get results that looks like this (95% of the time):

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

But pseudo-randomly this happens (it only happens for specific problems, but reoccurs exactly at the same point each time):

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

At which point, python continues to run endlessly.

Any thoughts or suggestions would be appreciated.

Could you provide a link to a complete example that produces the behavior described above? We do not have enough information to diagnose the problem. — Leonardo de Moura, Feb 05 '13 at 18:06

score 1 · Accepted Answer · answered Feb 06 '13 at 00:50

There is no problem with the script you put in the link above. It is just hard to solve the instance for bits=6. It is probably unsatisfiable, but Z3 will take a long time to prove it. I attached the output I got in the end of the post. If the output is truncated in your system, you may try to use

sys.stdout.flush()

in the end of each iteration. It will force Python to flush the results to standard output. You may also use a timeout to interrupt Z3 when it can't solve the problem in less than x milliseconds. For example, for setting a timeout of 60 seconds, you should include the following command after s = Solver()

s.set("timeout", 60000)

Z3 will return unknown instead of unsat when the timeout is reached. You may decide to interpret the timeout as "probably" unsat. You may also force Z3 to display verbose messages. You can use them to check whether is dead or not. To enable verbose messages, we should include

set_option("verbose", 10)

Z3 will display many messages such as:

(sat-restart :conflicts 28553852 :decisions 35506087 :restarts 39751 :clauses 11002 :learned 297311 :gc-clause 28045187 :memory 103.26 :time 6557.84)

Here is the output produced by your script on my machine:

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, 20123428, 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,

Thank you. Adding the `sys.stdout.flush()` to the end of each iteration seemed to have worked (in my computations 6 was the lower bound that I did not expect to be sat.) As a side note - is there anything you would recommend in terms of code refactoring to "play nicer" with z3. — mborowczak, Feb 06 '13 at 03:16
Trying `s.set("timeout", 30000)` and even `s.set("timeout", 3)` did not result in early termination for any of the iterations, including the last case (bits=6) - any thoughts? — mborowczak, Feb 06 '13 at 04:28

z3 pseudo-randomly hangs while parsing through a SAT Model

1 Answers1