Ramsey number R(5,5)

"""Verifier for "Ramsey number R(5,5)" (statement in ramsey_5_5.json).

Problem: colour each edge of the complete graph on V vertices {0, ..., V-1}
with one of two colours so that no CLIQUE vertices have all the edges between
them in the same colour (no monochromatic K_CLIQUE). It is known that
43 <= R(5,5) <= 46; a valid colouring of K_43 would prove R(5,5) >= 44,
disproving the conjecture that R(5,5) = 43.

Expected submission: a JSON object with the C(V, 2) edge colours as JSON
integers 0 or 1, listed row by row over the pairs i < j:
(0,1), (0,2), ..., (0,V-1), (1,2), ..., (V-2,V-1). For example (V = 4):

    {"coloring": [0, 1, 1, 0, 1, 0]}

What the verifier checks, in order:
  1. The payload is at most MAX_BYTES characters and is a JSON object with
     exactly the key "coloring".
  2. "coloring" is a list of exactly C(V, 2) integers, each 0 or 1.
  3. Neither colour class contains a clique of CLIQUE vertices.

How step 3 is done: rather than testing all C(43, 5) = 962,598 vertex
subsets, each colour class is stored as a graph whose neighbourhoods are
bitmasks, and cliques are grown one vertex at a time, keeping only the
candidates adjacent to every vertex chosen so far (see _has_clique). Each
call of the search stands for one monochromatic clique of fewer than CLIQUE
vertices, so the work is bounded by the number of 4-vertex subsets,
C(43, 4) = 123,410, and in practice takes milliseconds.
"""
import itertools
import json

# Number of vertices of the complete graph.
V = 43
# Size of the forbidden monochromatic clique.
CLIQUE = 5
# Maximum size of the whole submission, in characters.
MAX_BYTES = 20_000


# ---------------------------------------------------------------------------
# Input-parsing helpers. The same code is copied into every verifier that
# needs it, so that each file works on its own.
# ---------------------------------------------------------------------------

def _load(solution, keys, max_bytes):
    """Parse the submission as a JSON object with exactly the given keys, or raise."""
    # Refuse oversized payloads before handing them to the JSON parser.
    if not isinstance(solution, str) or len(solution) > max_bytes:
        raise ValueError
    d = json.loads(solution)
    # It must be an object (not a list, string or number) whose keys are
    # exactly the expected ones: nothing missing, nothing extra.
    if not isinstance(d, dict) or set(d) != set(keys):
        raise ValueError
    return d


def _int_list(values, n, lo, hi):
    """Return `values` if it is a list of exactly n integers in [lo, hi], or raise.

    The length is checked before any element is looked at. `type(v) is int`
    (rather than isinstance) also rejects true and false, which Python treats
    as the integers 1 and 0; floats such as 1.0 and strings such as "1" are
    rejected as well.
    """
    if not isinstance(values, list) or len(values) != n:
        raise ValueError
    for v in values:
        if type(v) is not int or not lo <= v <= hi:
            raise ValueError
    return values


def _has_clique(adj, candidates, k):
    """True iff k of the vertices in `candidates` are pairwise adjacent in `adj`.

    `adj[v]` is the bitmask of v's neighbours and `candidates` a bitmask of
    vertices. The search takes the highest remaining candidate v and looks for
    a (k - 1)-clique among the candidates adjacent to v; if there is none, v is
    dropped for good. Each clique is therefore explored once, from its highest
    vertex down, and a branch is abandoned as soon as fewer than k candidates
    remain.
    """
    if k == 0:
        return True
    while candidates.bit_count() >= k:
        v = candidates.bit_length() - 1  # highest remaining candidate
        candidates &= ~(1 << v)  # v is dealt with now, never again
        if _has_clique(adj, candidates & adj[v], k - 1):
            return True
    return False


# ---------------------------------------------------------------------------
# The actual check.
# ---------------------------------------------------------------------------

def _check(solution):
    # Steps 1-2: read the JSON object and the C(V, 2) edge colours.
    sol = _load(solution, ("coloring",), MAX_BYTES)
    coloring = _int_list(sol["coloring"], V * (V - 1) // 2, 0, 1)

    # Build one graph per colour; graphs[c][v] is the bitmask of the vertices
    # joined to v by an edge of colour c. itertools.combinations yields the
    # pairs i < j in exactly the documented row-by-row order.
    graphs = ([0] * V, [0] * V)
    for (i, j), colour in zip(itertools.combinations(range(V), 2), coloring):
        graphs[colour][i] |= 1 << j
        graphs[colour][j] |= 1 << i

    # Step 3: no clique of CLIQUE vertices in either colour.
    everyone = (1 << V) - 1
    return not any(_has_clique(graph, everyone, CLIQUE) for graph in graphs)


def verify(solution: str, rng) -> bool:
    """Platform entry point: return True only for a valid, correct solution.

    `rng` (a numpy.random.Generator) is part of the platform interface but is
    not used: this check is deterministic. Any exception (malformed JSON, a bad
    value, ...) means the submission is rejected, so this function never raises.
    """
    try:
        return _check(solution) is True
    except Exception:
        return False