#!/usr/bin/python3 import os, SAT_lib, GoL_SAT_utils, SL_common, my_utils W=20 # WIDTH H=20 # HEIGHT s=SAT_lib.SAT_lib() VAR_FALSE=s.const_false grid=[[s.create_var() for w in range(W)] for h in range(H)] def try_again (): # rules for the main part of grid for r in range(H): for c in range(W): s.add_clauses (SL_common.gen_SL(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W), GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W))) # cells behind visible grid must always be false: for c in range(-1, W+1): for r in [-1,H]: s.add_clauses (GoL_SAT_utils.cell_is_false(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W), GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W))) for c in [-1,W]: for r in range(-1, H+1): s.add_clauses (GoL_SAT_utils.cell_is_false(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W), GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W))) # each row must contain at least one cell! for r in range(H): s.OR_always ([GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W) for c in range(W)]) # each column must contain at least one cell! for c in range(W): s.OR_always ([GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W) for r in range(H)]) # make result denser: lst=[] for r in range(H): for c in range(W): lst.append(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W)) # divide them all by chunks and add to clauses: CHUNK_LEN=3 for c in my_utils.partition(lst,int(len(lst)/CHUNK_LEN)): s.add_clause(c) if s.solve()==False: return None t=GoL_SAT_utils.SAT_solution_to_grid(grid, VAR_FALSE, s.solution, H, W) GoL_SAT_utils.print_grid(t) GoL_SAT_utils.write_RLE(t) return t while True: solution=try_again() if solution==None: break s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(solution, grid, VAR_FALSE, H, W))) s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.reflect_vertically(solution), grid, VAR_FALSE, H, W))) s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.reflect_horizontally(solution), grid, VAR_FALSE, H, W))) # is this square? if W==H: s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,1), grid, VAR_FALSE, H, W))) s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,2), grid, VAR_FALSE, H, W))) s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,3), grid, VAR_FALSE, H, W))) print ("")