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

This script uses only the Python standard library.  It reconstructs the graph
from a compact K_{6,8}-minus-edges specification, checks the graph6 encoding,
enumerates every induced subgraph, and runs an exact Hamilton-path subset DP.
The output is a portable JSON certificate of the finite checks.
"""

from __future__ import annotations

import argparse
import hashlib
import json
from collections import Counter, deque
from fractions import Fraction
from pathlib import Path


GRAPH6 = "M??B]g{~FwT_u?{??"
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),
}
TREE_WITNESS = (0, 1, 2, 3, 4, 6, 7)


def popcount(value: int) -> int:
    return bin(value).count("1")


def graph_from_spec() -> list[int]:
    adjacency = [0] * 14
    for u in LEFT:
        for v in RIGHT:
            if (u, v) not in MISSING:
                adjacency[u] |= 1 << v
                adjacency[v] |= 1 << u
    return adjacency


def decode_graph6(text: str) -> list[int]:
    """Decode the small-order graph6 form (n <= 62)."""
    order = ord(text[0]) - 63
    assert 0 <= order <= 62
    bits: list[int] = []
    for character in text[1:]:
        value = ord(character) - 63
        assert 0 <= value < 64
        bits.extend((value >> shift) & 1 for shift in range(5, -1, -1))
    adjacency = [0] * order
    index = 0
    for high in range(1, order):
        for low in range(high):
            if bits[index]:
                adjacency[low] |= 1 << high
                adjacency[high] |= 1 << low
            index += 1
    return adjacency


def encode_graph6(adjacency: list[int]) -> str:
    order = len(adjacency)
    assert order <= 62
    bits = [
        (adjacency[low] >> high) & 1
        for high in range(1, order)
        for low in range(high)
    ]
    while len(bits) % 6:
        bits.append(0)
    data = []
    for start in range(0, len(bits), 6):
        value = 0
        for bit in bits[start : start + 6]:
            value = 2 * value + bit
        data.append(chr(value + 63))
    return chr(order + 63) + "".join(data)


def vertices(mask: int) -> list[int]:
    return [v for v in range(14) if mask & (1 << v)]


def edge_count(adjacency: list[int], mask: int) -> int:
    return sum(popcount(adjacency[v] & mask) for v in vertices(mask)) // 2


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


def bipartition(adjacency: list[int]) -> tuple[list[int], list[int]]:
    colors: list[int | None] = [None] * len(adjacency)
    for source in range(len(adjacency)):
        if colors[source] is not None:
            continue
        colors[source] = 0
        queue = deque([source])
        while queue:
            u = queue.popleft()
            for v in vertices(adjacency[u]):
                if colors[v] is None:
                    colors[v] = 1 - int(colors[u])
                    queue.append(v)
                else:
                    assert colors[v] != colors[u]
    return (
        [v for v, color in enumerate(colors) if color == 0],
        [v for v, color in enumerate(colors) if color == 1],
    )


def independent(adjacency: list[int], mask: int) -> bool:
    remainder = mask
    while remainder:
        bit = remainder & -remainder
        v = bit.bit_length() - 1
        remainder ^= bit
        if adjacency[v] & remainder:
            return False
    return True


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


def induced_tree_stats(
    adjacency: list[int],
) -> tuple[int, list[int], dict[int, int]]:
    maximum = 0
    witness: list[int] = []
    counts: Counter[int] = Counter()
    for mask in range(1, 1 << len(adjacency)):
        order = popcount(mask)
        if edge_count(adjacency, mask) != order - 1:
            continue
        if connected(adjacency, mask):
            counts[order] += 1
            if order > maximum:
                maximum = order
                witness = vertices(mask)
    return maximum, witness, dict(sorted(counts.items()))


def has_hamiltonian_path(adjacency: list[int]) -> bool:
    """Exact subset DP: endpoints[mask] is the set of feasible last vertices."""
    order = len(adjacency)
    endpoints = [0] * (1 << order)
    for v in range(order):
        endpoints[1 << v] = 1 << v
    for mask in range(1, 1 << order):
        if mask & (mask - 1) == 0:
            continue
        remainder = mask
        while remainder:
            bit = remainder & -remainder
            v = bit.bit_length() - 1
            if endpoints[mask ^ bit] & adjacency[v]:
                endpoints[mask] |= bit
            remainder ^= bit
    return bool(endpoints[-1])


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


def main() -> None:
    args = parse_args()
    adjacency = graph_from_spec()
    assert adjacency == decode_graph6(GRAPH6)
    assert encode_graph6(adjacency) == GRAPH6

    full = (1 << len(adjacency)) - 1
    edges = [
        [u, v]
        for u in range(14)
        for v in range(u + 1, 14)
        if adjacency[u] & (1 << v)
    ]
    assert connected(adjacency, full)
    parts = bipartition(adjacency)
    assert sorted(map(len, parts)) == [6, 8]

    local_independence = [
        independence_number(adjacency, adjacency[v]) for v in range(14)
    ]
    local_sum = sum(local_independence)
    premise_value = (14 + local_sum + 13) // 14

    tree_size, tree_witness, tree_counts = induced_tree_stats(adjacency)
    witness_mask = sum(1 << v for v in TREE_WITNESS)
    assert edge_count(adjacency, witness_mask) == len(TREE_WITNESS) - 1
    assert connected(adjacency, witness_mask)
    assert tree_size == 7
    assert premise_value == 7

    hamiltonian_path = has_hamiltonian_path(adjacency)
    assert not hamiltonian_path

    # Machine-check the finite pair analysis used in the prose upper bound.
    possible_large_tree_part_sizes = []
    for left_size in range(1, 7):
        for right_size in range(1, 9):
            if left_size + right_size < 8:
                continue
            smaller = min(left_size, right_size)
            larger = max(left_size, right_size)
            if smaller == 1:
                possible = larger <= max(popcount(mask) for mask in adjacency)
            else:
                required_missing = (left_size - 1) * (right_size - 1)
                possible = required_missing <= 2 * smaller
            if possible:
                possible_large_tree_part_sizes.append([left_size, right_size])
    assert not possible_large_tree_part_sizes

    edge_encoding = json.dumps(edges, separators=(",", ":")).encode("ascii")
    report = {
        "claim_status": "verified_counterexample",
        "conjecture": "WOWII-200",
        "graph": {
            "description": "K_{6,8} minus two disjoint C6 missing-edge cycles",
            "graph6": GRAPH6,
            "n": 14,
            "m": len(edges),
            "bipartition": [list(LEFT), list(RIGHT)],
            "missing_edges_from_K6_8": [list(edge) for edge in sorted(MISSING)],
            "edges": edges,
            "edge_list_sha256": hashlib.sha256(edge_encoding).hexdigest(),
            "degrees": [popcount(mask) for mask in adjacency],
            "connected": True,
        },
        "premise": {
            "local_independence_numbers": local_independence,
            "sum": local_sum,
            "average": str(Fraction(local_sum, 14)),
            "ceil_one_plus_average": premise_value,
            "largest_induced_tree_size": tree_size,
            "induced_tree_witness": list(TREE_WITNESS),
            "all_induced_tree_counts_by_order": tree_counts,
            "no_possible_tree_part_sizes_of_total_order_at_least_8": True,
        },
        "conclusion": {
            "hamiltonian_path_subset_dp": hamiltonian_path,
            "structural_obstruction": (
                "A path in a bipartite graph uses part sizes differing by at "
                "most one, but this graph has part sizes six and eight."
            ),
        },
        "implementation": {
            "script": "verification/verify_stdlib.py",
            "dependencies": "Python standard library only",
            "enumerated_induced_vertex_subsets": (1 << 14) - 1,
            "note": (
                "Independent implementation from the NetworkX verifier."
            ),
        },
    }
    rendered = json.dumps(report, indent=2, sort_keys=True) + "\n"
    if args.output is not None:
        args.output.parent.mkdir(parents=True, exist_ok=True)
        args.output.write_text(rendered, encoding="utf-8")
    print(rendered, end="")


if __name__ == "__main__":
    main()