#!/usr/bin/env python3
"""Independent exact audit of the public WOWII Conjecture 200 candidate."""

from __future__ import annotations

import argparse
import json
from fractions import Fraction
from pathlib import Path


LEFT = frozenset(range(6))
RIGHT = frozenset(range(6, 14))
MISSING = frozenset(
    {
        (0, 6), (0, 8), (1, 8), (1, 11), (2, 7), (2, 12),
        (3, 6), (3, 11), (4, 7), (4, 13), (5, 12), (5, 13),
    }
)


def adjacency_from_missing(missing: frozenset[tuple[int, int]]) -> tuple[int, ...]:
    adjacency = [0] * 14
    for left in LEFT:
        for right in RIGHT:
            if (left, right) in missing:
                continue
            adjacency[left] |= 1 << right
            adjacency[right] |= 1 << left
    return tuple(adjacency)


def vertices(mask: int):
    while mask:
        bit = mask & -mask
        yield bit.bit_length() - 1
        mask ^= bit


def connected(adjacency: tuple[int, ...], mask: int) -> bool:
    if mask == 0:
        return False
    seen = mask & -mask
    frontier = seen
    while frontier:
        neighbors = 0
        for vertex in vertices(frontier):
            neighbors |= adjacency[vertex]
        frontier = neighbors & mask & ~seen
        seen |= frontier
    return seen == mask


def edge_count(adjacency: tuple[int, ...], mask: int) -> int:
    return sum((adjacency[vertex] & mask).bit_count() for vertex in vertices(mask)) // 2


def independent(adjacency: tuple[int, ...], mask: int) -> bool:
    return edge_count(adjacency, mask) == 0


def independence_number(adjacency: tuple[int, ...], mask: int) -> int:
    best = 0
    subset = mask
    while True:
        if subset.bit_count() > best and independent(adjacency, subset):
            best = subset.bit_count()
        if subset == 0:
            return best
        subset = (subset - 1) & mask


def induced_tree_census(adjacency: tuple[int, ...]) -> tuple[int, int, list[int]]:
    maximum = 0
    maximum_count = 0
    first_witness: list[int] = []
    for mask in range(1, 1 << len(adjacency)):
        order = mask.bit_count()
        if edge_count(adjacency, mask) != order - 1 or not connected(adjacency, mask):
            continue
        if order > maximum:
            maximum = order
            maximum_count = 0
            first_witness = list(vertices(mask))
        if order == maximum:
            maximum_count += 1
    return maximum, maximum_count, first_witness


def has_hamiltonian_path(adjacency: tuple[int, ...]) -> bool:
    endpoints = [0] * (1 << len(adjacency))
    for vertex in range(len(adjacency)):
        endpoints[1 << vertex] = 1 << vertex
    for mask in range(1, len(endpoints)):
        remaining = mask
        while remaining:
            endpoint = remaining & -remaining
            vertex = endpoint.bit_length() - 1
            remaining ^= endpoint
            if endpoints[mask ^ endpoint] & adjacency[vertex]:
                endpoints[mask] |= endpoint
    return endpoints[-1] != 0


def analyze(missing: frozenset[tuple[int, int]]) -> dict[str, object]:
    adjacency = adjacency_from_missing(missing)
    full = (1 << len(adjacency)) - 1
    local = [independence_number(adjacency, adjacency[vertex]) for vertex in range(14)]
    local_average = Fraction(sum(local), 14)
    tree_size, maximum_tree_count, tree_witness = induced_tree_census(adjacency)
    hamiltonian_path = has_hamiltonian_path(adjacency)
    # Compute ceil(1 + p/q) using integer arithmetic only.
    ceiling = (local_average.numerator + local_average.denominator + local_average.denominator - 1) // local_average.denominator
    return {
        "vertices": 14,
        "edges": edge_count(adjacency, full),
        "connected": connected(adjacency, full),
        "bipartition_sizes": [len(LEFT), len(RIGHT)],
        "degrees": [neighbors.bit_count() for neighbors in adjacency],
        "local_independence_numbers": local,
        "local_independence_sum": sum(local),
        "local_independence_average": str(local_average),
        "ceil_one_plus_average": ceiling,
        "largest_induced_tree_size": tree_size,
        "maximum_induced_tree_count": maximum_tree_count,
        "first_maximum_tree_witness": tree_witness,
        "hamiltonian_path_subset_dp": hamiltonian_path,
        "part_imbalance_obstruction": abs(len(LEFT) - len(RIGHT)) > 1,
        "enumerated_nonempty_vertex_subsets": (1 << 14) - 1,
    }


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--output", type=Path, required=True)
    args = parser.parse_args()

    result = analyze(MISSING)
    expected = {
        "vertices": 14,
        "edges": 36,
        "connected": True,
        "bipartition_sizes": [6, 8],
        "degrees": [6, 6, 6, 6, 6, 6, 4, 4, 4, 6, 6, 4, 4, 4],
        "local_independence_numbers": [6, 6, 6, 6, 6, 6, 4, 4, 4, 6, 6, 4, 4, 4],
        "local_independence_sum": 72,
        "local_independence_average": "36/7",
        "ceil_one_plus_average": 7,
        "largest_induced_tree_size": 7,
        "maximum_induced_tree_count": 78,
        "hamiltonian_path_subset_dp": False,
        "part_imbalance_obstruction": True,
        "enumerated_nonempty_vertex_subsets": 16_383,
    }
    for field, value in expected.items():
        if result[field] != value:
            raise SystemExit(f"audit mismatch for {field}: {result[field]!r} != {value!r}")

    complete_bipartite = analyze(frozenset())
    if complete_bipartite["largest_induced_tree_size"] == complete_bipartite["ceil_one_plus_average"]:
        raise SystemExit("canary failed: verifier did not distinguish the complete bipartite graph")

    report = {
        "claim": "The explicit graph refutes the frozen WOWII Conjecture 200 implication.",
        "result": result,
        "canary": {
            "description": "Replacing the graph by K_6,8 must fail the conjecture-premise equality.",
            "passed": True,
            "complete_bipartite_tree_size": complete_bipartite["largest_induced_tree_size"],
            "complete_bipartite_ceiling": complete_bipartite["ceil_one_plus_average"],
        },
        "implementation": {
            "dependencies": "Python standard library only",
            "relationship_to_candidate": "Independent implementation from the published edge deletion specification; no candidate verifier code is imported.",
        },
    }
    args.output.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8")
    print(json.dumps(report, sort_keys=True))


if __name__ == "__main__":
    main()