<jupyter_start><jupyter_text>Read instance file:<jupyter_code>input_filename = '../../Instances/20x20.txt'

w, h, n, DX, DY = None, None, None, None, None

with open(input_filename, 'r') as f_in:
    lines = f_in.read().splitlines()

    split = lines[0].split(' ')
    w = int(split[0])
    h = int(split[1])

    n = int(lines[1])

    DX = []
    DY = []

    for i in range(int(n)):
        split = lines[i + 2].split(' ')
        DX.append(int(split[0]))
        DY.append(int(split[1]))<jupyter_output><empty_output><jupyter_text>Solver:<jupyter_code>solver = Solver()<jupyter_output><empty_output><jupyter_text>Model:<jupyter_code>B = [[[Bool(f'B_{i}_{j}_{k}') for k in range(n)] for j in range(w)] for i in range(h)]
def at_least_one(bool_vars: Sequence):
    return Or(bool_vars)

def at_most_one(bool_vars: Sequence):
    return [Not(And(pair[0], pair[1])) for pair in combinations(bool_vars, 2)]
# Constraint "at most one piece"
for i in range(h):
    for j in range(w):
        solver.add(at_most_one(B[i][j]))
# Iterate over all the pieces p
for p in tqdm(range(n), leave=False):
    dx = DX[p]
    dy = DY[p]
    
    package_clauses = []
    
    # Iterate over all the coordinates where p can fit
    for i in range(h - dy + 1):
        for j in range(w - dx + 1):
            
            patch_clauses = []
            # Iterate over the cells of p's patch
            for f1 in range(dy):
                for f2 in range(dx):
                    patch_clauses.append(B[i + f1][j + f2][p])
            
            package_clauses.append(And(patch_clauses))
    
    # Exactly one
    solver.add(at_least_one(package_clauses))
    # solver.add(at_most_one(package_clauses))
Sr = [[Bool(f'C_row_{i}_{j}') for j in range(w)] for i in range(w - 1)]
Sc = [[Bool(f'C_col_{i}_{j}') for j in range(h)] for i in range(h - 1)]
# Implied constraint for rows
for r in tqdm(range(h), leave=False):
    solver.add(Or(Not(at_least_one(B[r][0])), Sr[0][0]))  # SC1
    for j in range(1, w):
        solver.add(Not(Sr[0][j]))  # SC2
    for i in range(1, w - 1):
        solver.add(Or(Not(at_least_one(B[r][i])), Sr[i][0]))  # SC3
        solver.add(Or(Not(Sr[i - 1][0]), Sr[i][0]))  # SC4
        for j in range(1, w):
            solver.add(Or(Not(at_least_one(B[r][i])), Not(Sr[i - 1][j - 1]), Sr[i][j]))  # SC5
            solver.add(Or(Not(Sr[i - 1][j]), Sr[i][j]))  # SC6
        solver.add(Or(Not(at_least_one(B[r][i])), Not(Sr[i - 1][w - 1])))  # SC7
    solver.add(Or(Not(at_least_one(B[r][w - 1])), Not(Sr[w - 2][w - 1])))  # SC8

# Implied constraint for columns
for c in tqdm(range(w), leave=False):
    solver.add(Or(Not(at_least_one(B[0][c])), Sc[0][0]))  # SC1
    for j in range(1, h):
        solver.add(Not(Sc[0][j]))  # SC2
    for i in range(1, h - 1):
        solver.add(Or(Not(at_least_one(B[i][c])), Sc[i][0]))  # SC3
        solver.add(Or(Not(Sr[i - 1][0]), Sc[i][0]))  # SC4
        for j in range(1, h):
            solver.add(Or(Not(at_least_one(B[i][c])), Not(Sc[i - 1][j - 1]), Sc[i][j]))  # SC5
            solver.add(Or(Not(Sc[i - 1][j]), Sc[i][j]))  # SC6
        solver.add(Or(Not(at_least_one(B[i][c])), Not(Sc[i - 1][h - 1])))  # SC7
    solver.add(Or(Not(at_least_one(B[h - 1][c])), Not(Sc[h - 2][h - 1])))  # SC8
%%time
solver.check()<jupyter_output>CPU times: user 4.96 s, sys: 23.1 ms, total: 4.99 s
Wall time: 4.99 s<jupyter_text>From Z3 model solution to file:<jupyter_code>solution = np.zeros((h, w, n), dtype=bool)
model = solver.model()

for i in range(h):
    for j in range(w):
        for k in range(n):
            solution[i, j, k] = is_true(model[B[i][j][k]])
xy = {}
for p in range(n):
    y_ids, x_ids = solution[:, :, p].nonzero()
    #print(solution[:, :, p])
    x = np.min(x_ids)
    y = h-1-np.max(y_ids)
    xy[p] = [x, y]
xy
output_filename = '../../pwp_utilities/20x20_sol.txt'
with open(output_filename, 'w') as f_out:
    f_out.write('{} {}\n'.format(w, h))
    f_out.write('{}\n'.format(n))
    for i in range(n):
        f_out.write('{} {}\t{} {}\n'.format(DX[i], DY[i], xy[i][0], xy[i][1]))<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.20308294592610718, 'fraction_numerical': 0.02397846831416687, 'mean_word_length': 2.95357833655706, 'pattern_counts': {'":': 0, '<': 16, '<?xml version=': 0, '>': 16, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '4', 'dir': 'jupyter-structured-clean-dedup', 'id': '68529', 'license': 'MIT', 'n_tokens_mistral': 1804, 'n_tokens_neox': 1730, 'n_words': 366, 'path': 'SAT/src/pwp-final.ipynb', 'repo_name': 'Lostefra/Present_Wrapping_Problem', 'size': '4087'}