|
#include <algorithm> |
|
#include <array> |
|
#include <atomic> |
|
#include <chrono> |
|
#include <cstdint> |
|
#include <iostream> |
|
#include <mutex> |
|
#include <set> |
|
#include <string> |
|
#include <thread> |
|
#include <vector> |
|
|
|
using Perm = std::array<int, 32>; |
|
static constexpr int N = 32; |
|
static constexpr Perm seed = { |
|
0, 1, 28, 20, 27, 17, 18, 21, 30, 26, 14, 9, 25, 11, 31, 29, |
|
23, 5, 13, 6, 16, 15, 12, 3, 7, 19, 24, 8, 22, 2, 4, 10, |
|
}; |
|
|
|
struct Task { uint32_t mask; int next; }; |
|
struct Counts { |
|
uint64_t subsets = 0, persistent = 0, empty_domain = 0; |
|
uint64_t matching_fail = 0, matching_pass = 0, dfs_nodes = 0; |
|
uint64_t dynamic_matching_fail = 0; |
|
}; |
|
|
|
static std::array<std::array<std::vector<uint32_t>, N>, N> blockers; |
|
static std::vector<Task> tasks; |
|
static std::atomic<size_t> next_task{0}; |
|
static std::atomic<bool> stop{false}; |
|
static std::chrono::steady_clock::time_point started; |
|
static double seconds_limit = 0.0; |
|
static bool use_dynamic_matching = false; |
|
static Perm witness{}; |
|
static std::mutex witness_mutex; |
|
|
|
static std::pair<int, int> vector_of(int x1, int y1, int x2, int y2) { |
|
if (x1 < x2) return {x2 - x1, y2 - y1}; |
|
return {x1 - x2, y1 - y2}; |
|
} |
|
|
|
static void build_blockers() { |
|
uint64_t total = 0, triples = 0, quads = 0; |
|
for (int pos = 0; pos < N; ++pos) for (int source = 0; source < N; ++source) { |
|
if (pos == source) continue; |
|
std::set<uint32_t> raw; |
|
std::vector<std::pair<std::pair<int, int>, int>> incident; |
|
for (int other = 0; other < N; ++other) { |
|
if (other == pos || other == source) continue; |
|
incident.push_back({vector_of(pos, seed[source], other, seed[other]), other}); |
|
} |
|
for (size_t a = 0; a < incident.size(); ++a) |
|
for (size_t b = a + 1; b < incident.size(); ++b) |
|
if (incident[a].first == incident[b].first) |
|
raw.insert((1u << incident[a].second) | |
|
(1u << incident[b].second)); |
|
for (const auto& [candidate_vector, other] : incident) { |
|
for (int left = 0; left < N; ++left) { |
|
if (left == pos || left == source) continue; |
|
for (int right = left + 1; right < N; ++right) { |
|
if (right == pos || right == source) continue; |
|
if (candidate_vector == vector_of(left, seed[left], right, seed[right])) |
|
raw.insert((1u << other) | (1u << left) | (1u << right)); |
|
} |
|
} |
|
} |
|
for (uint32_t mask : raw) { |
|
bool minimal = true; |
|
for (uint32_t other : raw) |
|
if (other != mask && (other & mask) == other) { minimal = false; break; } |
|
if (minimal) blockers[pos][source].push_back(mask); |
|
} |
|
total += blockers[pos][source].size(); |
|
for (uint32_t mask : blockers[pos][source]) { |
|
const int length = 1 + __builtin_popcount(mask); |
|
triples += length == 3; |
|
quads += length == 4; |
|
} |
|
} |
|
if (total != 6578 || triples != 372 || quads != 6206) { |
|
std::cerr << "blocker self-test failed total=" << total |
|
<< " ternary=" << triples << " quaternary=" << quads << '\n'; |
|
std::exit(3); |
|
} |
|
} |
|
|
|
static uint32_t domain(int pos, uint32_t changed) { |
|
uint32_t result = 0; |
|
uint32_t sources = changed & ~(1u << pos); |
|
while (sources) { |
|
const int source = __builtin_ctz(sources); |
|
sources &= sources - 1; |
|
bool allowed = true; |
|
for (uint32_t blocker : blockers[pos][source]) |
|
if (!(blocker & changed)) { allowed = false; break; } |
|
if (allowed) result |= 1u << source; |
|
} |
|
return result; |
|
} |
|
|
|
static bool matching_rec(uint32_t positions, uint32_t used, |
|
const std::array<uint32_t, N>& domains) { |
|
if (!positions) return true; |
|
int chosen = -1, best = N + 1; |
|
for (uint32_t scan = positions; scan; scan &= scan - 1) { |
|
int pos = __builtin_ctz(scan); |
|
int count = __builtin_popcount(domains[pos] & ~used); |
|
if (!count) return false; |
|
if (count < best) { best = count; chosen = pos; } |
|
} |
|
uint32_t available = domains[chosen] & ~used; |
|
while (available) { |
|
uint32_t bit = available & -available; |
|
available -= bit; |
|
if (matching_rec(positions & ~(1u << chosen), used | bit, domains)) |
|
return true; |
|
} |
|
return false; |
|
} |
|
|
|
struct SearchState { |
|
Perm values; |
|
uint32_t assigned = 0, used_sources = 0; |
|
std::array<uint64_t, N> seen{}; |
|
}; |
|
|
|
static bool compatible(const SearchState& state, int pos, int source) { |
|
std::array<uint64_t, N> local{}; |
|
for (uint32_t scan = state.assigned; scan; scan &= scan - 1) { |
|
int other = __builtin_ctz(scan); |
|
auto [lag, difference] = vector_of(pos, seed[source], other, state.values[other]); |
|
uint64_t bit = 1ull << (difference + 31); |
|
if ((state.seen[lag] | local[lag]) & bit) return false; |
|
local[lag] |= bit; |
|
} |
|
return true; |
|
} |
|
|
|
static void set_point(SearchState& state, int pos, int source, bool add) { |
|
if (add) { |
|
for (uint32_t scan = state.assigned; scan; scan &= scan - 1) { |
|
int other = __builtin_ctz(scan); |
|
auto [lag, difference] = vector_of(pos, seed[source], other, state.values[other]); |
|
state.seen[lag] |= 1ull << (difference + 31); |
|
} |
|
state.values[pos] = seed[source]; |
|
state.assigned |= 1u << pos; |
|
state.used_sources |= 1u << source; |
|
} else { |
|
state.assigned &= ~(1u << pos); |
|
state.used_sources &= ~(1u << source); |
|
for (uint32_t scan = state.assigned; scan; scan &= scan - 1) { |
|
int other = __builtin_ctz(scan); |
|
auto [lag, difference] = vector_of(pos, seed[source], other, state.values[other]); |
|
state.seen[lag] &= ~(1ull << (difference + 31)); |
|
} |
|
state.values[pos] = -1; |
|
} |
|
} |
|
|
|
static bool solve_moves(uint32_t remaining, const std::array<uint32_t, N>& domains, |
|
SearchState& state, Counts& counts) { |
|
++counts.dfs_nodes; |
|
if (!remaining) { |
|
std::lock_guard<std::mutex> lock(witness_mutex); |
|
witness = state.values; |
|
stop.store(true); |
|
return true; |
|
} |
|
int chosen = -1, best = N + 1; |
|
uint32_t chosen_sources = 0; |
|
std::array<uint32_t, N> viable_domains{}; |
|
for (uint32_t scan = remaining; scan; scan &= scan - 1) { |
|
int pos = __builtin_ctz(scan), count = 0; |
|
uint32_t viable = 0, sources = domains[pos] & ~state.used_sources; |
|
while (sources) { |
|
uint32_t bit = sources & -sources; |
|
sources -= bit; |
|
int source = __builtin_ctz(bit); |
|
if (compatible(state, pos, source)) { viable |= bit; ++count; } |
|
} |
|
viable_domains[pos] = viable; |
|
if (!count) return false; |
|
if (count < best) { best = count; chosen = pos; chosen_sources = viable; } |
|
} |
|
if (use_dynamic_matching && |
|
!matching_rec(remaining, state.used_sources, viable_domains)) { |
|
++counts.dynamic_matching_fail; |
|
return false; |
|
} |
|
while (chosen_sources && !stop.load()) { |
|
uint32_t bit = chosen_sources & -chosen_sources; |
|
chosen_sources -= bit; |
|
int source = __builtin_ctz(bit); |
|
set_point(state, chosen, source, true); |
|
if (solve_moves(remaining & ~(1u << chosen), domains, state, counts)) return true; |
|
set_point(state, chosen, source, false); |
|
} |
|
return false; |
|
} |
|
|
|
static void check_subset(uint32_t changed, Counts& counts) { |
|
++counts.subsets; |
|
constexpr uint32_t core = (1u << 0) | (1u << 1) | (1u << 5) | (1u << 6); |
|
if (!(changed & core)) { ++counts.persistent; return; } |
|
std::array<uint32_t, N> domains{}; |
|
for (uint32_t scan = changed; scan; scan &= scan - 1) { |
|
int pos = __builtin_ctz(scan); |
|
domains[pos] = domain(pos, changed); |
|
if (!domains[pos]) { ++counts.empty_domain; return; } |
|
} |
|
if (!matching_rec(changed, 0, domains)) { ++counts.matching_fail; return; } |
|
++counts.matching_pass; |
|
SearchState state; |
|
state.values.fill(-1); |
|
uint32_t fixed = ~changed; |
|
for (int pos = 0; pos < N; ++pos) if (fixed >> pos & 1u) { |
|
if (!compatible(state, pos, pos)) std::exit(4); |
|
set_point(state, pos, pos, true); |
|
} |
|
solve_moves(changed, domains, state, counts); |
|
} |
|
|
|
static void choose_rest(int next, int left, uint32_t mask, Counts& counts) { |
|
if (stop.load()) return; |
|
if (!left) { |
|
check_subset(mask, counts); |
|
if ((counts.subsets & 4095u) == 0 && seconds_limit > 0.0) { |
|
double elapsed = std::chrono::duration<double>( |
|
std::chrono::steady_clock::now() - started).count(); |
|
if (elapsed >= seconds_limit) stop.store(true); |
|
} |
|
return; |
|
} |
|
for (int pos = next; pos <= N - left && !stop.load(); ++pos) |
|
choose_rest(pos + 1, left - 1, mask | (1u << pos), counts); |
|
} |
|
|
|
static void worker(int radius, Counts& counts) { |
|
while (!stop.load()) { |
|
size_t index = next_task.fetch_add(1); |
|
if (index >= tasks.size()) return; |
|
const Task task = tasks[index]; |
|
choose_rest(task.next, radius - 4, task.mask, counts); |
|
} |
|
} |
|
|
|
static uint64_t choose(int n, int k) { |
|
uint64_t result = 1; |
|
for (int i = 1; i <= k; ++i) result = result * (n - k + i) / i; |
|
return result; |
|
} |
|
|
|
int main(int argc, char** argv) { |
|
int radius = argc > 1 ? std::stoi(argv[1]) : 12; |
|
int workers = argc > 2 ? std::stoi(argv[2]) : 8; |
|
seconds_limit = argc > 3 ? std::stod(argv[3]) : 0.0; |
|
use_dynamic_matching = argc > 4 && std::string(argv[4]) == "hall"; |
|
if (radius < 4 || radius > N) return 2; |
|
witness.fill(-1); |
|
build_blockers(); |
|
for (int a = 0; a <= N - radius; ++a) |
|
for (int b = a + 1; b <= N - radius + 1; ++b) |
|
for (int c = b + 1; c <= N - radius + 2; ++c) |
|
for (int d = c + 1; d <= N - radius + 3; ++d) |
|
tasks.push_back({(1u << a) | (1u << b) | (1u << c) | (1u << d), d + 1}); |
|
started = std::chrono::steady_clock::now(); |
|
std::vector<Counts> per_worker(workers); |
|
std::vector<std::thread> threads; |
|
for (int i = 0; i < workers; ++i) threads.emplace_back(worker, radius, std::ref(per_worker[i])); |
|
for (auto& thread : threads) thread.join(); |
|
Counts total; |
|
for (const Counts& item : per_worker) { |
|
total.subsets += item.subsets; total.persistent += item.persistent; |
|
total.empty_domain += item.empty_domain; total.matching_fail += item.matching_fail; |
|
total.matching_pass += item.matching_pass; total.dfs_nodes += item.dfs_nodes; |
|
total.dynamic_matching_fail += item.dynamic_matching_fail; |
|
} |
|
double elapsed = std::chrono::duration<double>( |
|
std::chrono::steady_clock::now() - started).count(); |
|
bool complete = total.subsets == choose(N, radius); |
|
std::cout << "RESULT radius=" << radius << " workers=" << workers |
|
<< " status=" << (complete ? "COMPLETE" : (witness[0] >= 0 ? "WITNESS" : "UNKNOWN")) |
|
<< " subsets=" << total.subsets << " expected=" << choose(N, radius) |
|
<< " persistent=" << total.persistent << " empty_domain=" << total.empty_domain |
|
<< " matching_fail=" << total.matching_fail << " matching_pass=" << total.matching_pass |
|
<< " dfs_nodes=" << total.dfs_nodes |
|
<< " dynamic_matching_fail=" << total.dynamic_matching_fail |
|
<< " dynamic_matching=" << (use_dynamic_matching ? "true" : "false") |
|
<< " elapsed_seconds=" << elapsed << '\n'; |
|
if (witness[0] >= 0) { |
|
std::cout << "witness_zero_based="; |
|
for (int value : witness) std::cout << value << ','; |
|
std::cout << '\n'; |
|
return 0; |
|
} |
|
return complete ? 2 : 1; |
|
} |
