Toot

Written by Mark Gritter on 2024-11-01 at 08:28

OK, a simpler starting point. Consider just the case

for (i = 0; i < left_out; i++)

rooms[rnd_room()].r_flags |= ISGONE;

with left_out = 2. How many times can rnd_room() loop in the worst case? It looks for a room number in [0,8] which does not already have ISGONE set.

Let's write a Z3 model that searches for the first random number = 2, the second unconstrained, and the third, fourth, fifth, ... all equal (mod 9 of course) to the second number.

for loops in range( 1, 20 ):

print( loops, "loops" )

s = Solver()

s.add( left_out == 2 )

gone_1 = nth_rnd(1,9)

for n in range( loops ):

    s.add( nth_rnd(2 + n, 9) == gone_1 )

if s.check() == sat:

    print( s.model() )

else:

    print( "Unsatisfiable" )

    break

It ran quickly enough up to 6 loops, but 7 is taking a while so many be unsatisfiable.

=> View attached media | View attached media

=> More informations about this toot | View the thread | More toots from markgritter@mathstodon.xyz

Mentions

Tags