View On Github

Ever wanted to create a preimage of an arbitrary __G__ame __O__f __L__ife pattern? Running a simulated version of the game of life is very simple. However, as GOL is in fact turing complete, running it backwards is rather hard. In fact we know that there are so called garden of eden patterns that do not have any predecsessor. If one restricts the world to a fixed size, GOL is still able to compute arbitrary boolean functions. As a consequence, inverting the direction of time in GOL is rather difficult. Others have used rather complex algorithms to run a reverse GOL. Here we simply implement the evaluation rules of GOL in an SMT formula and use boolector to generate preimages. Using this approach, we can find preimages in a matter of seconds even for very large instances. In our case, the search space contains 525 bits or

109836762562089755439710412785302291476310964802292886550311415346968690934362496833960954250583272879636740982263693728593951807995466301001184452657840914432.

possible inputs. This nicely demonstrates the power of SMT solvers to quickly find solutions for NP-Hard problems that otherwise require rather clever algorithms to be solved efficiently.

Using this approach to generate a preimage for the ASCII-art string “COCO” yields a preimage, that after exactly four steps turns into the intended image!

[generation 0]
        o   o   o oooo         oo     
   oo   o  oo    oo  o  oo oo   o     
     oooo  o    o     o ooo ooo  o    
   oo  o o  ooo  oo   ooo oo          
     o        ooo ooo o       o oo    
o  ooo  oo o o   o    oo o  oo        
o               oo  oo o      oo  o   
o     o  o o    o oo ooooooo o        

[generation 1]
   o    oo  o  oo o  o  ooo oo        
    ooo oo oo   o o  oooo  oo o oo    
     oo  ooo    o    oo      o        
    o  o    ooo   o   o o ooo oooo    
     oo  oo    oo  o     ooooo        
    oo        o        oo    o  oo    
oo  oo  oo  o   o  oo      o  o       
        oo oo  oo oo o ooo o o o      

[generation 2]
        oo   oooo oooo    o o o       
    o o     o   o   o   o oo  o       
         o     o        ooo           
    o  oo   ooo oo   ooo      ooo     
      o        o                      
        o o     o  oo   oo   oo       
    oo  oooooo  ooooo o  oo  oooo     
       o   oo     o  o  o  o o        

[generation 3]
     o      o             o  o        
        oo   o  oo  oo  o    o        
     o oo   o oo o   oo o oo  o       
       oo    oo o     oooo     o      
        oo   ooo o  ooooo    o        
     o oo o o  oo   oo  ooo  o        
       oo    o  o      o  o    o      
             o    o  o  o   oo        

[generation 4]
                                      
      oooo  oooooo  oooo  ooooo       
      o     o    o  o     o   o       
      o     o    o  o     o   o       
      o     o    o  o     o   o       
      o     o    o  o     o   o       
      oooo  oooooo  oooo  ooooo