# パッケージ

# %matplotlib inline
import numpy as np
from collections import OrderedDict
import os
import math
import re
import glob
import time
import random
import itertools

if __name__ == '__main__':
    import cv2 as cv # opencv
    import matplotlib
    import matplotlib.pyplot as plt # matplotlibの描画系
    from matplotlib import cm

def split(string):
    re_list = re.split('[ X#@,()\t\n]',string)
    while '' in re_list:
        re_list.remove('')
    return re_list
    
def readQ(filename):
    Q = {'BLOCK':{}}
    max_l = 0
    with open(filename, 'r') as file:
        while True:
            str_line = file.readline()
            if not str_line:
                break
            result = split(str_line)
            if result == []:
                continue
            if result[0] == 'SIZE':
                Q['w'] = int(result[1])
                Q['h'] = int(result[2])
            elif result[0] == 'BLOCK_NUM':
                Q['num_b'] = int(result[1])
                Q['n'] = Q['num_b']
            elif result[0] == 'BLOCK':
                index = int(result[1])
                w = int(result[2])
                h = int(result[3])
                bs = Q['BLOCK']
                cells = {}
                bs[index] = {'index':index,'w':w,'h':h,'cells':cells}
                for i in range(h):
                    subline = file.readline()
                    subr = split(subline)
                    for j in range(w):
                        if subr[j] != '0':
                            cells[(j,i)] = subr[j]
                            if subr[j] != '+':
                                num = int(subr[j])
                                if num > max_l:
                                    max_l = num
    Q['num_l'] = max_l
    return Q
def readA(filename):
    A = {'BLOCK':{}}
    with open(filename, 'r') as file:
        i = 0
        while True:
            str_line = file.readline()
            if not str_line:
                break
            result = split(str_line)
            if result == []:
                continue
            if result[0] == 'SIZE':
                A['w'] = int(result[1])
                A['h'] = int(result[2])
                A['map'] = np.zeros((A['h'],A['w']), dtype=int)
            elif result[0] == 'BLOCK':
                index = int(result[1])
                x = int(result[2])
                y = int(result[3])
                bs = A['BLOCK']
                cells = {}
                bs[index] = {'index':index,'x':x,'y':y}
            else:
                for j in range(A['w']):
                    A['map'][i,j] = int(result[j])
                i += 1       
    return A

def strA(A):
    r = []
    w = A['w']
    h = A['h']
    num_b = A['num_b']
    r.append(f'SIZE {w}X{h}\n')
    for i in range(h):
        r.append(','.join(map(str,A['map'][i])))
        r.append('\n')
    block_list = A['BLOCK']
    for i in range(1, num_b+1):
        x = block_list[i]['x']
        y = block_list[i]['y']
        r.append(f'BLOCK#{i} @({x},{y})\n')
    return ''.join(r)

def index2color(index, mode='cell'):
    if mode == 'cell':
        if index == -1:
            R,G,B,Alpha = 1,1,1,1
        else:
            R,G,B,Alpha = cm.tab20((index*2)%20)
    else:
        R,G,B,Alpha = cm.tab20((index*2+1)%20)
    return np.array([R,G,B])

def QA2img(Q,A):
    w_grid = 5
    w_line = 25
    len_cell = 50
    margin = (len_cell + w_grid - w_line)//2
    white = [1,1,1]
    black = [0,0,0]
    red = [1,0,0]
    w_max, h_max = Q['w'],Q['h']
    w,h,n = A['w'],A['h'],Q['n']
    map_A = A['map']
    bs_q = Q['BLOCK']
    bs_a = A['BLOCK']
    img = np.zeros((h_max*len_cell+w_grid,w_max*len_cell+w_grid,3))
    img[:,:] = white
    img[[i for i in range(h_max*len_cell+w_grid) if (i%len_cell)<w_grid],:] = black
    img[:,[j for j in range(w_max*len_cell+w_grid) if (j%len_cell)<w_grid]] = black
    img[0:h*len_cell,0:w_grid] = red
    img[0:h*len_cell,w*len_cell:w*len_cell+w_grid] = red
    img[0:w_grid,0:w*len_cell] = red
    img[h*len_cell:h*len_cell+w_grid,0:w*len_cell+w_grid] = red

    for index in range(1, n+1):
        x, y = bs_a[index]['x'], bs_a[index]['y']
        cells = bs_q[index]['cells']
        for dx,dy in cells.keys():
            X = (x+dx)*len_cell
            Y = (y+dy)*len_cell
            img[Y+w_grid:Y+len_cell,X+w_grid:X+len_cell] = index2color(index-1, 'cell')
            
    for i in range(h):
        for j in range(w):
            index_line = map_A[i][j]
            if index_line == 0:
                continue
            X = j*len_cell
            Y = i*len_cell
            Xp = X+len_cell
            Yp = Y+len_cell
            img[Y+margin:Y+margin+w_line,X+margin:X+margin+w_line] = index2color(index_line, 'line')
            if j+1<w and map_A[i][j+1] == index_line:
                img[Y+margin:Y+margin+w_line,X+margin+w_line:X+margin+len_cell] = index2color(index_line, 'line')
                    
            if i+1<h and map_A[i+1][j] == index_line:
                img[Y+margin+w_line:Y+margin+len_cell,X+margin:X+margin+w_line] = index2color(index_line, 'line')
                            
            cv.putText(img, f'{index_line}', (X+margin,Y+margin+w_line-3), cv.FONT_HERSHEY_PLAIN, 1.5, (.1,.1,.1), 2)
                    
    return img
def show(index, read=None):
    
    paths = sorted(glob.glob(f"../Q*.txt"))
    Q = readQ(paths[index])
    if read is None:
        A = readA(f'../A{paths[index][4:7]}.txt')
    else:
        A = read
        
    print(f'A{paths[index][4:7]}.txt')
    img = QA2img(Q,A)
    wQ = Q['w']
    hQ = Q['h']
    wA = A['w']
    hA = A['h']
    print(f'問題サイズ{wQ}×{hQ},解答サイズ{wA}×{hA}')
    print(f'矩形領域の割合{(wA*hA)/(wQ*hQ)}')
    img_uint8 = (img*255).astype(int)
    R = np.array(img_uint8[:,:,2])
    B = np.array(img_uint8[:,:,0])
    img_uint8[:,:,0] = R
    img_uint8[:,:,2] = B
    cv.imwrite(f'A{index+1:03}.png', img_uint8)
      
    plt.imshow(img)
      
def add(e, _dict):
    if e not in _dict.keys():
        _dict[e] = len(_dict) + 1
