#include "vision.h"
#include <bits/stdc++.h>

using namespace std;
using ll = long long;

template <class T> using Vec = std::vector<T>;
#define L(i, l, r) for (int i = (l); i < (r); ++i)
#define R(i, l, r) for (int i = (r - 1); i >= (l); --i)
#define ALL(x) (x).begin(), (x).end()
#define sz(x) (int)(x.size())

int startH, endH, startW, endW;
int zeroP, oneP;

int nwId;

pair<int, int> process(int inStartPos, int inEndPos) {
	const int n = inEndPos - inStartPos;
	const int B = sqrt(n);
	Vec<pair<int, int>> blocks;
	for (int l = 0; l < n; l += B) {
		blocks.push_back({l, min(l + B, n)});
	}
	int nBlock = sz(blocks);
	int isSame = nwId++;
	{
		Vec<int> ns;
		L(i, 0, n) ns.push_back(inStartPos + i);
		add_xor(ns);
	}
	add_not(isSame); int isNotSame = nwId++;

	Vec<int> mns, mxs;
	{
		add_not(zeroP); ++nwId;
		Vec<int> ns;
		L(i, 0, n) {
			add_and({inStartPos + i, nwId - 1});
			add_xor({nwId - 1, inStartPos + i});
			mns.push_back(nwId);
			nwId += 2;
		}
		add_not(oneP); ++nwId;
		L(i, 0, n) {
			add_and({inStartPos + i, nwId - 1});
			add_xor({nwId - 1, inStartPos + i});
			mxs.push_back(nwId);
			nwId += 2;
		}
	}

	int isNotSameBlock = -1;
	{
		int s = nwId;
		for (auto &[l, r] : blocks) {
			Vec<int> ns;
			L(i, l, r) ns.push_back(inStartPos + i);
			add_xor(ns); ++nwId;
		}
		Vec<int> ns;
		L(i, s, nwId) ns.push_back(i);
		add_or(ns); isNotSameBlock = nwId++;
	}
	add_not(isNotSameBlock); int isSameBlock = nwId++;

	// 同じブロックな場合の距離テーブル
	int startSameBlockDisTablePos = -1, endSameBlockDisTablePos = -1;
	{
		Vec<int> ps;
		L(i, 0, B) L(j, i + 1, B) {
			Vec<int> ns;
			L(k, 0, nBlock) {
				if (blocks[k].first + j >= blocks[k].second) continue;
				ns.push_back(inStartPos + blocks[k].first + i);
				ns.push_back(inStartPos + blocks[k].first + j);
			}
			add_or(ns);ns.push_back(oneP);add_xor(ns);
			add_and({nwId, nwId + 1}); nwId += 3; ps.push_back(nwId - 1);
		}
		startSameBlockDisTablePos = nwId;
		L(dis, 0, B) {
			Vec<int> ns;
			int cnt = 0;
			L(i, 0, B) L(j, i + 1, B) {
				if (j - i == 0) ns.push_back(ps[cnt]);
				++cnt;
			}
			ns.push_back(zeroP);
			add_or(ns); ++nwId;
		}
		endSameBlockDisTablePos = nwId;
	}

	int startDifBlockDisTablePos = -1, endDifBlockDisTablePos = -1;
	{
		Vec<int> ps;
		L(i, 0, B) L(j, 0, B) {
			Vec<int> ns;
			L(k, 0, nBlock) {
				if (blocks[k].first + j >= blocks[k].second) continue;
				ns.push_back(mns[blocks[k].first + i]);
				ns.push_back(mxs[blocks[k].first + j]);
			}
			add_or(ns);ns.push_back(oneP);add_xor(ns);
			add_and({nwId, nwId + 1}); nwId += 3; ps.push_back(nwId - 1);
		}
		startDifBlockDisTablePos = nwId;
		L(dis, 0, 2 * B) {
			Vec<int> ns;
			int cnt = 0;
			L(i, 0, B) L(j, 0, B) {
				if (j + (B - i) == dis) ns.push_back(ps[cnt]);
				++cnt;
			}
			ns.push_back(zeroP);
			add_or(ns); ++nwId;
		}
		endDifBlockDisTablePos = nwId;
	}

	int startBtDifBlockPos = -1, endBtDifBlockPos = -1;
	{
		Vec<int> ps;
		L(i, 0, nBlock) L(j, i + 1, nBlock) {
			Vec<int> ns;
			L(k, blocks[i].first, blocks[i].second) ns.push_back(inStartPos + k);
			ns.push_back(zeroP); add_or(ns); ++nwId;
			ns.clear();
			L(k, blocks[j].first, blocks[j].second) ns.push_back(inStartPos + k);
			ns.push_back(zeroP); add_or(ns); ++nwId;
			add_and({nwId - 2, nwId - 1}); ps.push_back(nwId++);
		}
		startBtDifBlockPos = nwId;
		L(dis, 0, nBlock) {
			Vec<int> ns;
			int cnt = 0;
			L(i, 0, nBlock) L(j, i + 1, nBlock) {
				if (j - i == dis) ns.push_back(ps[cnt]);
				++cnt;
			}
			ns.push_back(zeroP);
			add_or(ns); ++nwId;
		}
		endBtDifBlockPos = nwId;
	}

	// 違うブロックの場合の距離テーブル
	Vec<int> difBlockTable;
	{
		L(dis, 0, n) {
			Vec<int> ps;
			L(i, 0, 2 * B) L(j, 0, nBlock) {
				if (i + (j - 1) * B == dis) {
					add_and({startDifBlockDisTablePos + i, startBtDifBlockPos + j});
					ps.push_back(nwId++);
				}
			}
			ps.push_back(zeroP);
			add_or(ps);
			difBlockTable.push_back(nwId++);
		}
	}

	// 集計
	int aStart = nwId;
	L(i, 0, n) {
		add_and({isNotSame, isSameBlock, (i >= B ? zeroP : startSameBlockDisTablePos + i)});
		++nwId;
	}
	int bStart = nwId;
	L(i, 0, n) {
		add_and({isNotSame, isNotSameBlock, difBlockTable[i]});
		++nwId;
	}
	int retL = nwId;
	add_not(isNotSame); ++nwId;
	L(i, 1, n) {
		add_or({aStart + i, bStart + i}); ++nwId;
	}
	int retR = nwId;
	return {retL, retR};
}

void construct_network(int H, int W, int K) {
	nwId = H * W;
	add_not(0); ++nwId;
	add_and({0, nwId - 1}); zeroP = nwId++;
	add_or({0, nwId - 2}); oneP = nwId++;
	startH = nwId;
	endH = nwId + H;
	nwId += H;
	L(i, 0, H) {
		Vec<int> ns;
		L(j, 0, W) ns.push_back(i * W + j);
		add_or(ns);
	}
	startW = nwId;
	endW = nwId + W;
	nwId += W;
	L(j, 0, W) {
		Vec<int> ns;
		L(i, 0, H) ns.push_back(i * W + j);
		add_or(ns);
	}

	auto [al, ar] = process(startH, endH);
	auto [bl, br] = process(startW, endW);
	int lsStart = nwId;
	Vec<int> ns;
	L(i, 0, H) L(j, 0, W) {
		if (i + j == K) {
			add_and({al + i, bl + j}); ++nwId;
		}
	}
	L(i, lsStart, nwId) ns.push_back(i);
	add_or(ns);
	// ans !
}