#include "vision.h" #include <bits/stdc++.h> using namespace std; void construct_network(int H, int W, int K) { int qidx = H * W; vector<int> base(100); vector<int> Ns; base[1] = H * W; // 1: FALSE | TRUE add_xor({0, 0}), qidx++; add_not(qidx - 1), qidx++; // ---------- base[10] = qidx; // 10: row[i] >= 1 for (int i = 0; i < H; i++) { Ns.clear(); for (int j = 0; j < W; j++) { Ns.push_back(i * W + j); } add_or(Ns), qidx++; } base[11] = qidx; // 11: row[i] == 0 for (int i = 0; i < H; i++) { add_not(base[10] + i), qidx++; } base[12] = qidx; // 12: count(row[i]) == 1 for (int i = 0; i < H; i++) { Ns.clear(); for (int j = 0; j < W; j++) { Ns.push_back(i * W + j); } add_xor(Ns), qidx++; } base[13] = qidx; // 13: count(row[i]) == 2 for (int i = 0; i < H; i++) { add_xor({base[10] + i, base[12] + i}), qidx++; } base[14] = qidx; // 14: count(row[i]) >= 1 AND count(row[i+d]) >= 1 (d=[1,H/2)) for (int d = 1; d < H / 2; d++) { for (int i = 0; i + d < H; i++) { add_and({base[10] + i, base[10] + i + d}), qidx++; } } base[15] = qidx; // X int lb = 0, rb = H - 1 - (H % 2 == 0); while (lb < rb) { Ns.clear(); for (int i = 0; i <= lb; i++) { Ns.push_back(base[10] + i); } add_or(Ns), qidx++; Ns.clear(); for (int i = rb; i < H; i++) { Ns.push_back(base[11] + i); } add_and(Ns), qidx++; add_and({qidx - 1, qidx - 2}), qidx++; lb++, rb--; } base[16] = qidx; // 16: pre[0] + ... + pre[l] >= 1 AND pre[r] + ... + pre[H-1] == 0 for (int i = 0, idx = base[15] + 2; idx < base[16]; i++, idx += 3) { add_and({idx}), qidx++; } base[17] = qidx; // X lb = 0, rb = H - 1 - (H % 2 == 0); while (lb < rb) { Ns.clear(); for (int i = 0; i <= lb; i++) { Ns.push_back(base[11] + i); } add_and(Ns), qidx++; Ns.clear(); for (int i = rb; i < H; i++) { Ns.push_back(base[10] + i); } add_or(Ns), qidx++; add_and({qidx - 1, qidx - 2}), qidx++; lb++, rb--; } base[18] = qidx; // 18: pre[0] + ... + pre[l] == 0 AND pre[r] + ... + pre[H-1] >= 1 for (int i = 0, idx = base[17] + 2; idx < base[18]; i++, idx += 3) { add_and({idx}), qidx++; } base[30] = qidx; // 30: diff of row <= d (-1~H) add_and({base[1]}), qidx++; // -1 (FALSE) Ns.clear(); // 0 for (int i = 0; i < H; i++) { Ns.push_back(base[13] + i); } add_or(Ns), qidx++; for (int d = 1; d < H / 2; d++) { // 1 ~ H/2-1 Ns.clear(); for (int i = 0; i + d < H; i++) { Ns.push_back(base[14] + i); } add_or(Ns), qidx++; } for (int d = H / 2, idx = 0; d <= H - 2; d++, idx++) { // H/2 ~ H-2 Ns.clear(); for (int i = d; i < H - d; i++) { Ns.push_back(base[10] + i); } Ns.push_back(base[16] + (d - H / 2)); Ns.push_back(base[18] + (d - H / 2)); add_or(Ns), qidx++; } add_and({base[1] + 1}), qidx++; // H-1 (TRUE) // ---------- base[40] = qidx; // 40: col[j] >= 1 for (int j = 0; j < W; j++) { Ns.clear(); for (int i = 0; i < H; i++) { Ns.push_back(i * W + j); } add_or(Ns), qidx++; } base[41] = qidx; // 41: col[j] == 0 for (int j = 0; j < W; j++) { add_not(base[40] + j), qidx++; } base[42] = qidx; // 42: count(col[j]) == 1 for (int j = 0; j < W; j++) { Ns.clear(); for (int i = 0; i < H; i++) { Ns.push_back(i * W + j); } add_xor(Ns), qidx++; } base[43] = qidx; // 43: count(col[j]) == 2 for (int j = 0; j < W; j++) { add_xor({base[40] + j, base[42] + j}), qidx++; } base[44] = qidx; // 44: count(col[j]) >= 1 AND count(col[j+d]) >= 1 (d=[1,W/2)) for (int d = 1; d < W / 2; d++) { for (int j = 0; j + d < W; j++) { add_and({base[40] + j, base[40] + j + d}), qidx++; } } base[45] = qidx; // X lb = 0, rb = W - 1 - (W % 2 == 0); while (lb < rb) { Ns.clear(); for (int j = 0; j <= lb; j++) { Ns.push_back(base[40] + j); } add_or(Ns), qidx++; Ns.clear(); for (int j = rb; j < W; j++) { Ns.push_back(base[41] + j); } add_and(Ns), qidx++; add_and({qidx - 1, qidx - 2}), qidx++; lb++, rb--; } base[46] = qidx; // 46: pre[0] + ... + pre[l] >= 1 AND pre[r] + ... + pre[W-1] == 0 for (int j = 0, idx = base[45] + 2; idx < base[46]; j++, idx += 3) { add_and({idx}), qidx++; } base[47] = qidx; // X lb = 0, rb = W - 1 - (W % 2 == 0); while (lb < rb) { Ns.clear(); for (int j = 0; j <= lb; j++) { Ns.push_back(base[41] + j); } add_and(Ns), qidx++; Ns.clear(); for (int j = rb; j < W; j++) { Ns.push_back(base[40] + j); } add_or(Ns), qidx++; add_and({qidx - 1, qidx - 2}), qidx++; lb++, rb--; } base[48] = qidx; // 48: pre[0] + ... + pre[l] == 0 AND pre[r] + ... + pre[W-1] >= 1 for (int j = 0, idx = base[47] + 2; idx < base[48]; j++, idx += 3) { add_and({idx}), qidx++; } base[60] = qidx; // 60: diff of row <= d (-1~W) add_and({base[1]}), qidx++; // -1 (FALSE) Ns.clear(); // 0 for (int j = 0; j < W; j++) { Ns.push_back(base[43] + j); } add_or(Ns), qidx++; for (int d = 1; d < W / 2; d++) { // 1 ~ W/2-1 Ns.clear(); for (int j = 0; j + d < W; j++) { Ns.push_back(base[44] + j); } add_or(Ns), qidx++; } for (int d = W / 2, idx = 0; d <= W - 2; d++, idx++) { // W/2 ~ W-2 Ns.clear(); for (int j = d; j < W - d; j++) { Ns.push_back(base[40] + j); } Ns.push_back(base[46] + (d - W / 2)); Ns.push_back(base[48] + (d - W / 2)); add_or(Ns), qidx++; } add_and({base[1] + 1}), qidx++; // W-1 (TRUE) // ---------- base[80] = qidx; // get row positions for (int i = 0; i < H; i++) { add_xor({base[30] + i, base[30] + i + 1}), qidx++; } base[81] = qidx; // get col positions for (int j = 0; j < W; j++) { add_xor({base[60] + j, base[60] + j + 1}), qidx++; } base[82] = qidx; for (int i = 0; i < H; i++) { int j = K - i; if (j >= 0 && j < W) { add_and({base[80] + i, base[81] + j}), qidx++; } } base[83] = qidx; Ns.clear(); for (int x = base[82]; x < base[83]; x++) { Ns.push_back({x}); } add_or(Ns), qidx++; }