def print_cnf(nodes, cnfs, filename='p.txt'):
    s = []
    with open(filename, 'w') as file:
        s.append(f'p cnf {len(nodes)} {len(cnfs)}\n')
        file.write(''.join(s))
        for cnf in cnfs:
            s_sub = ''
            for e in cnf:
                s_sub += ('' if cnf[e] == '1' else '-')+f'{nodes[e]} '
            s_sub += '0\n'
            file.write(s_sub)
            #s.append(s_sub)
    #print(''.join(s))

def print_cnf2(nodes, cnfs, filename='p.txt'):
    s = []
    s.append(f'p cnf {len(nodes)} {len(cnfs)}\n')
    for cnf in cnfs:
        cnf = [str(i) for i in cnf]
        s.append((' '.join(cnf))+' 0\n')
    with open(filename, 'w') as file:
        file.write(''.join(s))

def _get_map_b(Q,A):
    map_b = np.zeros((A['h'], A['w']), dtype=int)
    for b in range(1, Q['num_b']+1):
        x = A['BLOCK'][b]['x']
        y = A['BLOCK'][b]['y']
        for dx,dy in Q['BLOCK'][b]['cells'].keys():
            map_b[y+dy,x+dx] = b
    return map_b

def optimize(Q, A):
    Q, A = del_blank(Q, A)
    num_b = Q['num_b']
    num_l = Q['num_l']
    map_l = A['map']
    h, w = map_l.shape
    map_b = _get_map_b(Q,A)

    # 左に動かす
    while True:
        updated = False
        for b in range(1,num_b+1):
            cells = Q['BLOCK'][b]['cells']
            x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y']
            canMove = True
            for dx,dy in cells.keys():
                if cells[(dx,dy)] != '+':
                    # とりあえず配線のあるブロックは動かさない
                    canMove = False
                    break
                if x+dx-1 < 0:
                    canMove = False
                    break
                if map_b[y+dy,x+dx-1] != 0 and map_b[y+dy,x+dx-1] != b:
                    canMove = False
                    break
                if map_l[y+dy,x+dx-1] != 0:
                    canMove = False
                    break
            if not canMove:
                continue
            # 左に動かせる!
            A['BLOCK'][b]['x'] = x-1
            for dx,dy in cells.keys():
                map_b[y+dy,x+dx] = 0
            for dx,dy in cells.keys():
                map_b[y+dy,x+dx-1] = b
            updated = True
        if not updated:
            break
        else:
            Q, A = del_blank(Q, A)
            map_b = _get_map_b(Q,A)
            h, w = map_b.shape
    # 上に動かす
    while True:
        updated = False
        for b in range(1,num_b+1):
            cells = Q['BLOCK'][b]['cells']
            x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y']
            canMove = True
            for dx,dy in cells.keys():
                if cells[(dx,dy)] != '+':
                    # とりあえず配線のあるブロックは動かさない
                    canMove = False
                    break
                if y+dy-1 < 0:
                    canMove = False
                    break
                if map_b[y+dy-1,x+dx] != 0 and map_b[y+dy-1,x+dx] != b:
                    canMove = False
                    break
                if map_l[y+dy-1,x+dx] != 0:
                    canMove = False
                    break
            if not canMove:
                continue
            # 上に動かせる!
            A['BLOCK'][b]['y'] = y-1
            for dx,dy in cells.keys():
                map_b[y+dy,x+dx] = 0
            for dx,dy in cells.keys():
                map_b[y+dy-1,x+dx] = b
            updated = True
        if not updated:
            break
        else:
            Q, A = del_blank(Q, A)
            map_b = _get_map_b(Q,A)
            h, w = map_b.shape
    # 右に動かす
    while True:
        updated = False
        for b in range(1,num_b+1):
            cells = Q['BLOCK'][b]['cells']
            x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y']
            canMove = True
            for dx,dy in cells.keys():
                if cells[(dx,dy)] != '+':
                    # とりあえず配線のあるブロックは動かさない
                    canMove = False
                    break
                if x+dx+1 >= w:
                    canMove = False
                    break
                if map_b[y+dy,x+dx+1] != 0 and map_b[y+dy,x+dx+1] != b:
                    canMove = False
                    break
                if map_l[y+dy,x+dx+1] != 0:
                    canMove = False
                    break
            if not canMove:
                continue
            # 右に動かせる!
            A['BLOCK'][b]['x'] = x+1
            for dx,dy in cells.keys():
                map_b[y+dy,x+dx] = 0
            for dx,dy in cells.keys():
                map_b[y+dy,x+dx+1] = b
            updated = True
        if not updated:
            break
        else:
            Q, A = del_blank(Q, A)
            map_b = _get_map_b(Q,A)
            h, w = map_b.shape
    # 下に動かす
    while True:
        updated = False
        for b in range(1,num_b+1):
            cells = Q['BLOCK'][b]['cells']
            x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y']
            canMove = True
            for dx,dy in cells.keys():
                if cells[(dx,dy)] != '+':
                    # とりあえず配線のあるブロックは動かさない
                    canMove = False
                    break
                if y+dy+1 >= h:
                    canMove = False
                    break
                if map_b[y+dy+1,x+dx] != 0 and map_b[y+dy+1,x+dx] != b:
                    canMove = False
                    break
                if map_l[y+dy+1,x+dx] != 0:
                    canMove = False
                    break
            if not canMove:
                continue
            # 上に動かせる!
            A['BLOCK'][b]['y'] = y+1
            for dx,dy in cells.keys():
                map_b[y+dy,x+dx] = 0
            for dx,dy in cells.keys():
                map_b[y+dy+1,x+dx] = b
            updated = True
        if not updated:
            break
        else:
            Q, A = del_blank(Q, A)
            map_b = _get_map_b(Q,A)
            h, w = map_b.shape
    
    return A

def del_blank(Q, A):
    num_b = Q['num_b']
    num_l = Q['num_l']
    ## 最小矩形に更新
    map_l = A['map']
    h, w = map_l.shape
    map_b = np.zeros((h, w), dtype=int)
    for b in range(1, num_b+1):
        x = A['BLOCK'][b]['x']
        y = A['BLOCK'][b]['y']
        for dx,dy in Q['BLOCK'][b]['cells'].keys():
            map_b[y+dy,x+dx] = b
    i = 0
    while True:
        if i >= h:
            break
        if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all():
            map_l = np.delete(map_l, i, axis=0)
            map_b = np.delete(map_b, i, axis=0)
            for b in range(1, num_b+1):
                if A['BLOCK'][b]['y'] > i:
                    A['BLOCK'][b]['y'] -= 1
            h -= 1
            i -= 1
        i += 1
    j = 0
    while True:
        if j >= w:
            break
        if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all():
            map_l = np.delete(map_l, j, axis=1)
            map_b = np.delete(map_b, j, axis=1)
            for b in range(1, num_b+1):
                if A['BLOCK'][b]['x'] > j:
                    A['BLOCK'][b]['x'] -= 1
            w -= 1
            j -= 1
        j += 1
    A['map'] = map_l
    A['h'] = h
    A['w'] = w

    return Q, A

