backend/Sat_cnt.txt

# Solve the puzzle
if s.check() == sat:
    m = s.model()
    rows = []
    header = ["House"] + [cat_name for cat_name, _ in categories]
    for position in range(1, NUM_POSITIONS + 1):
        row = [str(position)]
        for cat_idx, (cat_name, item_list) in enumerate(categories):
            for item_idx, item_str in enumerate(item_list):
                if m.evaluate(Vars[cat_idx][item_idx]).as_long() == position:
                    row.append(item_str)
                    break
        rows.append(row)
    result_dict = {"header": header, "rows": rows}

    cnt = 1
    block = []
    for cat_idx, (cat_name, item_list) in enumerate(categories):
        for i in range(NUM_POSITIONS):
            block.append(Vars[cat_idx][i] != m[Vars[cat_idx][i]])
    s.add(Or(block))
    while s.check() == sat:
        m = s.model()
        cnt += 1
        block = []
        for cat_idx, (cat_name, item_list) in enumerate(categories):
            for i in range(NUM_POSITIONS):
                block.append(Vars[cat_idx][i] != m[Vars[cat_idx][i]])
        s.add(Or(block))
    print(f"sat:{cnt}")
else:
    print(f"error")