#!/usr/bin/python3

# generate maximum density still life using MaxSAT solver

# dennis(a)yurichev.com, 2020

import os
import GoL_SAT_utils
import SL_common
import SAT_lib
import collections

# WIDTH, HEIGHT
#H,W = 13,13
#H,W = 7,7
H,W = 6,6

s=SAT_lib.SAT_lib(maxsat=True)
VAR_FALSE=s.const_false

grid=[[s.create_var() for w in range(W)] for h in range(H)]

# 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)))
        #for cl in clauses:
        #    s.add_clause(cl.split(' '))

# 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 cl in clauses:
        #    s.add_clause(cl.split(' '))
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)))
        #for cl in clauses:
        #    s.add_clause(cl.split(' '))

for r in range(H):
    for c in range(W):
         s.add_soft_clause([GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W)], 1)

assert s.solve()
stat=collections.Counter(list(s.solution.values())[2:]) # skip first False/True
#print ("Stat:")
#print (stat)
print ("cells: %d" % stat[True])
print ("density: %f" % (float(stat[True]) / float(H*W)))

grid=GoL_SAT_utils.SAT_solution_to_grid(grid, VAR_FALSE, s.solution, H, W)

GoL_SAT_utils.print_grid(grid)
GoL_SAT_utils.write_RLE(grid)