def read_satA(filename, Q, nodes, TF=None):
    with open(filename, 'r') as file:
        str_line = file.readline()
        if str_line.startswith('UNSAT'):
            print('UNSAT')
            return None
        else:
            print('SAT')
        str_line = file.readline()
        ss = str_line.split()
    if TF is None:
        TF = [False] * (len(nodes)+1)
    for num_s in ss:
        num = int(num_s)
        if num>0:
          TF[num] = True
        else:
          TF[-num] = False
    w = Q['w']
    h = Q['h']
    A = {'BLOCK':{}}
    A['w'] = w
    A['h'] = h
    A['map'] = np.zeros((h,w), dtype=int)
    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    A['num_b'] = num_b
    A['num_l'] = num_l
    for i in range(1, num_b+1):
        A['BLOCK'][i] = {'index':i,'x':0,'y':0}
    for i in range(h):
        for j in range(w):
            for b in range(1,num_b+1):
                key = f'b{b}_{j}_{i}'
                if key not in nodes.keys():
                    break
                index = nodes[key]
                if TF[index]:
                    A['BLOCK'][b]['x'] = j    
                    A['BLOCK'][b]['y'] = i
            for l in range(1,num_l+1):
                key = f'l{l}_{j}_{i}'
                if key not in nodes.keys():
                    break
                index = nodes[key]
                if TF[index]:
                    A['map'][i][j] = l
    ## 閉路の削除
    validation_map = np.zeros((h, w), dtype=int)
    check_flag = np.zeros(num_l+1)
    map = A['map']

    # 端点から探索し
    for b in range(1, num_b):
        for dx,dy in Q['BLOCK'][b]['cells'].keys():
            c = Q['BLOCK'][b]['cells'][(dx,dy)]

            # 配線でないならcontinue
            if c == '+' or c == '0':
                continue
            c = int(c)

            # 探索済みならcontinue
            if check_flag[c] == 1:
                continue

            x, y = A['BLOCK'][b]['x']+dx, A['BLOCK'][b]['y']+dy
            while True:
                validation_map[y, x] = 1
                x -= 1
                if x >= 0 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                x += 2
                if x <= w-1 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                x -= 1
                y -= 1
                if y >= 0 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                y += 2
                if y <= h-1 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                y -= 1
                break
            check_flag[c] = 1
    # validation_mapが0 => 端点と接続していない => 閉路
    A['map'] = A['map'] * validation_map
    A = optimize(Q, A)
    return A
    
def read_satA2(filename, Q, nodes, TF=None):
    with open(filename, 'r') as file:
        str_line = file.readline()
        if str_line.startswith('UNSAT'):
            print('UNSAT')
            return None
        else:
            print('SAT')
        str_line = file.readline()
        ss = str_line.split()
    if TF is None:
        TF = [False] * (len(nodes)+1)
    for num_s in ss:
        num = int(num_s)
        if num>0:
          TF[num] = True
        else:
          TF[-num] = False
    w = Q['w']
    h = Q['h']
    A = {'BLOCK':{}}
    A['w'] = w
    A['h'] = h
    A['map'] = np.zeros((h,w), dtype=int)
    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    A['num_b'] = num_b
    A['num_l'] = num_l
    for i in range(1, num_b+1):
        A['BLOCK'][i] = {'index':i,'x':0,'y':0}
    for i in range(h):
        for j in range(w):
            for b in range(1,num_b+1):
                key = f'b{b}_{j}_{i}'
                if key not in nodes.keys():
                    break
                index = nodes[key]
                if TF[index]:
                    A['BLOCK'][b]['x'] = j    
                    A['BLOCK'][b]['y'] = i
            for l in range(1,num_l+1):
                key = f'l{l}_{j}_{i}'
                if key not in nodes.keys():
                    break
                index = nodes[key]
                if TF[index]:
                    A['map'][i][j] = l

    ## 閉路の削除
    validation_map = np.zeros((h, w), dtype=int)
    check_flag = np.zeros(num_l+1)
    map = A['map']

    # 端点から探索し
    for b in range(1, num_b):
        for dx,dy in Q['BLOCK'][b]['cells'].keys():
            c = Q['BLOCK'][b]['cells'][(dx,dy)]

            # 配線でないならcontinue
            if c == '+' or c == '0':
                continue
            c = int(c)

            # 探索済みならcontinue
            if check_flag[c] == 1:
                continue

            x, y = A['BLOCK'][b]['x']+dx, A['BLOCK'][b]['y']+dy
            while True:
                validation_map[y, x] = 1
                x -= 1
                if x >= 0 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                x += 2
                if x <= w-1 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                x -= 1
                y -= 1
                if y >= 0 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                y += 2
                if y <= h-1 and map[y, x] == c and validation_map[y, x] == 0:
                    continue
                y -= 1
                break
            check_flag[c] = 1
    # validation_mapが0 => 端点と接続していない => 閉路
    A['map'] = A['map'] * validation_map
    
    ## 最小矩形に更新
    map_l = A['map']
    h, w = map_l.shape
    map_b = np.zeros((h, w), dtype=int)
    for b in range(1, num_b+1):
        x = A['BLOCK'][b]['x']
        y = A['BLOCK'][b]['y']
        for dx,dy in Q['BLOCK'][b]['cells'].keys():
            map_b[y+dy,x+dx] = b
    i = 0
    while True:
        if i >= h:
            break
        if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all():
            map_l = np.delete(map_l, i, axis=0)
            map_b = np.delete(map_b, i, axis=0)
            for b in range(1, num_b+1):
                if A['BLOCK'][b]['y'] > i:
                    A['BLOCK'][b]['y'] -= 1
            h -= 1
            i -= 1
        i += 1
    j = 0
    while True:
        if j >= w:
            break
        if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all():
            map_l = np.delete(map_l, j, axis=1)
            map_b = np.delete(map_b, j, axis=1)
            for b in range(1, num_b+1):
                if A['BLOCK'][b]['x'] > j:
                    A['BLOCK'][b]['x'] -= 1
            w -= 1
            j -= 1
        j += 1
    A['map'] = map_l
    A['h'] = h
    A['w'] = w
    return A

