"""Claim 5 -- Section 3: computing incomp(G) exactly is NP-hard, because
"computing incomp(G) for an acyclic directed graph after adding all possible
bidirected edges is equivalent to solving the ACYCLIC TRANSITIVITY EDITING
problem" (hardness of the latter: Weller et al., 2012).

What is reproducible here is the REDUCTION, i.e. the identity

        incomp( D + all bidirected edges )  ==  ATE(D)        for every acyclic D,

together with the fact that the map D -> D + all bidirected edges is computable
in O(n^2).  The external hardness premise (Weller et al. 2012) is ASSUMED, not
reproduced -- see Limitations.
"""
import json, itertools, pickle, random, collections
import gcore

R = {}


def all_digraphs(n):
    enc = gcore.Enc(n)
    return enc, range(1 << enc.nd)


def ate_table(n):
    """Exact ACYCLIC TRANSITIVITY EDITING optimum for every digraph on n vertices,
    by multi-source BFS from all acyclic + transitively closed digraphs."""
    enc = gcore.Enc(n)
    N = 1 << enc.nd
    dist = bytearray([255]) * N
    frontier = []
    for d in range(N):
        succ = gcore.adj_from_dbits(n, enc.dir_pairs, d)
        if gcore.is_acyclic(n, succ) and gcore.is_transitively_closed(n, succ):
            dist[d] = 0
            frontier.append(d)
    k = 0
    while frontier:
        nxt = []
        for g in frontier:
            for b in range(enc.nd):
                h = g ^ (1 << b)
                if dist[h] == 255:
                    dist[h] = k + 1
                    nxt.append(h)
        frontier = nxt
        k += 1
    return enc, dist, frontier


# ------------------------------------------------- exhaustive reduction check
red = {}
for n in (3, 4):
    enc = gcore.Enc(n)
    ate_enc, ate, _ = ate_table(n)
    dist, compat = gcore.exact_incomp_table(enc)
    allbid = 0
    for e in enc.bid_pairs:
        allbid |= 1 << enc.BID[e]
    dags = []
    mism = 0
    hist_i, hist_a = collections.Counter(), collections.Counter()
    for d in range(1 << enc.nd):
        succ = gcore.adj_from_dbits(n, enc.dir_pairs, d)
        if not gcore.is_acyclic(n, succ):
            continue
        dags.append(d)
        i_val = dist[d | allbid]
        a_val = ate[d]
        hist_i[i_val] += 1; hist_a[a_val] += 1
        if i_val != a_val:
            mism += 1
    red[n] = dict(n_dags=len(dags), mismatches=mism,
                  incomp_histogram=dict(sorted(hist_i.items())),
                  ate_histogram=dict(sorted(hist_a.items())),
                  max_value=max(hist_i))
    print("n=%d" % n, red[n], flush=True)
R["reduction_exhaustive"] = red

# ------------------------------------------------------------ negative controls
ctl = {}

# (a) robustness probe only: the paper's reduction is stated for acyclic input.
# Do not assume that the finite identity must fail outside that scope; record the
# result literally and do not use it as a destructive control.
for n in (3, 4):
    enc = gcore.Enc(n)
    _, ate, _ = ate_table(n)
    dist, _ = gcore.exact_incomp_table(enc)
    allbid = 0
    for e in enc.bid_pairs:
        allbid |= 1 << enc.BID[e]
    tot = mism = 0
    for d in range(1 << enc.nd):
        succ = gcore.adj_from_dbits(n, enc.dir_pairs, d)
        if gcore.is_acyclic(n, succ):
            continue
        tot += 1
        if dist[d | allbid] != ate[d]:
            mism += 1
    ctl[f"cyclic inputs n={n}"] = dict(cyclic_digraphs=tot, mismatches=mism,
                                       mismatch_rate=mism / tot if tot else 0)
    print("control (cyclic inputs) n=%d" % n, ctl[f"cyclic inputs n={n}"], flush=True)

