#!/usr/bin/env python3
"""Independent NetworkX verifier for the WOWII-200 counterexample.

The graph is K_{6,8} with twelve edges removed.  The missing-edge graph is
the disjoint union of two 6-cycles (plus two isolated vertices on the
8-vertex side).  This script independently checks every graph invariant in
the conjecture, exhaustively enumerates induced trees, and runs an exact
Hamilton-path dynamic program.
"""

from __future__ import annotations

import argparse
import hashlib
import itertools
import json
import math
from fractions import Fraction
from pathlib import Path
from typing import Iterable

import networkx as nx


LEFT = tuple(range(6))
RIGHT = tuple(range(6, 14))
MISSING = (
    (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 sha256_file(path: Path) -> str:
    digest = hashlib.sha256()
    with path.open("rb") as handle:
        for chunk in iter(lambda: handle.read(1024 * 1024), b""):
            digest.update(chunk)
    return digest.hexdigest()


def build_graph() -> nx.Graph:
    graph = nx.Graph()
    graph.add_nodes_from(LEFT + RIGHT)
    missing = {tuple(sorted(edge)) for edge in MISSING}
    graph.add_edges_from(
        (left, right)
        for left in LEFT
        for right in RIGHT
        if (left, right) not in missing
    )
    return graph


def maximum_independent_size(graph: nx.Graph, vertices: Iterable[int]) -> int:
    values = tuple(vertices)
    for size in range(len(values), -1, -1):
        for subset in itertools.combinations(values, size):
            if graph.subgraph(subset).number_of_edges() == 0:
                return size
    raise AssertionError("empty set should always be independent")


def exact_largest_induced_tree(graph: nx.Graph) -> tuple[int, list[list[int]]]:
    vertices = tuple(sorted(graph))
    best = 0
    witnesses: list[list[int]] = []
    for mask in range(1, 1 << len(vertices)):
        size = bin(mask).count("1")
        if size < best:
            continue
        selected = [
            vertices[index]
            for index in range(len(vertices))
            if mask & (1 << index)
        ]
        if not nx.is_tree(graph.subgraph(selected)):
            continue
        if size > best:
            best = size
            witnesses = []
        witnesses.append(selected)
    return best, witnesses


def exact_hamilton_path(graph: nx.Graph) -> tuple[bool, list[int] | None]:
    """Held--Karp subset DP, with a predecessor map for any witness."""
    vertices = tuple(sorted(graph))
    index = {vertex: position for position, vertex in enumerate(vertices)}
    full = (1 << len(vertices)) - 1
    reachable = [0] * (1 << len(vertices))
    predecessor: dict[tuple[int, int], int] = {}
    for position in range(len(vertices)):
        reachable[1 << position] = 1 << position
    for mask in range(1, full + 1):
        endpoints = reachable[mask]
        while endpoints:
            endpoint_bit = endpoints & -endpoints
            endpoint = endpoint_bit.bit_length() - 1
            endpoints ^= endpoint_bit
            for neighbor_vertex in graph.neighbors(vertices[endpoint]):
                neighbor = index[neighbor_vertex]
                neighbor_bit = 1 << neighbor
                if mask & neighbor_bit:
                    continue
                next_mask = mask | neighbor_bit
                if not (reachable[next_mask] & neighbor_bit):
                    reachable[next_mask] |= neighbor_bit
                    predecessor[(next_mask, neighbor)] = endpoint
    if not reachable[full]:
        return False, None
    endpoint = (reachable[full] & -reachable[full]).bit_length() - 1
    path = []
    mask = full
    while True:
        path.append(vertices[endpoint])
        if mask == 1 << endpoint:
            break
        previous = predecessor[(mask, endpoint)]
        mask ^= 1 << endpoint
        endpoint = previous
    path.reverse()
    return True, path


def induced_tree_upper_bound_cases() -> list[dict[str, int | bool]]:
    """Check the elementary edge-count contradiction for every part size."""
    cases = []
    for left_count in range(2, len(LEFT) + 1):
        for right_count in range(2, len(RIGHT) + 1):
            if left_count + right_count < 8:
                continue
            required_missing = (left_count - 1) * (right_count - 1)
            degree_two_upper = 2 * min(left_count, right_count)
            cases.append(
                {
                    "left_count": left_count,
                    "right_count": right_count,
                    "required_missing_edges_for_tree": required_missing,
                    "missing_edges_upper_bound": degree_two_upper,
                    "contradiction": required_missing > degree_two_upper,
                }
            )
    return cases


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


def main() -> None:
    args = parse_args()
    graph = build_graph()
    expected_edges = len(LEFT) * len(RIGHT) - len(MISSING)
    if graph.number_of_edges() != expected_edges:
        raise AssertionError("edge construction mismatch")

    local_independence = {
        vertex: maximum_independent_size(graph, graph.neighbors(vertex))
        for vertex in graph
    }
    local_sum = sum(local_independence.values())
    local_average = Fraction(local_sum, graph.number_of_nodes())
    required_tree_size = math.ceil(1 + local_average)
    largest_tree_size, tree_witnesses = exact_largest_induced_tree(graph)
    has_hamilton_path, hamilton_path = exact_hamilton_path(graph)
    upper_cases = induced_tree_upper_bound_cases()

    canonical_tree_witness = [0, 1, 2, 3, 4, 6, 7]
    witness_graph = graph.subgraph(canonical_tree_witness)
    missing_graph = nx.Graph()
    missing_graph.add_nodes_from(LEFT + RIGHT)
    missing_graph.add_edges_from(MISSING)
    nontrivial_missing_components = sorted(
        (
            sorted(component)
            for component in nx.connected_components(missing_graph)
            if len(component) > 1
        ),
        key=lambda component: component[0],
    )

    checks = {
        "simple": not graph.is_multigraph()
        and nx.number_of_selfloops(graph) == 0,
        "connected": nx.is_connected(graph),
        "bipartite": nx.is_bipartite(graph),
        "declared_bipartition_valid": all(
            (
                left in LEFT and right in RIGHT
                or left in RIGHT and right in LEFT
            )
            for left, right in graph.edges()
        ),
        "part_size_imbalance_blocks_hamilton_path": (
            abs(len(LEFT) - len(RIGHT)) > 1
        ),
        "exact_dp_finds_no_hamilton_path": not has_hamilton_path,
        "every_neighborhood_independent": all(
            graph.subgraph(tuple(graph.neighbors(vertex))).number_of_edges()
            == 0
            for vertex in graph
        ),
        "local_independence_sum_is_72": local_sum == 72,
        "ceiling_is_7": required_tree_size == 7,
        "canonical_induced_tree_witness": (
            witness_graph.number_of_nodes() == 7
            and nx.is_tree(witness_graph)
        ),
        "exhaustive_largest_induced_tree_is_7": largest_tree_size == 7,
        "all_large_two_part_tree_cases_contradict_edge_bound": all(
            bool(case["contradiction"]) for case in upper_cases
        ),
        "maximum_graph_degree_is_6": max(dict(graph.degree()).values()) == 6,
        "missing_graph_is_two_disjoint_6_cycles": (
            len(nontrivial_missing_components) == 2
            and all(len(component) == 6 for component in nontrivial_missing_components)
            and all(
                missing_graph.subgraph(component).number_of_edges() == 6
                and all(
                    degree == 2
                    for _, degree in missing_graph.subgraph(component).degree()
                )
                for component in nontrivial_missing_components
            )
        ),
    }
    verified = all(checks.values()) and (
        largest_tree_size == required_tree_size
    )

    script_path = Path(__file__).resolve()
    report = {
        "problem": "Written on the Wall II, Conjecture 200",
        "claim": "explicit counterexample",
        "verified_by_this_script": verified,
        "vertices": sorted(graph),
        "left_part": list(LEFT),
        "right_part": list(RIGHT),
        "edge_count": graph.number_of_edges(),
        "missing_edges_from_K6_8": [list(edge) for edge in MISSING],
        "edge_list": [list(edge) for edge in sorted(graph.edges())],
        "graph6": nx.to_graph6_bytes(
            graph,
            nodes=sorted(graph),
            header=False,
        ).decode("ascii").strip(),
        "degrees": {
            str(vertex): graph.degree(vertex) for vertex in sorted(graph)
        },
        "local_independence": {
            str(vertex): local_independence[vertex]
            for vertex in sorted(graph)
        },
        "local_independence_sum": local_sum,
        "average_local_independence": {
            "numerator": local_average.numerator,
            "denominator": local_average.denominator,
        },
        "ceiling_of_one_plus_average": required_tree_size,
        "largest_induced_tree_size": largest_tree_size,
        "number_of_maximum_induced_tree_witnesses": len(tree_witnesses),
        "first_maximum_induced_tree_witnesses": tree_witnesses[:20],
        "canonical_tree_witness": canonical_tree_witness,
        "canonical_tree_witness_edges": [
            list(edge) for edge in sorted(witness_graph.edges())
        ],
        "hamilton_path_dp_result": has_hamilton_path,
        "hamilton_path_dp_witness": hamilton_path,
        "missing_graph_nontrivial_components": nontrivial_missing_components,
        "induced_tree_upper_bound_cases": upper_cases,
        "checks": checks,
        "runtime": {
            "networkx": nx.__version__,
        },
        "verifier_path": "verification/verify_networkx.py",
        "verifier_sha256": sha256_file(script_path),
    }
    args.output.parent.mkdir(parents=True, exist_ok=True)
    args.output.write_text(
        json.dumps(report, indent=2) + "\n",
        encoding="utf-8",
    )
    print(json.dumps(report, indent=2))
    if not verified:
        raise SystemExit(1)


if __name__ == "__main__":
    main()