def debug_satA(filename, Q, nodes, TF=None):
    TF = [False] * (len(nodes)+1)
    A = read_satA(filename, Q, nodes, TF)
    w = Q['w']
    h = Q['h']
    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    for b in range(1,num_b+1):
        b_board = np.zeros((h,w),dtype=bool)
        for i in range(h):
            for j in range(w):
                key = f'b{b}_{j}_{i}'
                index = nodes[key]
                b_board[i, j] = TF[index]
        print(f'b{b}=')
        print(b_board)
    for l in range(1,num_l+1):
        l_board = np.zeros((h,w),dtype=bool)
        for i in range(h):
            for j in range(w):
                key = f'l{l}_{j}_{i}'
                index = nodes[key]
                l_board[i, j] = TF[index]
        print(f'l{l}=')
        print(l_board)
    return A
                
def debug_satA2(filename, Q, nodes, TF=None):
    TF = [False] * (len(nodes)+1)
    A = read_satA(filename, Q, nodes, TF)
    w = Q['w']
    h = Q['h']
    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    v_board = np.zeros((h-1, w),dtype=bool)
    for i in range(h-1):
        for j in range(w):
            key = f'lv_{j}_{i}'
            index = nodes[key]
            v_board[i, j] = TF[index]
    print(f'lv=')
    print(v_board)
    h_board = np.zeros((h, w-1),dtype=bool)
    for i in range(h):
        for j in range(w-1):
            key = f'lh_{j}_{i}'
            index = nodes[key]
            h_board[i, j] = TF[index]
    print(f'lh=')
    print(h_board)


#    for b in range(1,num_b+1):
#        b_board = np.zeros((h,w),dtype=bool)
#        for i in range(h):
#            for j in range(w):
#                key = f'b{b}_{j}_{i}'
#                index = nodes[key]
#                b_board[i, j] = TF[index]
#        print(f'b{b}=')
#        print(b_board)
    for l in range(1,num_l+1):
        l_board = np.zeros((h, w),dtype=bool)
        for i in range(h):
            for j in range(w):
                key = f'l{l}_{j}_{i}'
                index = nodes[key]
                l_board[i, j] = TF[index]
        print(f'l{l}=')
        print(l_board)

    
    return A