# (b) drop the "add all bidirected edges" step of the reduction
for n in (3, 4):
    enc = gcore.Enc(n)
    _, ate, _ = ate_table(n)
    dist, _ = gcore.exact_incomp_table(enc)
    tot = mism = 0
    for d in range(1 << enc.nd):
        succ = gcore.adj_from_dbits(n, enc.dir_pairs, d)
        if not gcore.is_acyclic(n, succ):
            continue
        tot += 1
        if dist[d] != ate[d]:          # no bidirected edges added
            mism += 1
    ctl[f"no bidirected edges added n={n}"] = dict(dags=tot, mismatches=mism,
                                                   mismatch_rate=mism / tot)
    print("control (skip 'add all bidirected') n=%d" % n,
          ctl[f"no bidirected edges added n={n}"], flush=True)

# (c) drop transitive closure from the target predicate (acyclicity only)
for n in (4,):
    enc = gcore.Enc(n)
    N = 1 << enc.nd
    dist_ac = bytearray([255]) * N
    fr = []
    for d in range(N):
        if gcore.is_acyclic(n, gcore.adj_from_dbits(n, enc.dir_pairs, d)):
            dist_ac[d] = 0; fr.append(d)
    k = 0
    while fr:
        nxt = []
        for g in fr:
            for b in range(enc.nd):
                h = g ^ (1 << b)
                if dist_ac[h] == 255:
                    dist_ac[h] = k + 1; nxt.append(h)
        fr = nxt; k += 1
    _, ate, _ = ate_table(n)
    tot = mism = 0
    for d in range(N):
        if not gcore.is_acyclic(n, gcore.adj_from_dbits(n, enc.dir_pairs, d)):
            continue
        tot += 1
        if dist_ac[d] != ate[d]:
            mism += 1
    ctl[f"acyclicity-only target n={n}"] = dict(dags=tot, mismatches=mism,
                                                mismatch_rate=mism / tot)
    print("control (acyclicity-only target) n=4", ctl["acyclicity-only target n=4"], flush=True)
R["controls"] = ctl

# --------------------------------------------------------- sampled n = 5 check
enc5 = gcore.Enc(5)
rng = random.Random(5)
allbid5 = 0
for e in enc5.bid_pairs:
    allbid5 |= 1 << enc5.BID[e]


def ate_bounded(n, d, ub=6):
    enc = gcore.Enc(n)
    succ = gcore.adj_from_dbits(n, enc.dir_pairs, d)
    if gcore.is_acyclic(n, succ) and gcore.is_transitively_closed(n, succ):
        return 0
    for k in range(1, ub + 1):
        for combo in itertools.combinations(range(enc.nd), k):
            h = d
            for b in combo:
                h ^= 1 << b
            s2 = gcore.adj_from_dbits(n, enc.dir_pairs, h)
            if gcore.is_acyclic(n, s2) and gcore.is_transitively_closed(n, s2):
                return k
    return None


n5, mism5, vals5 = 0, 0, []
tries = 0
while n5 < 120 and tries < 6000:
    tries += 1
    d = rng.getrandbits(enc5.nd)
    succ = gcore.adj_from_dbits(5, enc5.dir_pairs, d)
    if not gcore.is_acyclic(5, succ):
        continue
    a = ate_bounded(5, d, 4)
    if a is None:
        continue
    i = gcore.bounded_incomp(enc5, d | allbid5, 4)
    n5 += 1
    vals5.append(a)
    if a != i:
        mism5 += 1
R["sampled_n5"] = dict(dags_tested=n5, mismatches=mism5,
                       ate_histogram=dict(sorted(collections.Counter(vals5).items())))
print("sampled n=5:", R["sampled_n5"], flush=True)

# ----------------------------------------- reduction is polynomial-time (O(n^2))
R["reduction_cost"] = {str(n): dict(bidirected_edges_added=n * (n - 1) // 2,
                                    total_edges=n * (n - 1) + n * (n - 1) // 2)
                       for n in (3, 4, 5, 10, 50)}

# ------------- the paper's remark: deciding incomp(G) <= k is polynomial for fixed k
R["ball_search_sizes"] = {}
for n in (5, 10, 20, 50):
    bits = n * (n - 1) + n * (n - 1) // 2
    R["ball_search_sizes"][str(n)] = {f"k={k}": int(
        __import__("math").comb(bits, k)) for k in (1, 2, 3)}
print("ball sizes (poly in n for fixed k):", R["ball_search_sizes"]["10"], flush=True)

json.dump(R, open("outputs/claim5.json", "w"), indent=1, default=str)
print("\nwrote outputs/claim5.json")