def generate_sat(Q, WH=None, seed=0):
    nodes = {}
    cnfs = []

    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    w = Q['w']
    h = Q['h']

    if not WH is None:
        w = WH[0]
        h = WH[1]
        Q['w'] = WH[0]
        Q['h'] = WH[1]

    # ラインからブロック番号, 位置を逆引き
    l2b = [[] for _ in range(num_l+1)]
    for b in range(1, num_b+1):
        cells = Q['BLOCK'][b]['cells']
        for dx,dy in cells.keys():
            v = cells[(dx,dy)]
            if v == '+' or v == '0':
                l2b[0].append((b,-dx,-dy))
            else:
                index = int(v)
                l2b[index].append((b,-dx,-dy))


    for b in range(1,num_b+1):
        for i in range(h):
            for j in range(w):
                nodes[f'b{b}_{j}_{i}'] = len(nodes) + 1
    for l in range(1, num_l+1):
        for i in range(h):
            for j in range(w):
                nodes[f'l{l}_{j}_{i}'] = len(nodes) + 1

    # minisatが決定的に動く?ので変数の番号をランダムに割り当て
    keys = list(nodes.keys())
    values = list(nodes.values())
    random.seed(seed)
    np.random.seed(seed)
    random.shuffle(values)
    nodes = dict(zip(keys, values))
    
    # b one-hot
    for b in range(1,num_b+1):
        cnf = {}
        cnfs.append(cnf)
        for i in range(h):
            for j in range(w):
                cnf[f'b{b}_{j}_{i}'] = '1'
        for i in range(h):
            for j in range(w):
                for i2 in range(i, h):
                    for j2 in range(w):
                        if i < i2 or j < j2:
                            cnf = {}
                            cnfs.append(cnf)
                            cnf[f'b{b}_{j}_{i}'] = '-1'
                            cnf[f'b{b}_{j2}_{i2}'] = '-1'

    # line 0 or 1
    for i in range(h):
        for j in range(w):
            for l in range(1, num_l):
                for l2 in range(l+1, num_l+1):
                    cnf = {}
                    cnfs.append(cnf)
                    cnf[f'l{l}_{j}_{i}'] = '-1'
                    cnf[f'l{l2}_{j}_{i}'] = '-1'


    # line孤立禁止
    for i in range(h):
        for j in range(w):
            for l in range(1, num_l+1):
                around = [(1,0),(-1,0),(0,1),(0,-1)]
                cnf = {}
                cnfs.append(cnf)
                cnf[f'l{l}_{j}_{i}'] = '-1'
                for dx,dy in around:
                    if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
                        continue
                    cnf[f'l{l}_{j+dx}_{i+dy}'] = '1'
    # line三叉禁止
    for i in range(h):
        for j in range(w):
            for l in range(1, num_l+1):
                around = [(1,0),(-1,0),(0,1),(0,-1)]
                new_around = []
                for dx,dy in around:
                    if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
                        continue
                    new_around.append((dx,dy))
                if len(new_around) <= 2:
                    continue
                elif len(new_around) <= 3:
                    cnf = {}
                    cnfs.append(cnf)
                    cnf[f'l{l}_{j}_{i}'] = '-1'
                    for dx,dy in new_around:
                        cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
                elif len(new_around) <= 4:
                    for dx,dy in new_around:
                        for dx2,dy2 in new_around:
                            if dx*3+dy >= dx2*3+dy2:
                                continue
                            for dx3,dy3 in new_around:
                                if dx2*3+dy2 >= dx3*3+dy3:
                                    continue
                                cnf = {}
                                cnfs.append(cnf)
                                cnf[f'l{l}_{j}_{i}'] = '-1'
                                cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
                                cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1'
                                cnf[f'l{l}_{j+dx3}_{i+dy3}'] = '-1'

    # blockがはみ出る位置には置けない                
    for i in range(h):
        for j in range(w):
            for b in range(1, num_b+1):
                cells = Q['BLOCK'][b]['cells']
                for dx,dy in cells:
                    if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
                        cnf = {}
                        cnfs.append(cnf)
                        cnf[f'b{b}_{j}_{i}'] = '-1'
                        break

    # block位置に対してライン位置が決定
    for i in range(h):
        for j in range(w):
            for b in range(1, num_b+1):
                cells = Q['BLOCK'][b]['cells']
                flag = False
                for dx,dy in cells:
                    if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
                        break
                    l_str = cells[(dx,dy)]
                    if l_str == '+':
                        for l in range(1,num_l+1):
                            cnf = {}
                            cnfs.append(cnf)
                            cnf[f'b{b}_{j}_{i}'] = '-1'
                            cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
                    elif l_str != '0':
                        for l in range(1,num_l+1):
                            cnf = {}
                            cnfs.append(cnf)
                            cnf[f'b{b}_{j}_{i}'] = '-1'
                            if l == int(l_str):
                                cnf[f'l{l}_{j+dx}_{i+dy}'] = '1'
                            else:
                                cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'                    

    # block同士の衝突禁止
    for b in range(1, num_b+1):
        cells = Q['BLOCK'][b]['cells']
        wb = Q['BLOCK'][b]['w']
        hb = Q['BLOCK'][b]['h']
        for b2 in range(b+1, num_b+1):
            cells2 = Q['BLOCK'][b2]['cells']
            wb2 = Q['BLOCK'][b2]['w']
            hb2 = Q['BLOCK'][b2]['h']
            for i in range(h-hb+1):
                for j in range(w-wb+1):
                    for i2 in range(i-hb2+1,i+hb):
                        if i2 < 0 or i2 >= h:
                            continue
                        for j2 in range(j-wb2+1,j+wb):
                            if j2 < 0 or j2 >= w:
                                continue
                            flag = False
                            for dx,dy in cells.keys():
                                if flag:
                                    break
                                for dx2,dy2 in cells2.keys(): 
                                    if i+dy == i2+dy2 and j+dx == j2+dx2:
                                        if not flag:
                                            flag = True
                                            cnf = {}
                                            cnfs.append(cnf)
                                            cnf[f'b{b}_{j}_{i}'] = '-1'
                                            cnf[f'b{b2}_{j2}_{i2}'] = '-1'
                                            break

    # block上にないlineは周囲2マスに接続
    for i in range(h):
        for j in range(w):
            for l in range(1, num_l+1):
                around = [(1,0),(-1,0),(0,1),(0,-1)]
                new_around = []
                for dx,dy in around:
                    if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
                        continue
                    new_around.append((dx,dy))
                bdxdylist = l2b[l]
                if len(new_around) <= 2:
                    for dx,dy in new_around:
                        cnf = {}
                        cnfs.append(cnf)
                        for b,mdx,mdy in bdxdylist:
                            if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                                continue
                            cnf[f'b{b}_{j+mdx}_{i+mdy}'] = '1'
                        cnf[f'l{l}_{j}_{i}'] = '-1'
                        cnf[f'l{l}_{j+dx}_{i+dy}'] = '1'
                elif len(new_around) <= 3:
                    for dx,dy in new_around:
                        for dx2,dy2 in new_around:
                            if dx*3+dy <= dx2*3+dy2:
                                continue
                            cnf = {}
                            cnfs.append(cnf)
                            for b,mdx,mdy in bdxdylist:
                                if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                                    continue
                                cnf[f'b{b}_{j+mdx}_{i+mdy}'] = '1'
                            cnf[f'l{l}_{j}_{i}'] = '-1'
                            cnf[f'l{l}_{j+dx}_{i+dy}'] = '1'
                            cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '1'

                elif len(new_around) == 4:
                    for dx,dy in new_around:
                        for dx2,dy2 in new_around:
                            if dx*3+dy >= dx2*3+dy2:
                                continue
                            for dx3,dy3 in new_around:
                                if dx2*3+dy2 >= dx3*3+dy3:
                                    continue
                                cnf = {}
                                cnfs.append(cnf)
                                for b,mdx,mdy in bdxdylist:
                                    if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                                        continue
                                    cnf[f'b{b}_{j+mdx}_{i+mdy}'] = '1'
                                cnf[f'l{l}_{j}_{i}'] = '-1'
                                cnf[f'l{l}_{j+dx}_{i+dy}'] = '1'
                                cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '1'
                                cnf[f'l{l}_{j+dx3}_{i+dy3}'] = '1'

    # block上にあるlineは周囲2マスに接続禁止
    for i in range(h):
        for j in range(w):
            for l in range(1, num_l+1):
                around = [(1,0),(-1,0),(0,1),(0,-1)]
                new_around = []
                for dx,dy in around:
                    if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
                        continue
                    new_around.append((dx,dy))
                bdxdylist = l2b[l]
                if len(new_around) <= 2:
                    dx,dy = new_around[0]
                    dx2,dy2 = new_around[1]
                    for b,mdx,mdy in bdxdylist:
                        if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                            continue
                        cnf = {}
                        cnfs.append(cnf)
                        cnf[f'b{b}_{j+mdx}_{i+mdy}'] = '-1'
                        cnf[f'l{l}_{j}_{i}'] = '-1'
                        cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
                        cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1'
                elif len(new_around) <= 3:
                    for dx,dy in new_around:
                        for dx2,dy2 in new_around:
                            if dx*3+dy >= dx2*3+dy2:
                                continue
                            for b,mdx,mdy in bdxdylist:
                                if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                                    continue
                                cnf = {}
                                cnfs.append(cnf)
                                cnf[f'b{b}_{j+mdx}_{i+mdy}'] = '-1'
                                cnf[f'l{l}_{j}_{i}'] = '-1'
                                cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
                                cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1'
                elif len(new_around) == 4:
                    for dx,dy in new_around:
                        for dx2,dy2 in new_around:
                            if dx*3+dy >= dx2*3+dy2:
                                continue
                            for b,mdx,mdy in bdxdylist:
                                if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                                    continue
                                cnf = {}
                                cnfs.append(cnf)
                                cnf[f'b{b}_{j+mdx}_{i+mdy}'] = '-1'
                                cnf[f'l{l}_{j}_{i}'] = '-1'
                                cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
                                cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1'
    return nodes,cnfs
    
    
def _get_around(j, i, w, h, nodes):
    around = []
    if j+1 <= w-1:
        around.append(nodes[f'lh_{j}_{i}'])
    if j-1 >= 0:
        around.append(nodes[f'lh_{j-1}_{i}'])
    if i+1 <= h-1:
        around.append(nodes[f'lv_{j}_{i}'])
    if i-1 >= 0:
        around.append(nodes[f'lv_{j}_{i-1}'])
    return around

def generate_sat2(Q, WH=None, seed=0):
    nodes = {}
    cnfs = []

    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    w = Q['w']
    h = Q['h']

    if not WH is None:
        w = WH[0]
        h = WH[1]
        Q['w'] = WH[0]
        Q['h'] = WH[1]

    # 端点制約に使用
    bdxdylist = []
    for b in range(1, num_b+1):
        cells = Q['BLOCK'][b]['cells']
        for dx,dy in cells.keys():
            v = cells[(dx,dy)]
            if v == '+' or v == '0':
                continue
            else:
                bdxdylist.append((b,-dx,-dy))

    # 変数の作成
    keys = []
    for i, j in itertools.product(range(h),range(w)):
        for b in range(1,num_b+1):
            keys.append(f'b{b}_{j}_{i}')
        for l in range(1,num_l+1):
            keys.append(f'l{l}_{j}_{i}')
        if i != h-1:
            keys.append(f'lv_{j}_{i}')
        if j != w-1:
            keys.append(f'lh_{j}_{i}')

    # minisatが決定的に動く?ので変数の番号をランダムに割り当て
    values = list(range(1, len(keys)+1))
    random.seed(seed)
    np.random.seed(seed)
    random.shuffle(values)
    nodes = dict(zip(keys, values))
    
    # b one-hot
    for b in range(1,num_b+1):
        cnf = []
        cnfs.append(cnf)
        for i, j in itertools.product(range(h),range(w)):
            cnf.append(nodes[f'b{b}_{j}_{i}'])
        for i, j in itertools.product(range(h),range(w)):
            for i2 in range(i, h):
                for j2 in range(w):
                    if i == i2 and j >= j2:
                        continue
                    cnf = []
                    cnfs.append(cnf)
                    cnf.append(-nodes[f'b{b}_{j}_{i}'])
                    cnf.append(-nodes[f'b{b}_{j2}_{i2}'])

    # line 0 or 1
    for i, j in itertools.product(range(h),range(w)):
        for l in range(1, num_l):
            for l2 in range(l+1, num_l+1):
                cnf = []
                cnfs.append(cnf)
                cnf.append(-nodes[f'l{l}_{j}_{i}'])
                cnf.append(-nodes[f'l{l2}_{j}_{i}'])

    # block位置に対してライン位置が決定
    for b in range(1, num_b+1):
        cells = Q['BLOCK'][b]['cells']
        wb = Q['BLOCK'][b]['w']
        hb = Q['BLOCK'][b]['h']
        for i, j in itertools.product(range(h-hb+1),range(w-wb+1)):
            for dx,dy in cells:
                l_str = cells[(dx,dy)]
                if l_str == '+':
                    for l in range(1,num_l+1):
                        cnf = []
                        cnfs.append(cnf)
                        cnf.append(-nodes[f'b{b}_{j}_{i}'])
                        cnf.append(-nodes[f'l{l}_{j+dx}_{i+dy}'])
                elif l_str != '0':
                    cnf = []
                    cnfs.append(cnf)
                    cnf.append(-nodes[f'b{b}_{j}_{i}'])
                    cnf.append(nodes[f'l{int(l_str)}_{j+dx}_{i+dy}'])

    # blockがはみ出る位置には置けない
    for b in range(1, num_b+1):
        cells = Q['BLOCK'][b]['cells']
        wb = Q['BLOCK'][b]['w']
        hb = Q['BLOCK'][b]['h']
        for i, j in itertools.product(range(h),range(w)):
            if i <= h - hb and j <= w - wb:
                continue
            cnf = []
            cnfs.append(cnf)
            cnf.append(-nodes[f'b{b}_{j}_{i}'])

    # block同士の衝突禁止
    for b in range(1, num_b+1):
        cells = Q['BLOCK'][b]['cells']
        wb = Q['BLOCK'][b]['w']
        hb = Q['BLOCK'][b]['h']
        for b2 in range(b+1, num_b+1):
            cells2 = Q['BLOCK'][b2]['cells']
            wb2 = Q['BLOCK'][b2]['w']
            hb2 = Q['BLOCK'][b2]['h']
            for i, j in itertools.product(range(h-hb+1),range(w-wb+1)):
                for i2 in range(i-hb2+1,i+hb):
                    if i2 < 0 or i2 >= h:
                        continue
                    for j2 in range(j-wb2+1,j+wb):
                        if j2 < 0 or j2 >= w:
                            continue
                        flag = False
                        for dx,dy in cells.keys():
                            if flag:
                                break
                            for dx2,dy2 in cells2.keys(): 
                                if i+dy == i2+dy2 and j+dx == j2+dx2:
                                    if not flag:
                                        flag = True
                                        cnf = []
                                        cnfs.append(cnf)
                                        cnf.append(-nodes[f'b{b}_{j}_{i}'])
                                        cnf.append(-nodes[f'b{b2}_{j2}_{i2}'])
                                        break

    # 接続セルの配線は等しい
    for i, j in itertools.product(range(h-1),range(w)):
        for l in range(1, num_l+1):
            cnf = []
            cnfs.append(cnf)
            cnf.append(-nodes[f'lv_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j}_{i}'])
            cnf.append(nodes[f'l{l}_{j}_{i+1}'])
            cnf = []
            cnfs.append(cnf)
            cnf.append(-nodes[f'lv_{j}_{i}'])
            cnf.append(nodes[f'l{l}_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j}_{i+1}'])
    for i, j in itertools.product(range(h),range(w-1)):
        for l in range(1, num_l+1):
            cnf = []
            cnfs.append(cnf)
            cnf.append(-nodes[f'lh_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j}_{i}'])
            cnf.append(nodes[f'l{l}_{j+1}_{i}'])
            cnf = []
            cnfs.append(cnf)
            cnf.append(-nodes[f'lh_{j}_{i}'])
            cnf.append(nodes[f'l{l}_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j+1}_{i}'])

    # 接続していない配線は異なる
    for i, j in itertools.product(range(h-1),range(w)):
        for l in range(1, num_l+1):
            cnf = []
            cnfs.append(cnf)
            cnf.append(nodes[f'lv_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j}_{i+1}'])
    for i, j in itertools.product(range(h),range(w-1)):
        for l in range(1, num_l+1):
            cnf = []
            cnfs.append(cnf)
            cnf.append(nodes[f'lh_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j}_{i}'])
            cnf.append(-nodes[f'l{l}_{j+1}_{i}'])

    # line孤立禁止
    for i, j in itertools.product(range(h),range(w)):
        for l in range(1, num_l+1):
            cnf = []
            cnfs.append(cnf)
            cnf.append(-nodes[f'l{l}_{j}_{i}'])
            around = _get_around(j, i, w, h, nodes)
            cnf.extend(around)

    # line三叉禁止
    for i, j in itertools.product(range(h),range(w)):
        around = _get_around(j, i, w, h, nodes)
        if len(around) == 2:
            continue
        elif len(around) == 3:
            cnf = []
            cnfs.append(cnf)
            cnf.append(-around[0])
            cnf.append(-around[1])
            cnf.append(-around[2])
        elif len(around) == 4:
            for ar in itertools.combinations(around, 3):
                cnf = []
                cnfs.append(cnf)
                cnf.append(-ar[0])
                cnf.append(-ar[1])
                cnf.append(-ar[2])

    # 非端点は周囲2マス以上に接続
    for i, j in itertools.product(range(h),range(w)):
        for l in range(1, num_l+1):
            around = _get_around(j, i, w, h, nodes)
            if len(around) == 2:
                around_itr = itertools.combinations(around, 1)
            elif len(around) == 3:
                around_itr = itertools.combinations(around, 2)
            elif len(around) == 4:
                around_itr = itertools.combinations(around, 3)
            else:
                # assert error
                around_itr = []
            for ar in around_itr:
                cnf = []
                cnfs.append(cnf)
                for b,mdx,mdy in bdxdylist:
                    if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                        continue
                    cnf.append(nodes[f'b{b}_{j+mdx}_{i+mdy}'])
                cnf.append(-nodes[f'l{l}_{j}_{i}'])
                cnf.extend(list(ar))

    # 端点は周囲2マス以上に接続禁止
    for i, j in itertools.product(range(h),range(w)):
            around = _get_around(j, i, w, h, nodes)
            if len(around) == 2:
                around_itr = [around]
            elif len(around) == 3:
                around_itr = itertools.combinations(around, 2)
            elif len(around) == 4:
                around_itr = itertools.combinations(around, 2)
            else:
                # assert error
                around_itr = []
            for ar in around_itr:
                for b,mdx,mdy in bdxdylist:
                    if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
                        continue
                    cnf = []
                    cnfs.append(cnf)
                    cnf.append(-nodes[f'b{b}_{j+mdx}_{i+mdy}'])
                    cnf.append(-ar[0])
                    cnf.append(-ar[1])

    # 配線していないセルには線を接続しない
    for i, j in itertools.product(range(h),range(w)):
        around = _get_around(j, i, w, h, nodes)
        for index in around:
            cnf = []
            cnfs.append(cnf)
            for l in range(1, num_l+1):
                cnf.append(nodes[f'l{l}_{j}_{i}'])
            cnf.append(-index)

    # コの字禁止
    for i, j in itertools.product(range(h-1),range(w-1)):
        cnf = []
        cnfs.append(cnf)
        cnf.append(-nodes[f'lv_{j}_{i}'])
        cnf.append(-nodes[f'lv_{j+1}_{i}'])
        cnf.append(-nodes[f'lh_{j}_{i}'])
        cnf = []
        cnfs.append(cnf)
        cnf.append(-nodes[f'lv_{j}_{i}'])
        cnf.append(-nodes[f'lv_{j+1}_{i}'])
        cnf.append(-nodes[f'lh_{j}_{i+1}'])
        cnf = []
        cnfs.append(cnf)
        cnf.append(-nodes[f'lv_{j}_{i}'])
        cnf.append(-nodes[f'lh_{j}_{i}'])
        cnf.append(-nodes[f'lh_{j}_{i+1}'])
        cnf = []
        cnfs.append(cnf)
        cnf.append(-nodes[f'lv_{j+1}_{i}'])
        cnf.append(-nodes[f'lh_{j}_{i}'])
        cnf.append(-nodes[f'lh_{j}_{i+1}'])

    return nodes,cnfs
    
#############
## 協調動作用
def ensemble_readQ(filename):
    Q = {'BLOCK':{}}
    max_l = 0
    with open(filename, 'r') as file:
        while True:
            str_line = file.readline()
            if not str_line:
                break
            result = split(str_line)
            if result == []:
                continue
            if result[0] == 'SIZE':
                Q['w'] = int(result[1])
                Q['h'] = int(result[2])
            elif result[0] == 'BLOCK_NUM':
                Q['num_b'] = int(result[1])
                Q['n'] = Q['num_b']
            elif result[0] == 'BLOCK':
                index = int(result[1])
                w = int(result[2])
                h = int(result[3])
                if index not in Q['BLOCK']:
                    Q['BLOCK'][index] = []
                cells = {}
                b = {'index':index,'w':w,'h':h,'cells':cells}
                Q['BLOCK'][index].append(b)
                for i in range(h):
                    subline = file.readline()
                    subr = split(subline)
                    for j in range(w):
                        if subr[j] != '0':
                            cells[(j,i)] = subr[j]
                            if subr[j] != '+':
                                num = int(subr[j])
                                if num > max_l:
                                    max_l = num
    Q['num_l'] = max_l
    return Q

def ensemble_generate_sat(Q, WH=None, seed=0):
    nodes = {}
    cnfs = []

    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    w = Q['w']
    h = Q['h']

    if not WH is None:
        w = WH[0]
        h = WH[1]
        Q['w'] = WH[0]
        Q['h'] = WH[1]

    # 変数の作成
    keys = []
    for b in range(1,num_b+1):
        b_list = Q['BLOCK'][b]
        num_bb = len(b_list)
        for bb in range(num_bb): 
        # 0-origin
            for i, j in itertools.product(range(h),range(w)):
                keys.append(f'b{b}-{bb}_{j}_{i}')

    # minisatが決定的に動く?ので変数の番号をランダムに割り当て
    values = list(range(1, len(keys)+1))
    random.seed(seed)
    np.random.seed(seed)
    random.shuffle(values)
    nodes = dict(zip(keys, values))

    # b and bb one-hot
    for b in range(1,num_b+1):
        b_list = Q['BLOCK'][b]
        num_bb = len(b_list)
        b_all = []
        for bb in range(num_bb): 
            for i, j in itertools.product(range(h),range(w)):
                b_all.append(nodes[f'b{b}-{bb}_{j}_{i}'])
        cnf = []
        cnfs.append(cnf)
        cnf.extend(b_all)
        for index,index2 in itertools.combinations(b_all, 2):
            cnf = []
            cnfs.append(cnf)
            cnf.append(-index)
            cnf.append(-index2)

    # blockがはみ出る位置には置けない
    for b in range(1,num_b+1):
        b_list = Q['BLOCK'][b]
        num_bb = len(b_list)
        for bb in range(num_bb): 
            cells = Q['BLOCK'][b][bb]['cells']
            wb = Q['BLOCK'][b][bb]['w']
            hb = Q['BLOCK'][b][bb]['h']
            for i, j in itertools.product(range(h),range(w)):
                if i <= h - hb and j <= w - wb:
                    continue
                cnf = []
                cnfs.append(cnf)
                cnf.append(-nodes[f'b{b}-{bb}_{j}_{i}'])

    # block同士の衝突禁止
    for b,b2 in itertools.combinations(range(1,num_b+1),2):
        b_list = Q['BLOCK'][b]
        num_bb = len(b_list)
        b_list2 = Q['BLOCK'][b2]
        num_bb2 = len(b_list2)
        for bb,bb2 in itertools.product(range(num_bb),range(num_bb2)):
            cells = Q['BLOCK'][b][bb]['cells']
            wb = Q['BLOCK'][b][bb]['w']
            hb = Q['BLOCK'][b][bb]['h']
            cells2 = Q['BLOCK'][b2][bb2]['cells']
            wb2 = Q['BLOCK'][b2][bb2]['w']
            hb2 = Q['BLOCK'][b2][bb2]['h']
            for i, j in itertools.product(range(h-hb+1),range(w-wb+1)):
                for i2,j2 in itertools.product(range(i-hb2+1,i+hb),range(j-wb2+1,j+wb)):
                    if i2 < 0 or i2 >= h or j2 < 0 or j2 >= w:
                        continue
                    flag = False
                    for dx,dy in cells.keys():
                        if flag:
                            break
                        for dx2,dy2 in cells2.keys(): 
                            if i+dy == i2+dy2 and j+dx == j2+dx2:
                                if not flag:
                                    flag = True
                                    cnf = []
                                    cnfs.append(cnf)
                                    cnf.append(-nodes[f'b{b}-{bb}_{j}_{i}'])
                                    cnf.append(-nodes[f'b{b2}-{bb2}_{j2}_{i2}'])
                                    break

    return nodes,cnfs

def ensemble_print_cnf(nodes, cnfs, filename='p.txt'):
    print_cnf2(len(nodes), cnfs, filename=filename)

def ensemble_read_satA(filename, Q, nodes, TF=None):
    with open(filename, 'r') as file:
        str_line = file.readline()
        if str_line.startswith('UNSAT'):
            print('UNSAT')
            return None
        else:
            print('SAT')
        str_line = file.readline()
        ss = str_line.split()
    if TF is None:
        TF = [False] * (len(nodes)+1)
    for num_s in ss:
        num = int(num_s)
        if num>0:
          TF[num] = True
        else:
          TF[-num] = False
    w = Q['w']
    h = Q['h']
    A = {'BLOCK':{}}
    A['w'] = w
    A['h'] = h
    A['map'] = np.zeros((h,w), dtype=int)
    num_b = len(Q['BLOCK'])
    num_l = Q['num_l']
    A['num_b'] = num_b
    A['num_l'] = num_l
    A['n'] = num_b
    for i in range(1, num_b+1):
        A['BLOCK'][i] = {'index':i,'offset':0,'x':0,'y':0}
    for b in range(1,num_b+1):
        b_list = Q['BLOCK'][b]
        num_bb = len(b_list)
        for bb in range(num_bb):
            for i, j in itertools.product(range(h), range(w)):
                key = f'b{b}-{bb}_{j}_{i}'
                if key not in nodes.keys():
                    continue
                index = nodes[key]
                if TF[index]:
                    A['BLOCK'][b]['offset'] = bb
                    A['BLOCK'][b]['x'] = j
                    A['BLOCK'][b]['y'] = i

    ## 最小矩形に更新
    map_b = np.zeros((h, w), dtype=int)
    for b in range(1, num_b+1):
        bb = A['BLOCK'][b]['offset']
        x = A['BLOCK'][b]['x']
        y = A['BLOCK'][b]['y']
        for dx,dy in Q['BLOCK'][b][bb]['cells'].keys():
            map_b[y+dy,x+dx] = b
    i = 0
    while True:
        if i >= h:
            break
        if (map_b[i,:] == 0).all():
            map_b = np.delete(map_b, i, axis=0)
            for b in range(1, num_b+1):
                if A['BLOCK'][b]['y'] > i:
                    A['BLOCK'][b]['y'] -= 1
            h -= 1
            i -= 1
        i += 1
    j = 0
    while True:
        if j >= w:
            break
        if (map_b[:,j] == 0).all():
            map_b = np.delete(map_b, j, axis=1)
            for b in range(1, num_b+1):
                if A['BLOCK'][b]['x'] > j:
                    A['BLOCK'][b]['x'] -= 1
            w -= 1
            j -= 1
        j += 1
    A['map'] = np.zeros((h,w), dtype=int)
    A['h'] = h
    A['w'] = w
    return A

def ensemble_strA(A):
    r = []
    w = A['w']
    h = A['h']
    num_b = A['num_b']
    r.append(f'SIZE {w}X{h}\n')
    for i in range(h):
        r.append(','.join(map(str,A['map'][i])))
        r.append('\n')
    block_list = A['BLOCK']
    for i in range(1, num_b+1):
        bb = block_list[i]['offset']
        x = block_list[i]['x']
        y = block_list[i]['y']
        r.append(f'BLOCK#{i}-{bb} @({x},{y})\n')
    return ''.join(r)


## 協調動作用
#############


def main():
    
    #Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt')
    #Q = readQ('./adc2019problem/Q002_10X10_b8_l9.txt')
    #Q = readQ('./adc2019problem/Q003_10X10_b5_l5.txt')
    #Q = readQ('./adc2019problem/Q004_10X10_b8_l9.txt')
    #Q = readQ('./adc2019problem/Q005_10X10_b7_l6.txt')
    #Q = readQ('./adc2019problem/Q006_10X10_b8_l9.txt')
    #Q = readQ('./adc2019problem/Q007_10X10_b7_l8.txt')
    Q = readQ('./adc2019problem/Q008_10X10_b10_l0.txt')
    #Q = readQ('./adc2019problem/Q009_10X10_b7_l9.txt')
    #Q = readQ('./adc2019problem/Q010_10X10_b20_l24.txt')
    #Q = readQ('./adc2019problem/Q013_10X10_b8_l9.txt')
    #Q = readQ('./adc2019problem/Q014_10X10_b9_l9.txt')
    #Q = readQ('./adc2019problem/Q015_10X10_b8_l9.txt')
    #Q = readQ('./adc2019problem/QRAND327_20X20_b20_l15.txt')
    #Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt')
    #Q = readQ('./adc2019problem/random_problem/QRAND136_30X30_b30_l30.txt')
    #Q = readQ('./Q1.txt')

    mode = 1

    if mode == 1:
        # cell-line variables
        #start_time = time.time() 
        nodes,cnfs = generate_sat(Q, WH=None, seed=0)
        #print(nodes)
        print_cnf(nodes, cnfs)
        os.system('minisat p.txt a.txt')
        A = read_satA('a.txt', Q, nodes)
        if A is None:
            return
        print(strA(A))
        #debug_satA2('a.txt', Q, nodes)
        #end_time= time.time()
        #print(f"経過時間：{end_time - start_time}")
        #img = QA2img(Q,A)
        #plt.imshow(img)
    elif mode == 2:
        # line variables
        nodes,cnfs = generate_sat2(Q, WH=None, seed=0)
        print_cnf2(nodes, cnfs)
        os.system('minisat p.txt a.txt')
        A = read_satA2('a.txt', Q, nodes)
        if A is None:
            return
        print(strA(A))
    elif mode == 3:
        # ensemble
        Q = ensemble_readQ('./qq.txt')
        nodes,cnfs = ensemble_generate_sat(Q, WH=None, seed=0)
        ensemble_print_cnf(nodes, cnfs)
        os.system('minisat p.txt a.txt')
        A = ensemble_read_satA('a.txt', Q, nodes)
        print(ensemble_strA(A))

if __name__ == '__main__':
    main()