Repository navigation
Conversation
Collaborator
Author
Verification certificateVerdict: VERIFIED mathematically and against the Rust construction. Worktree: Type gate: source The theorem is Failing behavior tests were established before implementation for the polynomial repeated-string size and unavailable MVC→LCS fields. The unused-symbol regression additionally failed on integer overflow before alphabet restriction. Expected results came from the proof, independent source enumeration, and separately written constructor/adversary scripts. PR: #1193; verified implementation commit: Repository gates and workflow evidence after /simplifyThe mathematical construction and its size formulas are unchanged. The decoder now stores group-completeness flags and output symbols, eliminating the full embedding-assignment vectors and final output copy. Canonical source data is derived from its existing assignment array; the CLI test uses a direct field lookup. An existing rejection test now explicitly covers an independent set with a complete symbol cluster but no embedding group, and passed before and after the refactor.
The earlier full The original constructor and independent adversary suites were not repeated because the graph construction and mathematical proof did not change. Their evidence below remains applicable; the rewritten Rust decoder was rechecked against their exports. No large-instance performance benchmark was run. The graph is polynomial, but can be larger than the legacy construction for a small fixed number of strings. Previously saved LCS→MIS routes/bundles/witnesses should be regenerated, because vertex numbering, cardinality, and parameter schema changed. No merge was performed. The verified changes are committed as Constructor counts{
"verdict": "VERIFIED",
"exhaustive_cases": 9472,
"checks": {
"symbolic": 2,
"overhead": 18954,
"optimal_equivalence": 18954,
"extraction_and_expansion": 34500,
"all_forward_words": 10479,
"structure": 9477,
"rejected_witnesses": 686,
"worked_yes_no_examples": 8,
"sparse_declared_alphabet": 3
},
"total_checks": 93063
}Independent adversary counts and settings{
"proof_correct": true,
"counts": {
"size_and_edges": 9945,
"optimum_and_backward": 9945,
"forward_words": 11901,
"expanded_clone_equivalence": 9945,
"malformed_rejected": 42491,
"exhaustive_families": 9472,
"expanded_exact_optima": 397,
"saturated_missing_group_bound": 48130,
"incomplete_independent_sets_rejected": 47138,
"complete_backward_encodings": 992,
"extra_boundary_families": 5,
"all_pairs_gap_case": 1,
"sparse_alphabet_invariance": 125,
"extra_sparse_families": 5,
"invalid_inputs_rejected": 4,
"worked_examples": 2,
"hypothesis_arbitrary": 180,
"hypothesis_shared_word": 160,
"hypothesis_sparse_labels": 120,
"constructor_cross_comparisons": 120
},
"total_counted_checks": 181135,
"count_definition": "Counts validation groups, excluding case bookkeeping; each group checks a distinct failure mode, not an atomic assert count.",
"exhaustive_scope": "all ordered binary string tuples with k in 0..5 and sum(lengths) in 0..5, including empty strings",
"hypothesis": {
"seeds": [
739104,
739105,
739106
],
"max_examples": [
180,
160,
120
],
"deadline": null,
"database": null,
"strategies": [
"arbitrary ternary string families",
"alphabet-varying shared-word embeddings",
"sparse original integer labels with huge declared alphabets"
]
},
"export_count": 165,
"examples": [
{
"strings": [
[
0,
1,
2
],
[
1,
0,
2
],
[
0,
1,
2
]
],
"word": [
0,
2
],
"source_optimum": 2,
"target_optimum": 26,
"vertices": 105,
"edges": 1323
},
{
"strings": [
[
0,
1,
0,
2
],
[
1,
0,
2,
0
]
],
"word": [
1,
0,
2
],
"source_optimum": 3,
"target_optimum": 27,
"vertices": 124,
"edges": 1936
}
],
"limitations": [
"Finite computational checks supplement the mathematical audit; do not prove all lengths.",
"No repository or parent implementation code was read."
]
}
Rust cross-comparison{
"verdict": "VERIFIED",
"unique_rust_graphs_and_decoders_checked": 162,
"malformed_independent_sets_rejected": 486,
"out_of_usize_domain_python_cases_skipped": 3
}Python-only sparse cases beyond Rust’s Typst proof#set page(width: 180mm, margin: 15mm)
#set text(size: 10pt)
= Polynomial-size LCS to unweighted MIS
*Type resolution.* The source is `LongestCommonSubsequence` with `Value = Max<i64>`.
The target is `MaximumIndependentSet<SimpleGraph, One>` with `Value = Max<i64>`,
since `One::Sum = i64`. Both witnesses have finite coordinate spaces.
*Theorem.* For strings $s_1, dots, s_k$ over a finite declared alphabet, let $A$ be the number of distinct symbols occurring in the strings and let
$L = min_i |s_i|$ (or zero for no strings), $T = sum_i |s_i|$,
$G = L(k+1)$, $M = 2$, and $B = 2 G$.
The construction below produces an unweighted graph with
$alpha(H) = B + "LCS"(s_1, dots, s_k)$ and polynomial size.
*Construction.*
1. For each slot $p in {0, dots, L-1}$ create a symbol-choice group
$X_p$ with choices $a$ occurring in at least one input string and one padding choice $bot$.
2. For each string $r$ and slot $p$ create an embedding-choice group
$Y_(r,p)$ with choices $j in {0, dots, |s_r|-1}$ and padding $bot$.
There are $G$ groups. Replace every choice by an independent cluster of
$M$ vertices, except active symbol choices, which have $M+1$ vertices.
3. Join every pair of distinct choices within a group by all edges between
their clusters. Hence an independent set can use at most one choice per group.
4. For symbol groups at slots $p<q$, join padding at $p$ to every active
choice at $q$. This enforces a suffix of padding.
5. For $X_p$ and $Y_(r,p)$, join incompatible choices: padding is compatible
only with padding; active symbol $a$ and position $j$ are compatible
exactly when $s_r[j]=a$.
6. For two embedding groups belonging to the same string at slots $p<q$,
join padding at $p$ to an active position at $q$, and join active positions
$j,j'$ unless $j<j'$. Active followed by padding and two padding choices
are compatible. There are no other edges.
*Forward correctness.* Let $w$ be any common subsequence of length $ell <= L$.
Choose its symbols in slots $0$ through $ell-1$ and padding in remaining slots.
For every string choose strictly increasing positions witnessing its embedding,
then padding. Select all vertices of all chosen clusters. No within-group
edges are selected; symbols and positions agree; every string's positions
increase; padding is a suffix. Thus the selected set is independent and has
cardinality $B+ell$. In particular all-padding gives an independent set of size $B$.
*Backward correctness.* Within-group edges restrict an independent set to
one nonempty cluster per group. Vertices within a cluster have identical
external neighbours and no internal edges. If an independent set is maximum,
every nonempty chosen cluster is full, since another clone can otherwise be added.
Suppose it omits $d_X$ symbol groups and $d_Y$ embedding groups, and selects
$q$ active symbol choices. Discard each active slot with a missing embedding
group. At most $d_Y$ active slots are discarded. The remaining symbols have
compatible positions in every string, and those positions increase strictly
across all retained slot pairs. Thus they form a common subsequence of length
at least $q-d_Y$, so $q <= "LCS" + d_Y$. Its saturated size is then at most
$2(G-d_X-d_Y)+q <= 2G + "LCS" - 2d_X-d_Y$.
Whenever a group is absent this is strictly below the full encoding of an
optimal common subsequence, whose size is $2G+"LCS"$. Therefore an optimum
contains one full cluster in every group. The symbol
choices form a padded sequence; every embedding group matches its symbol,
and embedding positions increase strictly. Removing padding yields a common
subsequence of length $ell$, and the independent-set size is $B+ell$.
Combining directions proves the theorem. If $L=0$, there are no groups,
the target graph is empty, $B=0$, and both optima are zero.
*Extraction.* First validate the target's solution against the graph. Reject
partial clusters, missing groups, or multiple selected choices. Read the
choices of $X_0$ through $X_(L-1)$ as the source's fixed-length padded witness.
Every optimum passes these checks. A complete nonoptimal encoding also decodes
to a valid (possibly nonoptimal) source witness. Malformed or incomplete
independent sets are errors, never repaired by inventing choices.
*Overhead.* Symbol groups contribute $L(A(M+1)+M)$ vertices; embedding groups
contribute $L(T+k)M$. Therefore
$V_H = L(3A+2+2(T+k))$ exactly.
Use the upper bound $E_H <= V_H^2$ for edges. Construction scans pairs of
logical choices, inserts their complete bipartite edges, and runs in
$O(V_H^2 + T log(T+1) + k)$ time; extraction takes $O(V_H+E_H)$ including validation.
Since $A <= T$, the graph is polynomial in the total input string length, even for an enormous declared alphabet. These formulas do not use products across strings.
*YES and NO example.* With alphabet $(A,B,C)$ and strings ABC, BAC, ABC,
$L=3$, $k=3$, $T=9$, $G=12$, $M=2$, $B=24$, $V_H=105$.
The word AC uses positions $(0,2)$, $(1,2)$, $(0,2)$, followed by padding.
It selects two active symbol clusters of size 3, one padding cluster of size 2,
and nine embedding clusters of size 2, for a total of 26. Thus length at least
2 is YES, equivalent to independent-set size at least 26. A length-3 word would
have to equal each of the first two length-3 strings, ABC and BAC, which differ.
Thus length at least 3 is NO, equivalent to independent-set size at least 27.
*Repeated-symbol example.* ABAC and BACA give $A=3$, $L=4$, $k=2$, $T=8$,
$G=12$, $M=2$, $B=24$, $V_H=124$. BAC embeds at positions $(1,2,3)$ in
ABAC and $(0,1,2)$ in BACA. It selects three active symbol clusters of size 3,
one padding symbol cluster of size 2, and eight embedding clusters of size 2,
for 27 vertices. Length 4 is impossible because the two length-4 strings differ.
Constructor scriptimport functools
import itertools
import json
from collections import Counter
from pathlib import Path
import sympy as sp
COUNTS = Counter()
def reduce(strings, alphabet_size):
L = min(map(len, strings), default=0)
occurring_symbols = sorted({a for s in strings for a in s})
choices = []
cursor = 0
for kind, p, r, values in (
[('X', p, None, [*occurring_symbols, None]) for p in range(L)]
+ [('Y', p, r, [*range(len(s)), None]) for r, s in enumerate(strings) for p in range(L)]
):
for value in values:
size = 3 if kind == 'X' and value is not None else 2
choices.append({'group': [kind, p] if r is None else [kind, r, p],
'value': value, 'clone_range': [cursor, cursor + size]})
cursor += size
edges = []
logical_edges = []
for i, a in enumerate(choices):
for j in range(i+1, len(choices)):
b = choices[j]
ga, gb = a['group'], b['group']
va, vb = a['value'], b['value']
conflict = ga == gb
if ga != gb and ga[0] == gb[0] == 'X':
conflict = va is None and vb is not None
elif ga != gb and ga[0] == gb[0] == 'Y' and ga[1] == gb[1]:
conflict = vb is not None and (va is None or va >= vb)
elif ga[0] == 'X' and gb[0] == 'Y' and ga[1] == gb[2]:
conflict = va != (None if vb is None else strings[gb[1]][vb])
if conflict:
logical_edges.append([i,j])
edges.extend([u,v] for u in range(*a['clone_range']) for v in range(*b['clone_range']))
k, T = len(strings), sum(map(len, strings))
return dict(strings=strings, alphabet_size=alphabet_size, A=len(occurring_symbols), occurring_symbols=occurring_symbols, L=L, k=k, T=T,
G=L*(k+1), M=2, B=2*L*(k+1), vertex_count=cursor,
choices=choices, logical_edges=logical_edges, edges=sorted(edges))
def oracle(strings):
if not strings:
return {()}
shortest = min(strings, key=len)
candidates = {tuple(shortest[j] for j in range(len(shortest)) if mask & (1<<j))
for mask in range(1<<len(shortest))}
def is_subsequence(word, string):
i = 0
for c in string:
if i < len(word) and c == word[i]:
i += 1
return i == len(word)
return {w for w in candidates if all(is_subsequence(w,s) for s in strings)}
def solve_logical(graph):
weights = [b-a for a,b in (c['clone_range'] for c in graph['choices'])]
neighbours = [0]*len(weights)
for a,b in graph['logical_edges']:
neighbours[a] |= 1<<b
neighbours[b] |= 1<<a
@functools.lru_cache(None)
def search(mask):
if not mask:
return 0, 0
choices = [i for i in range(len(weights)) if mask & (1<<i)]
v = max(choices, key=lambda i: (neighbours[i] & mask).bit_count())
tail = mask & ~(1<<v)
excluded = search(tail)
included = search(tail & ~neighbours[v])
included = (included[0]+weights[v], included[1] | (1<<v))
return max(excluded, included)
return search((1<<len(weights))-1)
def decode(graph, selected):
if any(selected & (1<<a) and selected & (1<<b) for a,b in graph['logical_edges']):
raise ValueError('conflicting choices')
by_group = {}
for i,c in enumerate(graph['choices']):
if selected & (1<<i):
key = tuple(c['group'])
if key in by_group:
raise ValueError('multiple choices')
by_group[key] = c['value']
all_groups = {tuple(c['group']) for c in graph['choices']}
if by_group.keys() != all_groups:
raise ValueError('missing group')
padded = [by_group[('X',p)] for p in range(graph['L'])]
return tuple(v for v in padded if v is not None)
def full_witnesses(graph):
groups = {}
for i,c in enumerate(graph['choices']):
groups.setdefault(tuple(c['group']), []).append(i)
adjacency = [0]*len(graph['choices'])
for i,j in graph['logical_edges']:
adjacency[i] |= 1<<j
adjacency[j] |= 1<<i
def visit(rows, selected):
if not rows:
yield selected
else:
for i in rows[0]:
if not selected & adjacency[i]:
yield from visit(rows[1:], selected | (1<<i))
yield from visit(list(groups.values()), 0)
def check(strings, A=2, exhaustive_witnesses=True):
graph = reduce(strings,A)
valid = oracle(strings)
optimum = max(map(len,valid))
V = graph['L']*(3*graph['A']+2+2*(graph['T']+graph['k']))
assert graph['vertex_count'] == V
assert len(graph['edges']) <= V*V
COUNTS['overhead'] += 2
weight, solution = solve_logical(graph)
assert weight == graph['B']+optimum
word = decode(graph, solution)
assert word in valid and len(word) == optimum
COUNTS['optimal_equivalence'] += 2
witnesses = list(full_witnesses(graph)) if exhaustive_witnesses else [solution]
represented = set()
for selected in witnesses:
word = decode(graph,selected)
assert word in valid
represented.add(word)
expanded = {v for i,c in enumerate(graph['choices']) if selected & (1<<i)
for v in range(*c['clone_range'])}
assert not any(a in expanded and b in expanded for a,b in graph['edges'])
assert len(expanded) == graph['B'] + len(word)
COUNTS['extraction_and_expansion'] += 3
if exhaustive_witnesses:
assert represented == valid
COUNTS['all_forward_words'] += len(valid)
for a,b in graph['edges']:
assert 0 <= a < b < V
COUNTS['structure'] += 1
if graph['G']:
try:
decode(graph,0)
raise AssertionError('accepted missing groups')
except ValueError:
pass
COUNTS['rejected_witnesses'] += 1
return graph
L,A,T,k = sp.symbols('L A T k')
assert sp.expand(L*(3*A+2) + L*(T+k)*2 - L*(3*A+2+2*(T+k))) == 0
assert sp.expand(2*(L*(k+1))+sp.Symbol('q') - (2*L*(k+1)+sp.Symbol('q'))) == 0
COUNTS['symbolic'] += 2
exports = []
cases = 0
for k in range(6):
lengths_list = itertools.product(range(6), repeat=k)
for lengths in lengths_list:
total = sum(lengths)
if total > 5:
continue
for symbols in itertools.product(range(2), repeat=total):
cursor = 0
strings = []
for length in lengths:
strings.append(list(symbols[cursor:cursor+length]))
cursor += length
graph = check(strings)
cases += 1
if graph['L'] and len(exports)<120:
exports.append(graph)
for strings,A,expected,B,V in [
([[0,1,2],[1,0,2],[0,1,2]],3,2,24,105),
([[0,1,0,2],[1,0,2,0]],3,3,24,124),
]:
graph=check(strings,A)
assert max(map(len,oracle(strings)))==expected
assert graph['B']==B and graph['vertex_count']==V
weight,_=solve_logical(graph)
assert weight>=B+expected and weight<B+expected+1
COUNTS['worked_yes_no_examples']+=4
for strings in [[[0]], [[7, 99], [99, 7]], [[], [999999999]]]:
check(strings, 2**64 - 1)
COUNTS['sparse_declared_alphabet'] += 1
Path(__file__).with_name('constructor-reductions.json').write_text(json.dumps(exports))
result={'verdict':'VERIFIED','exhaustive_cases':cases,'checks':dict(COUNTS),'total_checks':sum(COUNTS.values())}
Path(__file__).with_name('constructor-result.json').write_text(json.dumps(result,indent=2))
print(json.dumps(result,indent=2))Fresh-context adversary script"""Independent adversarial audit derived exclusively from proof.typ."""
from collections import Counter
from functools import lru_cache
from itertools import combinations, product
import json
from pathlib import Path
from hypothesis import given, seed, settings, strategies as st, HealthCheck
ROOT = Path(__file__).parent
COUNTS = Counter()
SEED = 739104
def lcs_oracle(strings):
"""Enumerate index subsets of the shortest string, independent of graphs."""
if not strings:
return {()}
shortest = min(strings, key=len)
words = {tuple(shortest[i] for i in inds)
for size in range(len(shortest) + 1)
for inds in combinations(range(len(shortest)), size)}
return {w for w in words if all(is_subsequence(w, s) for s in strings)}
def is_subsequence(word, string):
it = iter(string)
return all(any(a == b for b in it) for a in word)
def reduce(strings, alphabet_size):
strings = tuple(tuple(s) for s in strings)
if alphabet_size < 0 or any(a < 0 or a >= alphabet_size for s in strings for a in s):
raise ValueError("invalid alphabet")
k, T = len(strings), sum(map(len, strings))
symbols = sorted({a for s in strings for a in s})
L = min(map(len, strings), default=0)
M, G = 2, L * (k + 1)
choices, groups = [], []
cursor = 0
for group, values in (
[(('X', p), [*symbols, None]) for p in range(L)]
+ [(('Y', r, p), [*range(len(s)), None])
for r, s in enumerate(strings) for p in range(L)]
):
ids = []
for value in values:
size = M + (group[0] == 'X' and value is not None)
ids.append(len(choices))
choices.append({'group': list(group), 'value': value,
'clone_range': [cursor, cursor + size]})
cursor += size
groups.append(ids)
def conflict(c, d):
g, h, a, b = c['group'], d['group'], c['value'], d['value']
if g == h:
return True
if g[0] == h[0] == 'X':
return (a is None and b is not None) if g[1] < h[1] else (b is None and a is not None)
if g[0] == 'X' and h[0] == 'Y':
if g[1] != h[2]:
return False
return (a is None) != (b is None) or (a is not None and strings[h[1]][b] != a)
if g[0] == 'Y' and h[0] == 'X':
return conflict(d, c)
if g[1] != h[1]:
return False
if g[2] > h[2]:
return conflict(d, c)
return (a is None and b is not None) or (a is not None and b is not None and a >= b)
logical_edges = [(i, j) for i, j in combinations(range(len(choices)), 2)
if conflict(choices[i], choices[j])]
edges = sorted((u, v) for i, j in logical_edges
for u in range(*choices[i]['clone_range'])
for v in range(*choices[j]['clone_range']))
return dict(strings=[list(s) for s in strings], alphabet_size=alphabet_size,
occurring_symbols=symbols, A=len(symbols),
L=L, k=k, T=T, G=G, M=M, B=M*G, vertex_count=cursor,
choices=choices, groups=groups, logical_edges=logical_edges, edges=edges)
def exact_mis(weights, edges):
"""Exact deletion/contraction solver on arbitrary weighted graphs."""
n = len(weights)
if n > 24:
import numpy as np
from scipy.optimize import Bounds, LinearConstraint, milp
from scipy.sparse import coo_array
rows = np.repeat(np.arange(len(edges), dtype=np.int32), 2)
cols = np.array(edges, dtype=np.int32).ravel()
matrix = coo_array((np.ones(len(cols)), (rows, cols)), shape=(len(edges), n)).tocsc()
result = milp(-np.array(weights, dtype=float), integrality=np.ones(n), bounds=Bounds(0, 1),
constraints=LinearConstraint(matrix, -np.inf, 1),
options={'mip_rel_gap': 0.0, 'time_limit': 30.0})
assert result.success and result.status == 0, result.message
ids = [i for i, x in enumerate(result.x) if x > 0.5]
assert all(abs(x-round(x)) < 1e-7 for x in result.x)
assert not any(i in ids and j in ids for i, j in edges)
value = sum(weights[i] for i in ids)
assert abs(value+result.fun) < 1e-7
return value, ids
neighbours = [0] * n
for i, j in edges:
neighbours[i] |= 1 << j
neighbours[j] |= 1 << i
@lru_cache(None)
def solve(remaining):
if not remaining:
return 0, 0
ids = [i for i in range(n) if remaining & (1 << i)]
v = max(ids, key=lambda i: (neighbours[i] & remaining).bit_count())
without = remaining & ~(1 << v)
skip = solve(without)
value, picked = solve(without & ~neighbours[v])
take = value + weights[v], picked | (1 << v)
return max(skip, take, key=lambda x: x[0])
value, mask = solve((1 << n) - 1)
return value, [i for i in range(n) if mask & (1 << i)]
def expand_selected(graph, logical_ids):
return sorted(v for i in logical_ids for v in range(*graph['choices'][i]['clone_range']))
def extract(graph, selected):
"""Validate the actual expanded independent set before reading symbols."""
n = graph['vertex_count']
if len(set(selected)) != len(selected) or any(type(v) is not int or v < 0 or v >= n for v in selected):
raise ValueError('invalid selected vertices')
chosen = set(selected)
if any(u in chosen and v in chosen for u, v in graph['edges']):
raise ValueError('edge selected')
by_group = {}
for choice in graph['choices']:
cluster = set(range(*choice['clone_range']))
used = chosen & cluster
if used:
if used != cluster:
raise ValueError('partial cluster')
group = tuple(choice['group'])
if group in by_group:
raise ValueError('multiple choices')
by_group[group] = choice['value']
if len(by_group) != graph['G']:
raise ValueError('missing group')
padded = tuple(by_group[('X', p)] for p in range(graph['L']))
seen_padding = False
for a in padded:
if a is None:
seen_padding = True
elif seen_padding:
raise AssertionError('graph allowed non-suffix padding')
word = tuple(a for a in padded if a is not None)
if not all(is_subsequence(word, s) for s in graph['strings']):
raise AssertionError('graph allowed invalid subsequence')
return padded
def encode_word(graph, word):
choices = graph['choices']
mapping = {(tuple(c['group']), c['value']): i for i, c in enumerate(choices)}
ids = [mapping[(('X', p), word[p] if p < len(word) else None)] for p in range(graph['L'])]
for r, s in enumerate(graph['strings']):
cursor = 0
for p in range(graph['L']):
if p < len(word):
while s[cursor] != word[p]:
cursor += 1
value = cursor
cursor += 1
else:
value = None
ids.append(mapping[(('Y', r, p), value)])
return expand_selected(graph, ids)
def check(graph, expanded_optimum=False):
words = lcs_oracle(graph['strings'])
source_optimum = max(map(len, words))
expected_vertices = graph['L'] * (3*len({a for s in graph['strings'] for a in s})+2
+ 2*(graph['T']+graph['k']))
assert graph['A'] <= graph['T']
for group in graph['groups']:
domain = [graph['choices'][i]['value'] for i in group]
if graph['choices'][group[0]]['group'][0] == 'X':
assert domain == sorted({a for s in graph['strings'] for a in s}) + [None]
assert graph['vertex_count'] == expected_vertices
assert len(graph['edges']) <= graph['vertex_count']**2
assert len(set(graph['edges'])) == len(graph['edges'])
assert all(0 <= u < v < graph['vertex_count'] for u, v in graph['edges'])
COUNTS['size_and_edges'] += 1
weights = [c['clone_range'][1] - c['clone_range'][0] for c in graph['choices']]
target_optimum, ids = exact_mis(weights, graph['logical_edges'])
assert target_optimum == graph['B'] + source_optimum
optimal_vertices = expand_selected(graph, ids)
assert sum(a is not None for a in extract(graph, optimal_vertices)) == source_optimum
COUNTS['optimum_and_backward'] += 1
for word in words:
selected = encode_word(graph, word)
assert len(selected) == graph['B'] + len(word)
assert extract(graph, selected) == word + (None,)*(graph['L']-len(word))
COUNTS['forward_words'] += 1
# Verify the substitution used by the weighted solver against the real graph.
adjacency = [set() for _ in range(graph['vertex_count'])]
for u, v in graph['edges']:
adjacency[u].add(v)
adjacency[v].add(u)
for i, choice in enumerate(graph['choices']):
vertices = list(range(*choice['clone_range']))
expected = {v for a, b in graph['logical_edges'] if i in (a, b)
for v in range(*graph['choices'][b if a == i else a]['clone_range'])}
assert all(adjacency[v] == expected for v in vertices)
assert all(w not in adjacency[v] for v in vertices for w in vertices)
COUNTS['expanded_clone_equivalence'] += 1
if expanded_optimum:
actual, vertices = exact_mis([1]*graph['vertex_count'], graph['edges'])
assert actual == target_optimum
assert sum(a is not None for a in extract(graph, vertices)) == source_optimum
COUNTS['expanded_exact_optima'] += 1
return source_optimum, target_optimum
def malformed_checks(graph):
if not graph['G']:
bad = [[0], [-1], [None], [0, 0]]
else:
full = encode_word(graph, ())
first_padding = next(c for c in graph['choices'] if c['value'] is None)
cluster = set(range(*first_padding['clone_range']))
bad = [full[1:], [v for v in full if v not in cluster], full + [graph['vertex_count']],
full + [full[0]], full + [-1], full + [None]]
if graph['alphabet_size']:
active = next(c for c in graph['choices'] if c['group'][0] == 'X' and c['value'] is not None)
bad.append(full + list(range(*active['clone_range'])))
# Activate a symbol while keeping its embedding groups padded.
bad.append([v for v in full if v not in cluster] + list(range(*active['clone_range'])))
if graph['L'] > 1 and graph['alphabet_size']:
last_active = next(c for c in graph['choices'] if c['group'] == ['X', graph['L']-1]
and c['value'] == graph['occurring_symbols'][0])
last_padding = next(c for c in graph['choices'] if c['group'] == ['X', graph['L']-1] and c['value'] is None)
bad.append([v for v in full if v not in range(*last_padding['clone_range'])]
+ list(range(*last_active['clone_range'])))
for selected in bad:
try:
extract(graph, selected)
except (ValueError, TypeError):
COUNTS['malformed_rejected'] += 1
else:
raise AssertionError(('malformed accepted', graph['strings'], selected))
def compositions(total, k):
if k == 0:
if total == 0:
yield ()
return
for head in range(total + 1):
for tail in compositions(total-head, k-1):
yield (head,) + tail
def exhaustive_families():
for k in range(6):
for total in range(6):
for lengths in compositions(total, k):
for bits in product(range(2), repeat=total):
cursor, strings = 0, []
for length in lengths:
strings.append(bits[cursor:cursor+length])
cursor += length
yield tuple(strings)
def complete_encoding_checks(graph):
"""Enumerate all saturated sets, including every pattern of omitted groups."""
source_optimum = max(map(len, lcs_oracle(graph['strings'])))
for assignment in product(*[[-1, *group] for group in graph['groups']]):
ids = [i for i in assignment if i >= 0]
selected = expand_selected(graph, ids)
logical_set = set(ids)
if any(a in logical_set and b in logical_set for a, b in graph['logical_edges']):
continue
picked = {tuple(graph['choices'][i]['group']): graph['choices'][i]['value'] for i in ids}
missing_x = graph['L'] - sum(group[0] == 'X' for group in picked)
missing_y = graph['L']*graph['k'] - sum(group[0] == 'Y' for group in picked)
active = sum(group[0] == 'X' and value is not None for group, value in picked.items())
retained = [picked[('X', p)] for p in range(graph['L'])
if ('X', p) in picked and picked[('X', p)] is not None
and all(('Y', r, p) in picked for r in range(graph['k']))]
assert all(is_subsequence(retained, s) for s in graph['strings'])
assert active <= source_optimum + missing_y
assert len(selected) <= graph['B'] + source_optimum - 2*missing_x - missing_y
COUNTS['saturated_missing_group_bound'] += 1
if missing_x or missing_y:
try:
extract(graph, selected)
except ValueError:
COUNTS['incomplete_independent_sets_rejected'] += 1
else:
raise AssertionError('incomplete independent set accepted')
continue
word = tuple(a for a in extract(graph, selected) if a is not None)
assert len(selected) == graph['B'] + len(word)
assert word in lcs_oracle(graph['strings'])
COUNTS['complete_backward_encodings'] += 1
@seed(SEED)
@settings(max_examples=180, deadline=None, database=None,
suppress_health_check=[HealthCheck.too_slow])
@given(st.lists(st.lists(st.integers(0, 2), max_size=4), max_size=4))
def arbitrary_families(strings):
graph = reduce(strings, 3)
check(graph)
malformed_checks(graph)
COUNTS['hypothesis_arbitrary'] += 1
@st.composite
def shared_word_families(draw):
alphabet = draw(st.integers(1, 4))
word = draw(st.lists(st.integers(0, alphabet-1), max_size=3))
k = draw(st.integers(1, 4))
strings = []
for _ in range(k):
s = []
for a in word:
s += draw(st.lists(st.integers(0, alphabet-1), max_size=1))
s.append(a)
s += draw(st.lists(st.integers(0, alphabet-1), max_size=1))
strings.append(s)
return alphabet, word, strings
@seed(SEED + 1)
@settings(max_examples=160, deadline=None, database=None,
suppress_health_check=[HealthCheck.too_slow])
@given(shared_word_families())
def known_embedding_families(case):
alphabet, word, strings = case
graph = reduce(strings, alphabet)
source, target = check(graph)
assert source >= len(word)
assert target >= graph['B'] + len(word)
assert extract(graph, encode_word(graph, word)) == tuple(word) + (None,)*(graph['L']-len(word))
COUNTS['hypothesis_shared_word'] += 1
@st.composite
def sparse_original_labels(draw):
labels = draw(st.lists(st.integers(17, 2**63-1), min_size=1, max_size=4, unique=True))
ranked = draw(st.lists(st.lists(st.integers(0, len(labels)-1), max_size=4), max_size=4))
strings = [[labels[i] for i in s] for s in ranked]
alphabet = max(labels) + 1 + draw(st.integers(10**9, 10**12))
return strings, alphabet
@seed(SEED + 2)
@settings(max_examples=120, deadline=None, database=None,
suppress_health_check=[HealthCheck.too_slow])
@given(sparse_original_labels())
def sparse_alphabet_families(case):
strings, alphabet = case
graph = reduce(strings, alphabet)
check(graph)
malformed_checks(graph)
larger = reduce(strings, alphabet*10**20)
assert all(graph[key] == larger[key] for key in ('choices', 'logical_edges', 'edges', 'vertex_count', 'A'))
for word in lcs_oracle(strings):
assert extract(graph, encode_word(graph, word)) == word + (None,)*(graph['L']-len(word))
COUNTS['sparse_alphabet_invariance'] += 1
COUNTS['hypothesis_sparse_labels'] += 1
def main():
exports = []
unique_exports = set()
for strings in exhaustive_families():
graph = reduce(strings, 2)
check(graph, expanded_optimum=0 < graph['vertex_count'] <= 24)
malformed_checks(graph)
COUNTS['exhaustive_families'] += 1
if graph['G'] and len(graph['choices']) <= 15:
complete_encoding_checks(graph)
if graph['G'] and len(exports) < 160:
key = tuple(strings)
if key not in unique_exports:
exports.append(graph)
unique_exports.add(key)
if COUNTS['exhaustive_families'] % 1000 == 0:
print('exhaustive families:', COUNTS['exhaustive_families'], flush=True)
(ROOT/'adversary-reductions.json').write_text(json.dumps(exports, separators=(',', ':')))
print('exhaustive complete; exports ready', flush=True)
for strings, alphabet in [((), 0), (((),), 0), (((), ()), 0), (((0,),), 1), (((0, 0), (0,)), 3)]:
graph = reduce(strings, alphabet)
check(graph, expanded_optimum=graph['vertex_count'] <= 24)
malformed_checks(graph)
COUNTS['extra_boundary_families'] += 1
gap_graph = reduce(((0, 0, 0),), 1)
check(gap_graph)
complete_encoding_checks(gap_graph)
COUNTS['all_pairs_gap_case'] += 1
for strings, alphabet in [((), 10**100), (((), ()), 10**100),
(((17,), (17,)), 2**63),
(((2**63-2, 17, 2**63-2), (17, 2**63-2, 2**63-2)), 2**63),
(((10**80-1, 3), (3, 10**80-1)), 10**100)]:
graph = reduce(strings, alphabet)
check(graph)
malformed_checks(graph)
enlarged = reduce(strings, alphabet*10**100)
assert graph['choices'] == enlarged['choices'] and graph['edges'] == enlarged['edges']
exports.append(graph)
COUNTS['sparse_alphabet_invariance'] += 1
COUNTS['extra_sparse_families'] += 1
for strings, alphabet in [(((0,),), 0), (((-1,),), 2), (((2,),), 2), ((), -1)]:
try:
reduce(strings, alphabet)
except ValueError:
COUNTS['invalid_inputs_rejected'] += 1
else:
raise AssertionError('invalid alphabet accepted')
examples = []
for strings, word, wanted in [(((0, 1, 2), (1, 0, 2), (0, 1, 2)), (0, 2), (3, 3, 9, 12, 2, 24, 105, 2, 26)),
(((0, 1, 0, 2), (1, 0, 2, 0)), (1, 0, 2), (4, 2, 8, 12, 2, 24, 124, 3, 27))]:
graph = reduce(strings, 3)
source, target = check(graph)
assert tuple(graph[key] for key in ('L', 'k', 'T', 'G', 'M', 'B', 'vertex_count')) + (source, target) == wanted
selected = encode_word(graph, word)
assert len(selected) == target and extract(graph, selected) == word + (None,)*(graph['L']-len(word))
examples.append({'strings': graph['strings'], 'word': word, 'source_optimum': source,
'target_optimum': target, 'vertices': graph['vertex_count'], 'edges': len(graph['edges'])})
COUNTS['worked_examples'] += 1
arbitrary_families()
print('arbitrary Hypothesis strategy complete', flush=True)
known_embedding_families()
sparse_alphabet_families()
constructor_path = ROOT/'constructor-reductions.json'
if constructor_path.exists():
for expected in json.loads(constructor_path.read_text()):
actual = reduce(expected['strings'], expected['alphabet_size'])
for key in ('A', 'occurring_symbols', 'L', 'k', 'T', 'G', 'M', 'B', 'vertex_count', 'choices'):
assert actual[key] == expected[key], (key, expected['strings'])
for key in ('logical_edges', 'edges'):
assert [list(edge) for edge in actual[key]] == expected[key], (key, expected['strings'])
COUNTS['constructor_cross_comparisons'] += 1
assert len(exports) >= 100
validation_names = ('size_and_edges', 'optimum_and_backward', 'forward_words',
'expanded_clone_equivalence', 'malformed_rejected', 'expanded_exact_optima',
'saturated_missing_group_bound', 'incomplete_independent_sets_rejected',
'complete_backward_encodings', 'invalid_inputs_rejected', 'worked_examples',
'constructor_cross_comparisons', 'sparse_alphabet_invariance')
validations = sum(COUNTS[name] for name in validation_names)
assert COUNTS['optimum_and_backward'] >= 5000
(ROOT/'adversary-reductions.json').write_text(json.dumps(exports, separators=(',', ':')))
result = {'proof_correct': True, 'counts': dict(COUNTS), 'total_counted_checks': validations,
'count_definition': 'Counts validation groups, excluding case bookkeeping; each group checks a distinct failure mode, not an atomic assert count.',
'exhaustive_scope': 'all ordered binary string tuples with k in 0..5 and sum(lengths) in 0..5, including empty strings',
'hypothesis': {'seeds': [SEED, SEED+1, SEED+2], 'max_examples': [180, 160, 120], 'deadline': None,
'database': None, 'strategies': ['arbitrary ternary string families', 'alphabet-varying shared-word embeddings',
'sparse original integer labels with huge declared alphabets']},
'export_count': len(exports), 'examples': examples,
'limitations': ['Finite computational checks supplement the mathematical audit; do not prove all lengths.',
'No repository or parent implementation code was read.']}
(ROOT/'adversary-result.json').write_text(json.dumps(result, indent=2)+'\n')
print(json.dumps(result, indent=2))
if __name__ == '__main__':
main()Rust CLI graph and decoder cross-checkimport itertools, json, subprocess
from pathlib import Path
base = Path(__file__).parent
pred = "/Users/xiweipan/Codes/problem-reductions-worktrees/lcs-polynomial-mis/target/debug/pred"
def run(*args):
result = subprocess.run([pred, *args], capture_output=True, text=True, check=True)
return json.loads(result.stdout) if result.stdout.strip() else None
paths = run("path", "LongestCommonSubsequence", "MaximumIndependentSet/SimpleGraph/One", "--limit", "all", "--json")
route = next(p for p in paths["paths"] if len(p["path"]) == 1)
route_file = base / "rust-route.json"
route_file.write_text(json.dumps(route))
exports = json.loads((base / "constructor-reductions.json").read_text()) + json.loads((base / "adversary-reductions.json").read_text())
checked = skipped = rejected = 0
seen = set()
for graph in exports:
key = json.dumps([graph["strings"], graph["alphabet_size"]])
if key in seen: continue
seen.add(key)
if graph["alphabet_size"] > 2**64-1:
skipped += 1; continue
source = base / "rust-source.json"
bundle = base / "rust-bundle.json"
source.write_text(json.dumps({"type":"LongestCommonSubsequence", "variant":{}, "data":{"alphabet_size":graph["alphabet_size"],"strings":graph["strings"]}}))
run("reduce", str(source), "--via", str(route_file), "-o", str(bundle))
actual = json.loads(bundle.read_text())["target"]["data"]["graph"]
assert actual["num_vertices"] == graph["vertex_count"], key
assert sorted(map(tuple, actual["edges"])) == sorted(map(tuple, graph["edges"])), key
strings = graph["strings"]
shortest = min(strings, key=len, default=[])
def subseq(word, string):
it = iter(string)
return all(any(x == c for x in it) for c in word)
words = {tuple(shortest[i] for i in range(len(shortest)) if mask & (1<<i)) for mask in range(1<<len(shortest))}
word = max((w for w in words if all(subseq(w,s) for s in strings)), key=lambda w:(len(w),w))
padded = list(word)+[None]*(graph["L"]-len(word))
assignments = {("X", p): v for p,v in enumerate(padded)}
for r, string in enumerate(strings):
cursor = 0
for p,v in enumerate(padded):
if v is None: pos = None
else:
pos = next(j for j in range(cursor,len(string)) if string[j] == v)
cursor = pos + 1
assignments[("Y",r,p)] = pos
selected = [False]*graph["vertex_count"]
for choice in graph["choices"]:
if assignments[tuple(choice["group"])] == choice["value"]:
a,b = choice["clone_range"]
selected[a:b] = [True]*(b-a)
recovered = run("extract",str(bundle),"--config",json.dumps(selected),"--json")
assert recovered["solution"] == padded, key
assert recovered["evaluation"] == f"Max({len(word)})", key
assert recovered["intermediate"]["evaluation"] == f"Max({graph['B']+len(word)})", key
# Removing a selected cluster preserves independence but makes a group missing.
# Check both symbol and embedding omissions, and an incomplete clone cluster.
chosen = [c for c in graph["choices"] if selected[c["clone_range"][0]]]
if chosen:
for choice in [chosen[0], chosen[-1]]:
invalid = selected.copy()
a,b = choice["clone_range"]
invalid[a:b] = [False]*(b-a)
result = subprocess.run([pred,"extract",str(bundle),"--config",json.dumps(invalid),"--json"], capture_output=True, text=True)
assert result.returncode != 0 and "panicked" not in result.stderr, key
rejected += 1
invalid = selected.copy()
invalid[chosen[0]["clone_range"][0]] = False
result = subprocess.run([pred,"extract",str(bundle),"--config",json.dumps(invalid),"--json"], capture_output=True, text=True)
assert result.returncode != 0 and "panicked" not in result.stderr, key
rejected += 1
checked += 1
result = {"verdict":"VERIFIED", "unique_rust_graphs_and_decoders_checked":checked,"malformed_independent_sets_rejected":rejected,"out_of_usize_domain_python_cases_skipped":skipped}
(base / "rust-crosscheck-result.json").write_text(json.dumps(result, indent=2))
print(json.dumps(result)) |
Collaborator
Author
Agentic Review ReportReviewed commit Structural and semantic
QualitySeven focused rule tests passed, including the repeated-string bound, multi-string ordering, empty/disjoint cases, malformed/incomplete encodings, valid nonoptimal decoding, and maximum declared alphabet. Both changed CLI regressions passed. The source optimum is independently checked by brute force in the round-trip helper, but no nonempty target is now solved by Rust brute force in the persisted rule tests; see finding below. Feature testBuilt this checkout's
Evidence: Findings, severity sorted
No Critical findings. Full workspace/coverage/paper gates were not rerun during this review; focused checks passed, and no large-instance performance benchmark was performed. The intentional target encoding and parameter-schema change requires existing routes/bundles/witnesses to be regenerated. |
Collaborator
Author
|
Addressed the Important target-solver check in commit The final The rebuilt CLI also verifies the original KSatisfiability/K3→DecisionMVC/SimpleGraph/One→MVC/SimpleGraph/One→LCS→MIS/SimpleGraph/One path: Please kindly check the following items (PR #1193):
|
Collaborator
Author
Agentic Review Report — follow-upReviewed the complete The follow-up changes only this test; construction, extraction, metadata, and proof are unchanged. No outstanding findings from my review. The author reports the focused tests and broader gates passed except the already documented unchanged ignored macro doctest; I did not rerun compilation for this test-only follow-up. No new performance evidence was collected. The previously documented saved-route/bundle/witness regeneration requirement remains. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1193 +/- ##
========================================
Coverage 96.90% 96.91%
========================================
Files 1095 1095
Lines 145109 145265 +156
========================================
+ Hits 140621 140777 +156
Misses 4488 4488 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
isPANN
marked this pull request as draft
October 10, 2026 15:56
Collaborator
Author
Verification certificateVERIFIED mathematical research proposal: compact anchored LCS→MIS fallback. This is not implemented in the current PR, and does not replace its existing implementation certificate. No repository code was changed during this research. Concrete endpoints: The corpus evidence favors a bounded hybrid: count the legacy match tuples only up to a polynomial cap; retain the legacy graph below that cap and use the anchored construction otherwise. This preserves small graphs without permitting exponential graph allocation. This is a package recommendation, not a claim of globally optimal graph encoding. Let k be the number of strings, L the length of the first shortest string a (zero for no strings), T total length, and F the number of equal-symbol position pairs between a and all other strings. The anchored graph has exactly B = L(k+2)+F vertices and at most B² edges. Since F ≤ L(T−L), B is polynomial in input size. Its optimum is Lk+LCS. The proof includes missing embedding groups, skipped middle anchor positions, empty inputs, and sparse symbol labels. Let C = Σ_c Π_r frequency(c,s_r) (zero for no strings). Admit the legacy graph only when C ≤ B, counting common symbols with capped arithmetic before enumeration. The hybrid has V = min(C,B) ≤ B and E ≤ B²; the composable metadata is the polynomial upper bound, not an unconditional exact polynomial vertex count. Branch decoding/value offsets must be retained. Partial active-twin witnesses are rejected; every optimal target witness decodes correctly. For the existing MVC→LCS construction, with N vertices and M edges: L=N, k=M+1, F=2M(N−1), hence B=3N+3MN−2M. For the K3 path substitute N=2n+3m and M=n+6m. This gives quadratic vertex and quartic edge upper bounds in SAT counts, compared with the current PR's cubic vertex formula. To make this tight bound composable in Type resolution (current branch file evidence): Independent verification:
Corpus: Limits: no production Rust anchored/hybrid implementation, large-instance performance, specialized clique backend, or full-path end-to-end benchmark was tested. Bounded checks supplement the general proof and do not themselves prove it. No resource-impossible numeric boundary instance was allocated. Primary literature: Blum et al., matching-path conflict graphs explicitly describes exponential classic multi-string graph size and limits its graph-pruning experiments to two other variants. Bergougnoux et al., Section 4 provides a polynomial decision-LCS→IndependentSet construction designed for tree-model bounds; it is not a direct replacement for this optimization witness interface. The anchored encoding is a locally derived proposal, independently verified here, not attributed to those papers. Constructor check audit{
"verdict": "PASSED",
"counts": {
"symbolic": 4,
"overhead": 28416,
"structure": 18944,
"all_backward_witnesses": 33904,
"optimum_upper_bound": 146276,
"all_optimal_extractions": 10090,
"optimal_equivalence": 9472,
"all_forward_words": 10458,
"families": 9472,
"rejected_partial_twins": 112372,
"worked_yes_no": 5,
"boundary_optima": 2
},
"scope": "binary k<=5,total_length<=5; every independent witness and every maximum; all common words",
"example": {
"vertices": 21,
"edges": 31,
"optimum": 11
},
"limitations": [
"Mathematical proposal; no Rust replacement implemented",
"No resource-impossible numeric boundary allocated"
]
}Independent adversary audit{
"status": "PASS",
"counts": {
"exhaustive_families": 9472,
"maximum_witnesses": 18930,
"incomplete_optima": 3324,
"gapped_optima": 328,
"hypothesis_dense": 1500,
"hypothesis_sparse": 1500,
"nonoptimal_witnesses": 9332,
"solver_reference_graphs": 140
},
"examples": {
"incomplete_optimum": {
"strings": [
[
0
],
[
1
]
],
"mask": 3,
"decoded": [
null
]
},
"gapped_optimum": {
"strings": [
[
0,
1,
2
],
[
1,
0,
2
],
[
0,
1,
2
]
],
"mask": 697051,
"decoded": [
0,
2,
null
]
},
"worked_yes_no": {
"strings": [
[
0,
1,
2
],
[
1,
0,
2
],
[
0,
1,
2
]
],
"mask": 832227,
"source_optimum": 2,
"target_optimum": 11,
"yes_thresholds": [
2,
11
],
"no_thresholds": [
3,
12
]
}
},
"hypothesis_settings": {
"max_examples_per_strategy": 1500,
"deadline": null,
"derandomize": true,
"database": null
},
"elapsed_seconds": 2.301421880722046,
"cross_comparison": {
"status": "PASS",
"records": 9483,
"unique_families": 9480,
"exhaustive_unique_families": 9472,
"additional_unique_families": 8,
"repeated_boundary_records": 3,
"disagreements": 0,
"fields": [
"vertex_count",
"canonical_edges",
"source_optimum",
"target_optimum"
],
"reported_by": "parent independent verifier",
"parent_artifact": "/Users/xiweipan/.codex/scratchpads/lcs-polynomial-mis/research/cross-comparison.json"
}
}Cross-comparison audit{
"shared_records": 9475,
"additional_records": 8,
"disagreements": 0,
"unique_exhaustive_families": 9472,
"verdict": "VERIFIED"
}Corpus measurements{
"instances": 100,
"method_checks": 300,
"all_correct": true,
"jobs": 2,
"seconds": 18.651272957911715,
"methods": {
"old": {
"vertices": {
"min": 0,
"median": 11.0,
"max": 594,
"sum": 3202
},
"edges": {
"min": 0,
"median": 41.0,
"max": 169101,
"sum": 302830
},
"solve_seconds": {
"min": 0.0061757920775562525,
"median": 0.007906166953034699,
"max": 0.7823863329831511,
"sum": 2.0660012166481465
}
},
"current": {
"vertices": {
"min": 72,
"median": 218.0,
"max": 504,
"sum": 23532
},
"edges": {
"min": 711,
"median": 4408.0,
"max": 16128,
"sum": 540407
},
"solve_seconds": {
"min": 0.014425250003114343,
"median": 0.08572118752636015,
"max": 3.0068007498048246,
"sum": 24.777137586381286
}
},
"anchored": {
"vertices": {
"min": 14,
"median": 40.0,
"max": 114,
"sum": 4451
},
"edges": {
"min": 17,
"median": 97.0,
"max": 600,
"sum": 13207
},
"solve_seconds": {
"min": 0.0083578338380903,
"median": 0.009688333026133478,
"max": 0.03607670799829066,
"sum": 1.047078707255423
}
},
"hybrid": {
"vertices": {
"min": 0,
"median": 11.0,
"max": 114,
"sum": 2153
},
"edges": {
"min": 0,
"median": 41.0,
"max": 3659,
"sum": 27032
},
"solve_seconds": {
"min": 0.0061757920775562525,
"median": 0.007906166953034699,
"max": 0.03607670799829066,
"sum": 0.9171936728525907
}
}
},
"hybrid_branches": {
"old": 92,
"anchored": 8
},
"timing_scope": "Wall clock of identical pred solve - --solver ilp --json --timeout 30 calls on preconstructed graphs, including transport and startup. Current graph generated by Rust; old and proposed graphs generated independently in Python. Hybrid times reuse selected branch measurements and are not a production hybrid benchmark.",
"not_checked": [
"Production Rust anchored or hybrid implementation",
"Large-instance performance",
"Specialized maximum-clique solver backend"
]
}Typst theorem and proof#set page(width: 180mm, margin: 15mm)
#set text(size: 10pt)
= Anchored polynomial LCS to unweighted MIS: research proposal
*Type resolution.* Source `LongestCommonSubsequence::Value = Max<i64>`.
Target `MaximumIndependentSet<SimpleGraph, One>::Value = Max<One::Sum>`,
where `One::Sum = i64`. This is an optimization witness reduction.
*Theorem.* For $k$ input strings, select the first shortest string as anchor
$a$. Its length is $L$, with $L=0$ for no strings. Let $T$ be total input
length, and
$F = sum_(r != a) sum_(p=0)^(L-1) |{j : s_r[j]=s_a[p]}|$.
Then the construction has exactly
$V=L(k+2)+F$, at most $V^2$ edges, and
$alpha(H)=L k+"LCS"$.
Every maximum independent set decodes to an optimal source witness, including
optima that leave embedding groups empty. Since $F <= L(T-L)$, size is
polynomial even when the declared alphabet is large.
*Construction.*
1. There is one anchor group $X_p$ for each anchor position $p$. It has an
active choice consisting of two nonadjacent twin vertices, and a skip
choice consisting of one vertex. Join the skip vertex to both twins.
2. For every other input string $r$ and anchor position $p$, create a group
$Y_(r,p)$ with one vertex for every position $j$ with $s_r[j]=s_a[p]$ and
one skip vertex. Each such group is a clique.
3. Between $X_p$ and $Y_(r,p)$, join both active twins to the skip vertex,
and join the anchor skip vertex to every matching-position vertex.
4. Between embedding groups for the same string at $p<q$, join matching
position vertices $j,j'$ precisely when $j >= j'$. Skip vertices have
no edges between different slots. Check every slot pair, including
nonadjacent slots. There are no other edges.
5. Choose the first shortest string deterministically. Number anchor groups
first in increasing position order: active twins then skip. Then number
embedding groups by increasing original string index (excluding the
anchor) and increasing anchor position: increasing matching positions
then skip. This numbering is only for comparing independent scripts.
There are $G=L k$ groups. Unlike a padded output-position encoding, anchor
positions may be skipped in the middle. Decoder output is packed into
increasing anchor order and padded at the end.
*Forward correctness.* Any common subsequence of length $ell$ has strictly
increasing anchor positions. At each retained anchor position choose both
active twins and an increasing matching position in every other string.
At every discarded anchor position choose skip in every group. This is an
independent set of size $G+ell$. In particular a longest common subsequence
gives size $G+"LCS"$; the empty subsequence gives size $G$.
*Backward correctness.* For a maximum independent set, every nonempty active
anchor cluster includes both twins, since they have identical external
neighbours. At most one choice per group is selected. Let $d_X$ and $d_Y$
be the counts of empty anchor and embedding groups, and $q$ the count of
active anchor choices. Its cardinality is
$G-d_X-d_Y+q$.
Keep active anchor positions that have a selected matching-position vertex
in every other string. Each discarded active position has at least one
distinct missing embedding group, so at most $d_Y$ active positions are
discarded. Retained positions are strictly increasing in the anchor, match
its original symbols in every other string, and increase strictly within
each other string because all slot pairs are checked. They give a common
subsequence of length $ell >= q-d_Y$. Consequently
$G-d_X-d_Y+q <= G+"LCS"-d_X <= G+"LCS"$.
Forward correctness attains this upper bound. At any optimum, $d_X=0$ and
$q-d_Y="LCS"$; the decoded common subsequence has length at least LCS and
cannot exceed LCS, so it is optimal. Missing embedding groups are permitted
and decoded by the stated retention rule, not by inventing positions.
*Solution extraction.* Validate the target dimension and independence.
Reject a partially selected active twin cluster. Determine every selected
choice. Keep only complete active anchor clusters for which every other
string's embedding group selects a matching-position vertex. Read their
original symbols in increasing anchor position, then append `None` to length
$L$. A valid independent set may leave anchor or embedding groups empty;
this mapping still gives a valid, possibly nonoptimal common subsequence.
Every optimal target witness passes validation and decodes optimally.
No source-optimality assumption is made for nonoptimal target witnesses.
*Overhead derivation.* Anchor groups contribute $3L$ vertices. Embedding
groups contribute $L(k-1)+F$. Thus $V=L(k+2)+F$ exactly and $E<=V^2$.
Counting matching positions uses no declared-alphabet iteration. Construction
can scan choices and conflicts in $O(V^2+L T+k)$ time; validated decoding uses
$O(V+E)$ time. Empty input or any empty shortest string yields an empty graph
and a zero-length source witness. With one string, $F=0$ and $V=3L$.
*MVC-derived input.* Let the original unweighted simple graph have $N$
vertices and $M$ edges. The MVC to LCS construction places the base string
$(0,1,dots,N-1)$ first, followed by $M$ edge strings each of length $2N-2$.
For each edge string, summing matches against the unique base symbols gives
exactly $2N-2$. The base is shortest (tied first when $N=2$); if $N<=1$ there
are no simple-graph edges. Hence $L=N$, $k=M+1$, $F=2 M(N-1)$, and
$V=3N+3 M N-2 M$. This is quadratic in SAT counts after substitution
$N=2n+3m$, $M=n+6m$; edges have the upper bound $(3N+3 M N-2 M)^2$.
*YES and NO example.* Strings ABC, BAC, ABC have anchor ABC, $L=3$, $k=3$,
$F=6$, $G=9$, $V=21$. AC is common: use active anchor positions 0 and 2,
embedding positions 1 and 2 in BAC, and 0 and 2 in the other ABC. Fill skip
choices at anchor position 1. The independent set has size $9+2=11$.
Length at least 2 is YES, equivalent to independent-set size at least 11.
Length at least 3 is NO because length 3 forces ABC in the anchor and BAC
does not contain ABC. The theorem makes independent-set size at least 12 NO.
*Bounded tuple alternative.* Let $C=sum_c product_r "freq"(c,s_r)$ be the
legacy match-tuple count, with zero when there are no strings. Count C with
capped arithmetic at V, before enumerating tuples. Use the legacy graph only
if $C<=V$; otherwise use the anchored construction. The hybrid then has
$V_H=min(C,V)<=L(k+2)+F$ and $E_H<=(L(k+2)+F)^2$. Both construction branches
are polynomial-bounded because tuple enumeration is admitted only under this
polynomial cap. The legacy branch's optimum is LCS, and the anchored branch's
optimum is G+LCS; store the selected decoding mode. Exact vertex formulas
apply to the branches individually; the composable hybrid contract is the
polynomial upper bound, not an equality pretending the branch did not exist.
Constructor verifier"""Independent research constructor and checks; no package implementation edits."""
import itertools
import json
from collections import Counter
from functools import lru_cache
from pathlib import Path
def reduce(strings):
anchor = min(range(len(strings)), key=lambda i: len(strings[i]), default=None)
base = [] if anchor is None else strings[anchor]
choices = []
vertex_count = 0
groups = 0
def add_group(kind, p, r, values):
nonlocal vertex_count, groups
for value in values:
count = 2 if kind == 'X' and value is True else 1
choices.append({'kind': kind, 'p': p, 'r': r, 'value': value,
'group': groups, 'vertices': list(range(vertex_count, vertex_count + count))})
vertex_count += count
groups += 1
for p in range(len(base)):
add_group('X', p, anchor, [True, None])
for r, string in enumerate(strings):
if r != anchor:
for p, symbol in enumerate(base):
add_group('Y', p, r, [j for j, x in enumerate(string) if x == symbol] + [None])
edges = []
for a, b in itertools.combinations(choices, 2):
conflict = a['group'] == b['group']
if a['kind'] == 'X' and b['kind'] == 'Y' and a['p'] == b['p']:
conflict = (a['value'] is None) != (b['value'] is None)
if a['kind'] == b['kind'] == 'Y' and a['r'] == b['r'] and a['p'] < b['p']:
conflict = a['value'] is not None and b['value'] is not None and a['value'] >= b['value']
if conflict:
edges.extend((u, v) for u in a['vertices'] for v in b['vertices'])
return {'strings': strings, 'anchor': anchor, 'vertices': vertex_count,
'edges': edges, 'choices': choices, 'groups': groups}
def independent(graph, selected):
return len(selected) == graph['vertices'] and not any(selected[u] and selected[v] for u, v in graph['edges'])
def extract(graph, selected):
if not independent(graph, selected):
raise ValueError('invalid target witness')
active = set()
embedded = set()
for c in graph['choices']:
count = sum(selected[v] for v in c['vertices'])
if count and count != len(c['vertices']):
raise ValueError('partial active twins')
if count and c['value'] is not None:
if c['kind'] == 'X':
active.add(c['p'])
else:
embedded.add((c['r'], c['p']))
if graph['anchor'] is None:
return []
return [symbol for p, symbol in enumerate(graph['strings'][graph['anchor']])
if p in active and all((r, p) in embedded for r in range(len(graph['strings'])) if r != graph['anchor'])]
def is_subsequence(word, string):
cursor = iter(string)
return all(any(x == symbol for x in cursor) for symbol in word)
def words(strings):
anchor = min(strings, key=len, default=[])
return {tuple(anchor[i] for i in range(len(anchor)) if mask >> i & 1) for mask in range(1 << len(anchor))}
def source_optimum(strings):
return max((len(word) for word in words(strings) if all(is_subsequence(word, s) for s in strings)), default=0)
def forward(graph, word):
if graph['anchor'] is None:
assert not word
return []
strings = graph['strings']
anchor = graph['anchor']
assignments = {}
positions = []
cursor = 0
for symbol in word:
cursor = next(j for j in range(cursor, len(strings[anchor])) if strings[anchor][j] == symbol)
positions.append(cursor)
cursor += 1
active = set(positions)
for p in range(len(strings[anchor])):
assignments[('X', anchor, p)] = True if p in active else None
for r, string in enumerate(strings):
if r == anchor:
continue
cursor = 0
for p in range(len(strings[anchor])):
if p in active:
j = next(j for j in range(cursor, len(string)) if string[j] == strings[anchor][p])
assignments[('Y', r, p)] = j
cursor = j + 1
else:
assignments[('Y', r, p)] = None
selected = [False] * graph['vertices']
for c in graph['choices']:
if assignments[(c['kind'], c['r'], c['p'])] == c['value']:
for v in c['vertices']:
selected[v] = True
return selected
def all_independent_sets(graph):
adjacency = [0] * graph['vertices']
for u, v in graph['edges']:
adjacency[u] |= 1 << v
adjacency[v] |= 1 << u
def visit(candidates, selected):
if not candidates:
yield selected
return
bit = candidates & -candidates
v = bit.bit_length() - 1
yield from visit(candidates ^ bit, selected)
yield from visit((candidates ^ bit) & ~adjacency[v], selected | bit)
yield from visit((1 << graph['vertices']) - 1, 0)
def families():
for k in range(6):
for lengths in itertools.product(range(6), repeat=k):
total = sum(lengths)
if total > 5:
continue
for symbols in itertools.product(range(2), repeat=total):
cursor = 0
strings = []
for length in lengths:
strings.append(list(symbols[cursor:cursor + length]))
cursor += length
yield strings
def verify():
import sympy as sp
counts = Counter()
L, k, F, N, M, n, m = sp.symbols('L k F N M n m')
assert sp.expand(3*L + L*(k-1) + F - (L*(k+2)+F)) == 0
assert sp.expand((L*(k+2)+F).subs({L:N,k:M+1,F:2*M*(N-1)}) - (3*N+3*M*N-2*M)) == 0
assert sp.Poly((3*N+3*M*N-2*M).subs({N:2*n+3*m,M:n+6*m}),n,m).total_degree() == 2
assert sp.Poly(((3*N+3*M*N-2*M)**2).subs({N:2*n+3*m,M:n+6*m}),n,m).total_degree() == 4
counts['symbolic'] += 4
output = Path(__file__).parent
with (output / 'constructor-exports.jsonl').open('w') as exports:
for strings in families():
graph = reduce(strings)
length = min(map(len, strings), default=0)
anchor = graph['anchor']
matches = 0 if anchor is None else sum(sum(x == y for x in strings[anchor] for y in string)
for r, string in enumerate(strings) if r != anchor)
assert graph['vertices'] == length * (len(strings) + 2) + matches
assert matches <= length * (sum(map(len, strings)) - length)
assert len(graph['edges']) <= graph['vertices'] ** 2
counts['overhead'] += 3
assert len(graph['edges']) == len(set(map(tuple, graph['edges'])))
assert all(0 <= u < v < graph['vertices'] for u, v in graph['edges'])
counts['structure'] += 2
best = source_optimum(strings)
maximum = -1
witnesses = []
for mask in all_independent_sets(graph):
size = mask.bit_count()
selected = [bool(mask >> i & 1) for i in range(graph['vertices'])]
if size > maximum:
maximum = size
witnesses = [selected]
elif size == maximum:
witnesses.append(selected)
try:
word = extract(graph, selected)
except ValueError:
# The only invalid structure in an independent witness is partial twins.
assert any(len(c['vertices']) == 2 and sum(selected[v] for v in c['vertices']) == 1
for c in graph['choices'])
counts['rejected_partial_twins'] += 1
else:
assert all(is_subsequence(word, s) for s in strings)
counts['all_backward_witnesses'] += 1
assert size <= graph['groups'] + best
counts['optimum_upper_bound'] += 1
assert maximum == graph['groups'] + best
for selected in witnesses:
assert len(extract(graph, selected)) == best
counts['all_optimal_extractions'] += 1
counts['optimal_equivalence'] += 1
for word in words(strings):
if all(is_subsequence(word, s) for s in strings):
selected = forward(graph, word)
assert independent(graph, selected)
assert sum(selected) == graph['groups'] + len(word)
assert tuple(extract(graph, selected)) == word
counts['all_forward_words'] += 1
counts['families'] += 1
exports.write(json.dumps({'strings':strings,'vertices':graph['vertices'],'edges':graph['edges'],
'optimum': maximum}, separators=(',',':'))+'\n')
graph = reduce([[0,1,2],[1,0,2],[0,1,2]])
witness = forward(graph, [0,2])
assert graph['vertices'] == 21 and graph['groups'] == 9
assert independent(graph,witness) and sum(witness) == 11
assert source_optimum(graph['strings']) == 2
assert 11 < 12
counts['worked_yes_no'] += 5
# A maximum may omit an embedding group: AA and A have LCS=1.
graph = reduce([[0], [0,0]])
optimum = graph['groups'] + 1
incomplete_optima = 0
for mask in all_independent_sets(graph):
if mask.bit_count() == optimum:
selected=[bool(mask>>i&1) for i in range(graph['vertices'])]
assert len(extract(graph,selected)) == 1
counts['boundary_optima'] += 1
result={'verdict':'PASSED','counts':dict(counts),'scope':'binary k<=5,total_length<=5; every independent witness and every maximum; all common words',
'example':{'vertices':21,'edges':len(reduce([[0,1,2],[1,0,2],[0,1,2]])['edges']),'optimum':11},
'limitations':['Mathematical proposal; no Rust replacement implemented','No resource-impossible numeric boundary allocated']}
(output/'constructor-result.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result,indent=2),flush=True)
if __name__ == '__main__':
verify()Independent adversary verifier"""Proof-only adversary: does not import or read any repository implementation."""
from functools import lru_cache
from itertools import product
import json
from pathlib import Path
import random
import time
from hypothesis import given, settings, strategies as st
ROOT = Path(__file__).resolve().parent
COUNTS = {"exhaustive_families": 0, "maximum_witnesses": 0,
"incomplete_optima": 0, "gapped_optima": 0,
"hypothesis_dense": 0, "hypothesis_sparse": 0,
"nonoptimal_witnesses": 0, "solver_reference_graphs": 0}
EXAMPLES = {}
def reduce(strings):
anchor = min(range(len(strings)), key=lambda r: len(strings[r])) if strings else None
length = len(strings[anchor]) if anchor is not None else 0
vertices, xs, ys, edges = [], [], {}, set()
def vertex(label):
vertices.append(label)
return len(vertices) - 1
def join(u, v):
assert u != v
edges.add(tuple(sorted((u, v))))
for p in range(length):
x = tuple(vertex(("anchor", p, choice)) for choice in ("left", "right", "skip"))
xs.append(x)
join(x[0], x[2])
join(x[1], x[2])
for r, string in enumerate(strings):
if r == anchor:
continue
for p, symbol in enumerate(strings[anchor]):
matches = {j: vertex(("embedding", r, p, j))
for j, value in enumerate(string) if value == symbol}
skip = vertex(("embedding", r, p, "skip"))
choices = list(matches.values()) + [skip]
for i, u in enumerate(choices):
for v in choices[i + 1:]:
join(u, v)
join(xs[p][0], skip)
join(xs[p][1], skip)
for u in matches.values():
join(xs[p][2], u)
ys[r, p] = (matches, skip)
for p in range(length):
for q in range(p + 1, length):
for j, u in ys[r, p][0].items():
for jj, v in ys[r, q][0].items():
if j >= jj:
join(u, v)
return {"strings": strings, "anchor": anchor, "length": length,
"vertices": vertices, "xs": xs, "ys": ys, "edges": edges}
def exact_target(graph):
neighbors = [0] * len(graph["vertices"])
for u, v in graph["edges"]:
neighbors[u] |= 1 << v
neighbors[v] |= 1 << u
@lru_cache(None)
def solve(available):
if not available:
return 0, (0,)
choices = [v for v in range(len(neighbors)) if available >> v & 1]
v = max(choices, key=lambda u: (neighbors[u] & available).bit_count())
bit = 1 << v
no_size, no_sets = solve(available & ~bit)
yes_size, yes_sets = solve(available & ~bit & ~neighbors[v])
yes_size += 1
if no_size > yes_size:
return no_size, no_sets
included = tuple(mask | bit for mask in yes_sets)
if yes_size > no_size:
return yes_size, included
return no_size, no_sets + included
return solve((1 << len(neighbors)) - 1)
def subsequence(sequence, string):
cursor = iter(string)
return all(any(candidate == symbol for candidate in cursor) for symbol in sequence)
def source_optimum(strings):
if not strings:
return 0
shortest = min(strings, key=len)
subsequences = {tuple(shortest[i] for i in range(len(shortest)) if mask >> i & 1)
for mask in range(1 << len(shortest))}
return max(len(seq) for seq in subsequences if all(subsequence(seq, s) for s in strings))
def extract(graph, mask, dimension=None):
dimension = len(graph["vertices"]) if dimension is None else dimension
if dimension != len(graph["vertices"]) or mask < 0 or mask >> dimension:
raise ValueError("invalid target dimension")
selected = lambda v: bool(mask >> v & 1)
if any(selected(u) and selected(v) for u, v in graph["edges"]):
raise ValueError("dependent target witness")
retained = []
for p, (u, v, skip) in enumerate(graph["xs"]):
if selected(u) != selected(v):
raise ValueError("partial twins")
if selected(u) and all(any(selected(w) for w in matches.values())
for (r, slot), (matches, _) in graph["ys"].items()
if slot == p):
retained.append(p)
symbols = [graph["strings"][graph["anchor"]][p] for p in retained]
return symbols + [None] * (graph["length"] - len(symbols)), retained
def verify(strings, export=None):
graph = reduce(strings)
optimum = source_optimum(strings)
alpha, maxima = exact_target(graph)
length, k = graph["length"], len(strings)
total = sum(map(len, strings))
frequency = sum(sum(symbol == value for value in string)
for r, string in enumerate(strings) if r != graph["anchor"]
for symbol in strings[graph["anchor"]]) if strings else 0
assert len(graph["vertices"]) == length * (k + 2) + frequency
assert frequency <= length * (total - length)
assert alpha == length * k + optimum, (strings, alpha, optimum)
for mask in maxima:
decoded, positions = extract(graph, mask)
sequence = [value for value in decoded if value is not None]
assert len(decoded) == length
assert len(sequence) == optimum
assert all(subsequence(sequence, string) for string in strings)
assert all(mask >> skip & 1 or mask >> u & 1 or mask >> v & 1
for u, v, skip in graph["xs"])
COUNTS["maximum_witnesses"] += 1
incomplete = any(not (mask >> skip & 1) and not any(mask >> v & 1 for v in matches.values())
for matches, skip in graph["ys"].values())
gapped = any(q > p + 1 for p, q in zip(positions, positions[1:]))
if incomplete:
COUNTS["incomplete_optima"] += 1
EXAMPLES.setdefault("incomplete_optimum", {"strings": strings, "mask": mask, "decoded": decoded})
if gapped:
COUNTS["gapped_optima"] += 1
EXAMPLES.setdefault("gapped_optimum", {"strings": strings, "mask": mask, "decoded": decoded})
# Remove a whole selected group: accepted nonoptimal inputs must stay feasible.
if graph["xs"]:
removed = mask & ~sum(1 << v for v in graph["xs"][0])
lower, _ = extract(graph, removed)
assert all(subsequence([x for x in lower if x is not None], s) for s in strings)
COUNTS["nonoptimal_witnesses"] += 1
if graph["xs"]:
try:
extract(graph, 1 << graph["xs"][0][0])
except ValueError as error:
assert str(error) == "partial twins"
else:
raise AssertionError("partial twin was accepted")
for invalid, dimension in ((1 << len(graph["vertices"]), None), (0, len(graph["vertices"]) + 1)):
try:
extract(graph, invalid, dimension)
except ValueError:
pass
else:
raise AssertionError("invalid dimension was accepted")
if graph["edges"]:
u, v = next(iter(graph["edges"]))
try:
extract(graph, (1 << u) | (1 << v))
except ValueError:
pass
else:
raise AssertionError("dependent witness was accepted")
if export is not None:
export.write(json.dumps({"strings": strings, "anchor": graph["anchor"],
"n": len(graph["vertices"]), "edges": sorted(graph["edges"]),
"source_optimum": optimum, "target_optimum": alpha,
"maximum_witness_count": len(maxima)}, separators=(",", ":")) + "\n")
return graph, alpha, maxima
def compositions(total, count):
if count == 0:
if total == 0:
yield ()
elif count == 1:
yield (total,)
else:
for first in range(total + 1):
for tail in compositions(total - first, count - 1):
yield (first,) + tail
def exhaustive(export):
for k in range(6):
for total in range(6):
for lengths in compositions(total, k):
pools = [list(product((0, 1), repeat=n)) for n in lengths]
for family in product(*pools):
verify([list(s) for s in family], export)
COUNTS["exhaustive_families"] += 1
assert COUNTS["exhaustive_families"] == 9472
def verify_solver():
rng = random.Random(43117)
for n in range(7):
for _ in range(20):
edges = {(u, v) for u in range(n) for v in range(u + 1, n) if rng.randrange(2)}
feasible = [mask for mask in range(1 << n)
if all(not (mask >> u & 1 and mask >> v & 1) for u, v in edges)]
expected = max(map(int.bit_count, feasible))
actual, sets = exact_target({"vertices": [None] * n, "edges": edges})
assert actual == expected
assert set(sets) == {mask for mask in feasible if mask.bit_count() == expected}
COUNTS["solver_reference_graphs"] += 1
@st.composite
def dense_families(draw):
k = draw(st.integers(1, 5))
lengths = draw(st.lists(st.integers(1, 4), min_size=k, max_size=k).filter(lambda ns: sum(ns) <= 10))
return [draw(st.lists(st.integers(0, 1), min_size=n, max_size=n)) for n in lengths]
@st.composite
def sparse_families(draw):
symbols = draw(st.sampled_from(((0, 10**9), (3, 100_003, 999_999_937))))
k = draw(st.integers(0, 5))
lengths = draw(st.lists(st.integers(0, 4), min_size=k, max_size=k).filter(lambda ns: sum(ns) <= 10))
return [draw(st.lists(st.sampled_from(symbols), min_size=n, max_size=n)) for n in lengths]
@settings(max_examples=1500, deadline=None, derandomize=True, database=None)
@given(dense_families())
def test_dense(strings):
verify(strings)
COUNTS["hypothesis_dense"] += 1
@settings(max_examples=1500, deadline=None, derandomize=True, database=None)
@given(sparse_families())
def test_sparse(strings):
verify(strings)
COUNTS["hypothesis_sparse"] += 1
def worked_and_boundary(export):
worked = [[0, 1, 2], [1, 0, 2], [0, 1, 2]]
graph, alpha, _ = verify(worked, export)
assert len(graph["vertices"]) == 21 and alpha == 11
assert source_optimum(worked) >= 2 and alpha >= 11
assert source_optimum(worked) < 3 and alpha < 12
chosen = set(graph["xs"][0][:2] + (graph["xs"][1][2],) + graph["xs"][2][:2])
for r, positions in ((1, (1, 2)), (2, (0, 2))):
chosen.add(graph["ys"][r, 0][0][positions[0]])
chosen.add(graph["ys"][r, 1][1])
chosen.add(graph["ys"][r, 2][0][positions[1]])
mask = sum(1 << v for v in chosen)
assert mask.bit_count() == 11
assert extract(graph, mask)[0] == [0, 2, None]
EXAMPLES["worked_yes_no"] = {"strings": worked, "mask": mask,
"source_optimum": 2, "target_optimum": 11,
"yes_thresholds": [2, 11], "no_thresholds": [3, 12]}
cases = [[], [[]], [[], [0, 999999937]], [[999999937]],
[[1000000000, 3, 1000000000]], [[0], [1]],
[[0, 0], [1, 1], [2, 2]],
[[0, 1, 0], [0, 0, 1], [0, 1, 0]],
[[0, 1, 2, 3], [0, 2, 1, 3], [0, 1, 2, 3]],
[[3, 999999937], [999999937, 3]]]
for strings in cases:
verify(strings, export)
if __name__ == "__main__":
started = time.time()
verify_solver()
with (ROOT / "graph_exports.jsonl").open("w") as export:
exhaustive(export)
worked_and_boundary(export)
print("exhaustive and boundary complete", COUNTS, flush=True)
test_dense()
print("dense Hypothesis complete", COUNTS, flush=True)
test_sparse()
report = {"status": "PASS", "counts": COUNTS, "examples": EXAMPLES,
"hypothesis_settings": {"max_examples_per_strategy": 1500, "deadline": None,
"derandomize": True, "database": None},
"elapsed_seconds": time.time() - started}
(ROOT / "report.json").write_text(json.dumps(report, indent=2) + "\n")
print(json.dumps(report, indent=2))Structural cross-comparison"""Compare independently constructed graphs and optimal values."""
import json
from pathlib import Path
from anchor_constructor import reduce, source_optimum
root = Path(__file__).parent
parent = {}
for line in (root / 'constructor-exports.jsonl').read_text().splitlines():
record = json.loads(line)
key = json.dumps(record['strings'], separators=(',', ':'))
assert key not in parent
parent[key] = record
counts = {'shared_records': 0, 'additional_records': 0, 'disagreements': 0}
shared = set()
for line in (root / 'adversary/graph_exports.jsonl').read_text().splitlines():
independent = json.loads(line)
key = json.dumps(independent['strings'], separators=(',', ':'))
if key in parent:
graph = parent[key]
optimum = graph['optimum']
counts['shared_records'] += 1
shared.add(key)
else:
graph = reduce(independent['strings'])
optimum = graph['groups'] + source_optimum(independent['strings'])
counts['additional_records'] += 1
assert graph['vertices'] == independent['n'], key
assert sorted(map(tuple, graph['edges'])) == sorted(map(tuple, independent['edges'])), key
assert optimum == independent['target_optimum'], key
assert source_optimum(independent['strings']) == independent['source_optimum'], key
assert len(shared) == len(parent) == 9472
counts['unique_exhaustive_families'] = len(shared)
counts['verdict'] = 'VERIFIED'
(root / 'cross-comparison.json').write_text(json.dumps(counts, indent=2) + '\n')
print(json.dumps(counts, indent=2))
# Replace the preliminary formula-only study with actual measured graph sizes.
report = json.loads((root / 'corpus-comparison/report.json').read_text())
study = {
'instances': report['instances'],
'all_correct': report['all_correct'],
'anchored_formula': 'L*(k+2)+F',
'source': 'corpus-comparison/report.json; actual constructed graphs',
'methods': {name: {'vertices': data['vertices'], 'edges': data['edges']}
for name, data in report['methods'].items()},
'hybrid_branches': report['hybrid_branches'],
}
(root / 'size-study.json').write_text(json.dumps(study, indent=2) + '\n') |
isPANN
changed the title
Collaborator
Author
Agentic Review ReportFresh review of final head 69f5988, using Structural and semanticReviewed the complete PR diff and connected model, reduction, extraction, registry, test, and paper code. The eight changed files are needed for the capped hybrid, source parameter, exact incoming MVC relation, regressions, and theorem. No generated exports, unrelated changes, duplicate primitive endpoint, or missing registration/example found. Checked all five comment sources: PR discussion, inline comments, review bodies, review threads, and linked-issue context; there is no linked issue. Independently traced preprocessing and both encodings. Duplicate/containing-string removal and impossible-letter filtering preserve the feasible common words. Freezing the common-symbol set prevents a removed constraint from reintroducing an impossible letter. Tuple positions remain ordered coordinates of the original anchor; anchored positions use the filtered anchor, and both decoders pad to the original The anchored proof handles empty embedding groups: saturating twins gives size Checked QualityPersisted regressions cover the canonical tuple branch, redundant strings, cap boundaries, selection by vertices plus edges and tuple ties, empty/disjoint inputs, sparse maximum labels, original-input matching-pair metadata and deserialization, malformed/partial witnesses, and an optimal witness with a missing embedding group. Source optima are checked with real brute force; cheap target cases also use real brute force, with ILP retained for larger cases. The generic executable-parameter test covers the changed formulas. The new impossible-letter regression independently distinguishes 44 vertices from the earlier 49 and preserves the original output padding. Feature testUsed the already built actual worktree
Evidence: Findings, severity sortedNone. Compilation, full-workspace tests, coverage, and paper generation were coordinated by the author and were not rerun by this reviewer. No large-instance performance benchmark or memory-impossible overflow allocation was attempted. The intentional encoding/parameter-schema changes require old LCS→MIS routes, bundles, and witnesses to be regenerated; the previously reported ignored macro doctest failure is outside this diff. |
Collaborator
Author
Verification certificateVERIFIED final implemented compact LCS→MIS hybrid, head The final rule removes duplicate strings and strings containing the first shortest string, deletes anchor letters absent from another retained constraint, then removes newly redundant containing strings. The common-symbol set stays fixed, so pruning cannot reintroduce an unavailable letter; original-length padding is preserved. It caps tuple counting before Cartesian enumeration, and selects the smaller vertices-plus-edges graph among admitted tuples and the polynomial anchored encoding. Ties prefer tuples. A cheap lower bound skips a second construction when the tuple graph cannot lose. No solver is used in preprocessing or selection; no declared-alphabet scan occurs. Let L be the first shortest original string length, k the original string count, T total length, and F equal-symbol position pairs between the anchor and all other original strings. The registered bounds are V≤B=L(k+2)+F and E≤B², with F≤L(T−L). After preprocessing L', k', F' may shrink, with B'=L'(k'+2)+F'≤B. Admit tuples only if C'≤B'; the selected vertex count is either C' or B', never exceeding B. Selection may use additional vertices to save edges; it does not claim to minimize solver runtime. Tuple optimum equals LCS; anchored optimum equals L'*k'+LCS. The proof covers optima with missing embedding groups, nonadjacent slot crossings, sparse symbols, empty/single-string inputs, and twin saturation. Every optimal target witness decodes to an optimal original source witness. For MVC inputs with N vertices and M edges, F=2M(N−1) exactly, so B=3N+3MN−2M. On the requested K3SAT→DecisionMVC→MVC→LCS→MIS path, N=2n+3m and M=n+6m: V has a quadratic upper bound and E a quartic upper bound. Both relations are upper bounds, not unconditional exact graph counts, and neither field is unavailable. Actual CLI end-to-end verification for n=3,m=2 built 546 vertices/2,066 edges, solved the target optimally, recovered a satisfying assignment, and reevaluated it on the original source. Type-resolution gate: Independent mathematical checks: the foundation constructor enumerates all 9,472 ordered binary families with ≤5 strings and total length≤5, testing forward common words, all independent witnesses, optimum bounds and every optimal extraction. The final hybrid constructor also checks feasible-set preservation after pruning, target size bounds, and exact graph agreement for 9,488 shared exhaustive/targeted cases. Its source reference enumerates anchor subsequences; larger targets use real CLI ILP. The fresh adversary was given only the Typst proof, wrote independent construction/extraction and source/target checkers, and passed 12,495 hybrid checks (9,472 exhaustive, 1,500 dense Hypothesis, 1,500 sparse Hypothesis, and targeted families). It separately checked 9,495 forced anchored graphs, 9,583 optimal small anchored witness decodes, 122 anchored wins with admitted tuples, 756 graph-size ties, and 2,431 shortcut wins; 2,964 original-to-filtered anchor coordinate comparisons have identical canonical edges. Its graph solver uses maximum clique in the complement with coloring bounds, crosschecked against all-subset enumeration. CPython 3.12.14 and Hypothesis 6.168.5 were used via Actual Rust crosscomparison: all 9,488 graphs agree exactly on canonical edges and vertex counts. Rust source brute force, target brute force for ≤16 vertices (all optimal witnesses), and real ILP for larger targets checked 9,527 optimal decodings with zero disagreements. These are checks of the compiled production rule and decoder, independent of the parent prototype. Corpus:
Limits: bounded checks supplement the general proof; no resource-impossible numerical allocation, large-instance solver benchmark, or full SAT-path corpus sweep. This is a practical compact encoding, not a global optimality or solver-performance claim. Saved LCS→MIS routes/bundles/witnesses require regeneration after the schema/encoding change. Followed how-to-verify. Foundation audit{
"verdict": "PASSED",
"counts": {
"symbolic": 4,
"overhead": 28416,
"structure": 18944,
"all_backward_witnesses": 33904,
"optimum_upper_bound": 146276,
"all_optimal_extractions": 10090,
"optimal_equivalence": 9472,
"all_forward_words": 10458,
"families": 9472,
"rejected_partial_twins": 112372,
"worked_yes_no": 5,
"boundary_optima": 2
},
"scope": "binary k<=5,total_length<=5; every independent witness and every maximum; all common words",
"example": {
"vertices": 21,
"edges": 31,
"optimum": 11
},
"limitations": [
"Foundation proof/script unchanged; final hybrid Rust crosscomparison is reported separately",
"No resource-impossible numerical allocation"
]
}Final constructor audit{
"verdict": "VERIFIED",
"audit": {
"symbolic": 4,
"graph_cross_comparison": 9488,
"overhead_and_preprocessing": 47440,
"feasible_set_preservation": 10999,
"all_feasible_target_witnesses": 11246,
"optimum_equivalence": 9488,
"real_ilp_target_checks": 10
},
"disagreements": 0,
"limits": [
"No resource-impossible numeric allocation",
"Sparse large-alphabet source reference uses subsequence enumeration"
]
}Independent adversary audit{
"status": "PASS",
"counts": {
"full_feasible_set_checks": 12495,
"anchor_cap_exceeded": 66,
"checks": 12495,
"anchor": 188,
"forced_anchor_checks": 9495,
"anchor_position_isomorphisms": 2964,
"anchor_with_admitted_tuples": 122,
"exact_cap_boundary": 1,
"fast_tuple_wins": 2431,
"tuple": 2842,
"all_small_anchor_optima": 9583,
"brute_target_crosschecks": 9483,
"graph_size_ties": 756,
"absent_letter_reinsertion_regressions": 1,
"gapped_anchor": 1,
"hybrid_missing_group_optimum": 1,
"arbitrary_independent_decodes": 45,
"partial_twins_rejected": 60,
"small_all_optima": 4,
"missing_group_optima": 2,
"empty": 9465,
"zero_or_single_cases": 6,
"capped_count_regressions": 2,
"validation_regressions": 2,
"exhaustive": 9472,
"dense_hypothesis": 1500,
"sparse_hypothesis": 1500
},
"seconds": 2.5614277091808617,
"construction_source": "anchor-proof.typ",
"source_solver": "descending enumeration of anchor subsequences",
"target_solver": "maximum clique in complement with greedy coloring bounds",
"exports": [
"exhaustive.jsonl",
"targeted.jsonl"
]
}Independent adversary environment and derived seeds{
"command": "uv run --no-project --python /Users/xiweipan/Codes/pred-validation-corpus/.venv/bin/python --with hypothesis==6.168.5 verify.py",
"working_directory": "/Users/xiweipan/.codex/scratchpads/lcs-polynomial-mis/research/hybrid-adversary",
"python_version": "3.12.14 (main, Sep 1 2026, 14:09:38) [Clang 22.1.3 ]",
"requested_interpreter": "/Users/xiweipan/Codes/pred-validation-corpus/.venv/bin/python",
"base_prefix": "/Users/xiweipan/.local/share/uv/python/cpython-3.12.14-macos-aarch64-none",
"environment": "uv ephemeral environment; its temporary executable path changes per invocation and the original run path was not recorded",
"hypothesis_version": "6.168.5",
"settings_repr": "settings(backend='hypothesis', database=None, deadline=None, derandomize=True, max_examples=1500, phases=(Phase.generate,), print_blob=False, report_multiple_bugs=True, stateful_step_count=50, suppress_health_check=(HealthCheck.too_slow,), verbosity=Verbosity.normal)",
"database": null,
"explicit_seed": null,
"hypothesis_seed_environment": null,
"hypothesis_profile_environment": null,
"deterministic_seeds": {
"dense": 18180053857264028138491152404824351426463859085391436335048946415419244246115592507509277092856301852842287258442718,
"sparse": 37365564367670020138900098711702600163892622990505090112408647838113529152255960631081857519294674583087869779258058
},
"seed_derivation": "Hypothesis 6.168.5 get_random_for_wrapped_test uses Random(int_from_bytes(function_digest(test))) when derandomize=True",
"uv_version": "0.12.17 (635500036 2026-09-18 aarch64-apple-darwin)",
"inspection_only": true,
"final_check_count": 12495,
"run_dependency_pinned": true
}Rust graph and witness crosscomparison{
"disagreements": 0,
"fallback_graphs": 10,
"graphs": 9488,
"optimal_witnesses": 9527,
"verdict": "VERIFIED"
}Production corpus audit{
"instances": 100,
"correct": 100,
"jobs": 2,
"seconds": 4.041,
"branches": {
"anchor": 23,
"tuple": 77
},
"vertices": {
"min": 0,
"median": 6.0,
"max": 114
},
"edges": {
"min": 0,
"median": 13.5,
"max": 600
},
"total_vertices": 1932,
"total_edges": 7600,
"vs_legacy_vertices": {
"smaller": 39,
"equal": 49,
"larger": 12
},
"pred_sha256": "9322d2ede5f6f67472baa5391c767de155ebd6215896d87e8b02900644529012",
"corpus_commit": "b9ae9e39f6e51237760f26f8aec205d485490ab0",
"scope": "Real Rust reduction bundle, target solve and original source recovery; independent corpus objective and greedy witness checks; exact graph crosscomparison with independent prototype.",
"not_checked": [
"Large-instance solver performance",
"Full corpus composed SAT path sweep"
]
}Composed K3SAT path audit{
"verdict": "VERIFIED",
"source_evaluation": "Or(true)",
"source_solution": [
false,
false,
true
],
"vertices": 546,
"edges": 2066,
"vertex_bound": 546,
"edge_bound": 298116,
"overall_parameters": [
{
"field": "num_edges",
"formula": "(2 * (-1 + 2 * num_vars + 3 * num_clauses) * (num_vars + 6 * num_clauses) + (3 + num_vars + 6 * num_clauses) * (2 * num_vars + 3 * num_clauses))^2",
"relation": "upper_bound"
},
{
"field": "num_vertices",
"formula": "2 * (-1 + 2 * num_vars + 3 * num_clauses) * (num_vars + 6 * num_clauses) + (3 + num_vars + 6 * num_clauses) * (2 * num_vars + 3 * num_clauses)",
"relation": "upper_bound"
}
],
"scope": "One satisfiable composed K3SAT route with target solve, source recovery and original source reevaluation."
}Typst theorem and proof#set page(width: 180mm, margin: 15mm)
#set text(size: 10pt)
= Compact LCS to unweighted MIS: foundation and final selection
*Type resolution.* Source `LongestCommonSubsequence::Value = Max<i64>`.
Target `MaximumIndependentSet<SimpleGraph, One>::Value = Max<One::Sum>`,
where `One::Sum = i64`. This is an optimization witness reduction.
*Theorem.* For $k$ input strings, select the first shortest string as anchor
$a$. Its length is $L$, with $L=0$ for no strings. Let $T$ be total input
length, and
$F = sum_(r != a) sum_(p=0)^(L-1) |{j : s_r[j]=s_a[p]}|$.
Then the construction has exactly
$V=L(k+2)+F$, at most $V^2$ edges, and
$alpha(H)=L k+"LCS"$.
Every maximum independent set decodes to an optimal source witness, including
optima that leave embedding groups empty. Since $F <= L(T-L)$, size is
polynomial even when the declared alphabet is large.
*Construction.*
1. There is one anchor group $X_p$ for each anchor position $p$. It has an
active choice consisting of two nonadjacent twin vertices, and a skip
choice consisting of one vertex. Join the skip vertex to both twins.
2. For every other input string $r$ and anchor position $p$, create a group
$Y_(r,p)$ with one vertex for every position $j$ with $s_r[j]=s_a[p]$ and
one skip vertex. Each such group is a clique.
3. Between $X_p$ and $Y_(r,p)$, join both active twins to the skip vertex,
and join the anchor skip vertex to every matching-position vertex.
4. Between embedding groups for the same string at $p<q$, join matching
position vertices $j,j'$ precisely when $j >= j'$. Skip vertices have
no edges between different slots. Check every slot pair, including
nonadjacent slots. There are no other edges.
5. Choose the first shortest string deterministically. Number anchor groups
first in increasing position order: active twins then skip. Then number
embedding groups by increasing original string index (excluding the
anchor) and increasing anchor position: increasing matching positions
then skip. This numbering is only for comparing independent scripts.
There are $G=L k$ groups. Unlike a padded output-position encoding, anchor
positions may be skipped in the middle. Decoder output is packed into
increasing anchor order and padded at the end.
*Forward correctness.* Any common subsequence of length $ell$ has strictly
increasing anchor positions. At each retained anchor position choose both
active twins and an increasing matching position in every other string.
At every discarded anchor position choose skip in every group. This is an
independent set of size $G+ell$. In particular a longest common subsequence
gives size $G+"LCS"$; the empty subsequence gives size $G$.
*Backward correctness.* For a maximum independent set, every nonempty active
anchor cluster includes both twins, since they have identical external
neighbours. At most one choice per group is selected. Let $d_X$ and $d_Y$
be the counts of empty anchor and embedding groups, and $q$ the count of
active anchor choices. Its cardinality is
$G-d_X-d_Y+q$.
Keep active anchor positions that have a selected matching-position vertex
in every other string. Each discarded active position has at least one
distinct missing embedding group, so at most $d_Y$ active positions are
discarded. Retained positions are strictly increasing in the anchor, match
its original symbols in every other string, and increase strictly within
each other string because all slot pairs are checked. They give a common
subsequence of length $ell >= q-d_Y$. Consequently
$G-d_X-d_Y+q <= G+"LCS"-d_X <= G+"LCS"$.
Forward correctness attains this upper bound. At any optimum, $d_X=0$ and
$q-d_Y="LCS"$; the decoded common subsequence has length at least LCS and
cannot exceed LCS, so it is optimal. Missing embedding groups are permitted
and decoded by the stated retention rule, not by inventing positions.
*Solution extraction.* Validate the target dimension and independence.
Reject a partially selected active twin cluster. Determine every selected
choice. Keep only complete active anchor clusters for which every other
string's embedding group selects a matching-position vertex. Read their
original symbols in increasing anchor position, then append `None` to length
$L$. A valid independent set may leave anchor or embedding groups empty;
this mapping still gives a valid, possibly nonoptimal common subsequence.
Every optimal target witness passes validation and decodes optimally.
No source-optimality assumption is made for nonoptimal target witnesses.
*Overhead derivation.* Anchor groups contribute $3L$ vertices. Embedding
groups contribute $L(k-1)+F$. Thus $V=L(k+2)+F$ exactly and $E<=V^2$.
Counting matching positions uses no declared-alphabet iteration. Construction
can scan choices and conflicts in $O(V^2+L T+k)$ time; validated decoding uses
$O(V+E)$ time. Empty input or any empty shortest string yields an empty graph
and a zero-length source witness. With one string, $F=0$ and $V=3L$.
*MVC-derived input.* Let the original unweighted simple graph have $N$
vertices and $M$ edges. The MVC to LCS construction places the base string
$(0,1,dots,N-1)$ first, followed by $M$ edge strings each of length $2N-2$.
For each edge string, summing matches against the unique base symbols gives
exactly $2N-2$. The base is shortest (tied first when $N=2$); if $N<=1$ there
are no simple-graph edges. Hence $L=N$, $k=M+1$, $F=2 M(N-1)$, and
$V=3N+3 M N-2 M$. This is quadratic in SAT counts after substitution
$N=2n+3m$, $M=n+6m$; edges have the upper bound $(3N+3 M N-2 M)^2$.
*YES and NO example.* Strings ABC, BAC, ABC have anchor ABC, $L=3$, $k=3$,
$F=6$, $G=9$, $V=21$. AC is common: use active anchor positions 0 and 2,
embedding positions 1 and 2 in BAC, and 0 and 2 in the other ABC. Fill skip
choices at anchor position 1. The independent set has size $9+2=11$.
Length at least 2 is YES, equivalent to independent-set size at least 11.
Length at least 3 is NO because length 3 forces ABC in the anchor and BAC
does not contain ABC. The theorem makes independent-set size at least 12 NO.
*Final implementation preprocessing.* Choose the first shortest original
string as the original anchor. Keep it first, remove exact duplicate strings,
and remove every other string containing the whole original anchor as a
subsequence. Preserve the remaining input order. Compute the set of symbols
present in every remaining string, and delete all other letters from the
anchor. Write $a'$ for this filtered anchor and $L'=|a'|$. Remove every other
remaining string containing $a'$ as a subsequence. There is no pairwise
subsequence pruning and no solver in preprocessing.
This preserves the entire feasible source set. Every original common word
uses only symbols present in all original constraints, so it is a subsequence
of the filtered anchor. Conversely, the filtered anchor is a subsequence of
the original anchor. Removed containing strings follow by transitivity;
duplicates impose the same constraint. Keep the computed common-symbol set
fixed during the last pruning step, so removed constraints cannot reintroduce
an originally unavailable letter into the tuple branch. An empty filtered
anchor produces the empty tuple graph, while decoded witnesses still use
the original source padding length $L$.
Write $k'$ for retained constraints (counting the filtered anchor) and
$F'$ for their matching-position pairs against $a'$. The original bound
still applies: $L'<=L$, $k'<=k$, and $F'<=F$, because every filtered anchor
occurrence and retained string was present originally. The anchored graph
has exactly $B'=L'(k'+2)+F'<=B=L(k+2)+F$ vertices and optimum
$L' k'+"LCS"$. Let $C'$ be the retained tuple count restricted to the fixed
common symbols. Removing containing strings or duplicates removes only
positive frequency factors, so $C'<=C$. Admit tuples only when $C'<=B'$;
choose smaller total vertices plus edges, preferring tuples on a tie.
The final graph has either $C'$ or $B'$ vertices and at most $B^2$ edges.
Canonical metadata remains the original-input upper bound $B$ and exact MVC
relation for original $F$.
Skip building the anchored candidate when the admitted tuple graph has
$E_T<=B'-C'$: its total size is at most the anchored vertex count alone,
so it cannot lose. Otherwise build the anchored graph, with edge count $E_A$,
and prefer tuples if $E_T<=E_A$ or $E_T-E_A<=B'-C'$. This subtractive
comparison is equivalent to $C'+E_T<=B'+E_A$ and avoids sum overflow.
If $C'>B'$, construct only the anchored candidate. Both candidates have
already proved witness maps; selection never changes source feasibility.
Build sparse position maps over occurring symbols. Form tuple lists only for
symbols present in every retained string, and only then multiply their
nonzero lengths with arithmetic capped at $B'$. Checked multiplication or
addition exceeding the cap selects the anchored branch before enumeration.
This order prevents a missing symbol in a later string from being mistaken
for an excessive product. For $L=0$ return the empty graph and empty witness.
For one retained string the tuple graph has $L'$ isolated vertices and reads
its symbols in anchor position order. Enumerated Cartesian prefixes cannot
exceed the admitted final tuple count because every position list is nonempty.
Constructor foundation"""Independent research constructor and checks; no package implementation edits."""
import itertools
import json
from collections import Counter
from functools import lru_cache
from pathlib import Path
def reduce(strings):
anchor = min(range(len(strings)), key=lambda i: len(strings[i]), default=None)
base = [] if anchor is None else strings[anchor]
choices = []
vertex_count = 0
groups = 0
def add_group(kind, p, r, values):
nonlocal vertex_count, groups
for value in values:
count = 2 if kind == 'X' and value is True else 1
choices.append({'kind': kind, 'p': p, 'r': r, 'value': value,
'group': groups, 'vertices': list(range(vertex_count, vertex_count + count))})
vertex_count += count
groups += 1
for p in range(len(base)):
add_group('X', p, anchor, [True, None])
for r, string in enumerate(strings):
if r != anchor:
for p, symbol in enumerate(base):
add_group('Y', p, r, [j for j, x in enumerate(string) if x == symbol] + [None])
edges = []
for a, b in itertools.combinations(choices, 2):
conflict = a['group'] == b['group']
if a['kind'] == 'X' and b['kind'] == 'Y' and a['p'] == b['p']:
conflict = (a['value'] is None) != (b['value'] is None)
if a['kind'] == b['kind'] == 'Y' and a['r'] == b['r'] and a['p'] < b['p']:
conflict = a['value'] is not None and b['value'] is not None and a['value'] >= b['value']
if conflict:
edges.extend((u, v) for u in a['vertices'] for v in b['vertices'])
return {'strings': strings, 'anchor': anchor, 'vertices': vertex_count,
'edges': edges, 'choices': choices, 'groups': groups}
def independent(graph, selected):
return len(selected) == graph['vertices'] and not any(selected[u] and selected[v] for u, v in graph['edges'])
def extract(graph, selected):
if not independent(graph, selected):
raise ValueError('invalid target witness')
active = set()
embedded = set()
for c in graph['choices']:
count = sum(selected[v] for v in c['vertices'])
if count and count != len(c['vertices']):
raise ValueError('partial active twins')
if count and c['value'] is not None:
if c['kind'] == 'X':
active.add(c['p'])
else:
embedded.add((c['r'], c['p']))
if graph['anchor'] is None:
return []
return [symbol for p, symbol in enumerate(graph['strings'][graph['anchor']])
if p in active and all((r, p) in embedded for r in range(len(graph['strings'])) if r != graph['anchor'])]
def is_subsequence(word, string):
cursor = iter(string)
return all(any(x == symbol for x in cursor) for symbol in word)
def words(strings):
anchor = min(strings, key=len, default=[])
return {tuple(anchor[i] for i in range(len(anchor)) if mask >> i & 1) for mask in range(1 << len(anchor))}
def source_optimum(strings):
return max((len(word) for word in words(strings) if all(is_subsequence(word, s) for s in strings)), default=0)
def forward(graph, word):
if graph['anchor'] is None:
assert not word
return []
strings = graph['strings']
anchor = graph['anchor']
assignments = {}
positions = []
cursor = 0
for symbol in word:
cursor = next(j for j in range(cursor, len(strings[anchor])) if strings[anchor][j] == symbol)
positions.append(cursor)
cursor += 1
active = set(positions)
for p in range(len(strings[anchor])):
assignments[('X', anchor, p)] = True if p in active else None
for r, string in enumerate(strings):
if r == anchor:
continue
cursor = 0
for p in range(len(strings[anchor])):
if p in active:
j = next(j for j in range(cursor, len(string)) if string[j] == strings[anchor][p])
assignments[('Y', r, p)] = j
cursor = j + 1
else:
assignments[('Y', r, p)] = None
selected = [False] * graph['vertices']
for c in graph['choices']:
if assignments[(c['kind'], c['r'], c['p'])] == c['value']:
for v in c['vertices']:
selected[v] = True
return selected
def all_independent_sets(graph):
adjacency = [0] * graph['vertices']
for u, v in graph['edges']:
adjacency[u] |= 1 << v
adjacency[v] |= 1 << u
def visit(candidates, selected):
if not candidates:
yield selected
return
bit = candidates & -candidates
v = bit.bit_length() - 1
yield from visit(candidates ^ bit, selected)
yield from visit((candidates ^ bit) & ~adjacency[v], selected | bit)
yield from visit((1 << graph['vertices']) - 1, 0)
def families():
for k in range(6):
for lengths in itertools.product(range(6), repeat=k):
total = sum(lengths)
if total > 5:
continue
for symbols in itertools.product(range(2), repeat=total):
cursor = 0
strings = []
for length in lengths:
strings.append(list(symbols[cursor:cursor + length]))
cursor += length
yield strings
def verify():
import sympy as sp
counts = Counter()
L, k, F, N, M, n, m = sp.symbols('L k F N M n m')
assert sp.expand(3*L + L*(k-1) + F - (L*(k+2)+F)) == 0
assert sp.expand((L*(k+2)+F).subs({L:N,k:M+1,F:2*M*(N-1)}) - (3*N+3*M*N-2*M)) == 0
assert sp.Poly((3*N+3*M*N-2*M).subs({N:2*n+3*m,M:n+6*m}),n,m).total_degree() == 2
assert sp.Poly(((3*N+3*M*N-2*M)**2).subs({N:2*n+3*m,M:n+6*m}),n,m).total_degree() == 4
counts['symbolic'] += 4
output = Path(__file__).parent
with (output / 'constructor-exports.jsonl').open('w') as exports:
for strings in families():
graph = reduce(strings)
length = min(map(len, strings), default=0)
anchor = graph['anchor']
matches = 0 if anchor is None else sum(sum(x == y for x in strings[anchor] for y in string)
for r, string in enumerate(strings) if r != anchor)
assert graph['vertices'] == length * (len(strings) + 2) + matches
assert matches <= length * (sum(map(len, strings)) - length)
assert len(graph['edges']) <= graph['vertices'] ** 2
counts['overhead'] += 3
assert len(graph['edges']) == len(set(map(tuple, graph['edges'])))
assert all(0 <= u < v < graph['vertices'] for u, v in graph['edges'])
counts['structure'] += 2
best = source_optimum(strings)
maximum = -1
witnesses = []
for mask in all_independent_sets(graph):
size = mask.bit_count()
selected = [bool(mask >> i & 1) for i in range(graph['vertices'])]
if size > maximum:
maximum = size
witnesses = [selected]
elif size == maximum:
witnesses.append(selected)
try:
word = extract(graph, selected)
except ValueError:
# The only invalid structure in an independent witness is partial twins.
assert any(len(c['vertices']) == 2 and sum(selected[v] for v in c['vertices']) == 1
for c in graph['choices'])
counts['rejected_partial_twins'] += 1
else:
assert all(is_subsequence(word, s) for s in strings)
counts['all_backward_witnesses'] += 1
assert size <= graph['groups'] + best
counts['optimum_upper_bound'] += 1
assert maximum == graph['groups'] + best
for selected in witnesses:
assert len(extract(graph, selected)) == best
counts['all_optimal_extractions'] += 1
counts['optimal_equivalence'] += 1
for word in words(strings):
if all(is_subsequence(word, s) for s in strings):
selected = forward(graph, word)
assert independent(graph, selected)
assert sum(selected) == graph['groups'] + len(word)
assert tuple(extract(graph, selected)) == word
counts['all_forward_words'] += 1
counts['families'] += 1
exports.write(json.dumps({'strings':strings,'vertices':graph['vertices'],'edges':graph['edges'],
'optimum': maximum}, separators=(',',':'))+'\n')
graph = reduce([[0,1,2],[1,0,2],[0,1,2]])
witness = forward(graph, [0,2])
assert graph['vertices'] == 21 and graph['groups'] == 9
assert independent(graph,witness) and sum(witness) == 11
assert source_optimum(graph['strings']) == 2
assert 11 < 12
counts['worked_yes_no'] += 5
# A maximum may omit an embedding group: AA and A have LCS=1.
graph = reduce([[0], [0,0]])
optimum = graph['groups'] + 1
incomplete_optima = 0
for mask in all_independent_sets(graph):
if mask.bit_count() == optimum:
selected=[bool(mask>>i&1) for i in range(graph['vertices'])]
assert len(extract(graph,selected)) == 1
counts['boundary_optima'] += 1
result={'verdict':'PASSED','counts':dict(counts),'scope':'binary k<=5,total_length<=5; every independent witness and every maximum; all common words',
'example':{'vertices':21,'edges':len(reduce([[0,1,2],[1,0,2],[0,1,2]])['edges']),'optimum':11},
'limitations':['Mathematical proposal; no Rust replacement implemented','No resource-impossible numeric boundary allocated']}
(output/'constructor-result.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result,indent=2),flush=True)
if __name__ == '__main__':
verify()Final hybrid constructor"""Independent constructor of the final hybrid, plus full-domain formula checks."""
import itertools
import json
import math
import subprocess
from collections import Counter
from pathlib import Path
import sympy as sp
from anchor_constructor import reduce as anchored, extract as extract_anchor
from anchor_constructor import is_subsequence, source_optimum, words, all_independent_sets
ROOT = Path(__file__).parent
PRED = '/Users/xiweipan/Codes/problem-reductions-worktrees/lcs-polynomial-mis/target/debug/pred'
def preprocess(strings):
anchor = min(strings, key=len, default=[])
retained = [anchor]
for string in strings:
if string not in retained and not is_subsequence(anchor, string):
retained.append(string)
common = set.intersection(*map(set, retained))
filtered = [symbol for symbol in anchor if symbol in common]
return [filtered, *(s for s in retained[1:] if not is_subsequence(filtered, s))]
def cap(strings):
anchor = min(strings, key=len, default=[])
a = Counter(anchor)
counts = sum(sum(a[symbol] for symbol in string) for r, string in enumerate(strings)
if r != min(range(len(strings)), key=lambda i: len(strings[i]), default=None))
return len(anchor) * (len(strings)+2) + counts
def tuple_count(strings):
common = set.intersection(*map(set, strings)) if strings else set()
return sum(math.prod(Counter(s)[c] for s in strings) for c in common)
def reduce(strings):
retained = preprocess(strings)
bound = cap(retained)
count = tuple_count(retained)
if count > bound:
graph = anchored(retained)
graph['branch'] = 'anchor'
graph['retained'] = retained
return graph
common = set.intersection(*map(set, retained))
nodes = [(c, positions) for c in sorted(common)
for positions in itertools.product(*[[j for j,x in enumerate(s) if x == c] for s in retained])]
edges = [(i,j) for i,(_,a) in enumerate(nodes) for j,(_,b) in enumerate(nodes[i+1:],i+1)
if not (all(x<y for x,y in zip(a,b)) or all(x>y for x,y in zip(a,b)))]
if retained[0]:
candidate = anchored(retained)
if candidate['vertices'] + len(candidate['edges']) < len(nodes) + len(edges):
candidate.update(branch='anchor', retained=retained)
return candidate
return {'vertices':len(nodes),'edges':edges,'nodes':nodes,'retained':retained,
'branch':'empty' if not min(strings,key=len,default=[]) else 'tuple'}
def extract(graph, selected):
if graph['branch'] == 'anchor':
return extract_anchor(graph,selected)
assert not any(selected[u] and selected[v] for u,v in graph['edges'])
chosen = [graph['nodes'][i] for i,v in enumerate(selected) if v]
return [c for c,positions in sorted(chosen,key=lambda node:node[1][0])]
def verify():
L,k,F,N,M,n,m = sp.symbols('L k F N M n m')
assert sp.expand(3*L+L*(k-1)+F-(L*(k+2)+F)) == 0
expression = (L*(k+2)+F).subs({L:N,k:M+1,F:2*M*(N-1)})
assert sp.expand(expression-(3*N+3*M*N-2*M)) == 0
assert sp.Poly(expression.subs({N:2*n+3*m,M:n+6*m}),n,m).total_degree()==2
assert sp.Poly((expression**2).subs({N:2*n+3*m,M:n+6*m}),n,m).total_degree()==4
audit = Counter(symbolic=4)
for path in ['exhaustive.jsonl','targeted.jsonl']:
for line in (ROOT/'hybrid-adversary'/path).read_text().splitlines():
reference = json.loads(line)
strings=reference['strings']
graph=reduce(strings)
best=source_optimum(strings)
assert graph['vertices']==reference['vertices']
assert sorted(graph['edges'])==[tuple(e) for e in reference['edges']]
assert best==reference['source_optimum']
assert graph['branch']==reference['branch']
audit['graph_cross_comparison']+=1
retained=graph['retained']
assert cap(retained)<=cap(strings)
assert tuple_count(retained)<=tuple_count(strings)
assert graph['vertices']<=cap(retained)
assert graph['vertices']<=cap(strings)
assert len(graph['edges'])<=cap(strings)**2
audit['overhead_and_preprocessing']+=5
for word in words(strings):
assert all(is_subsequence(word,s) for s in strings)==all(is_subsequence(word,s) for s in retained)
audit['feasible_set_preservation']+=1
offset=len(retained[0])*len(retained) if graph['branch']=='anchor' else 0
if graph['vertices'] <= 16:
maximum=-1
for mask in all_independent_sets(graph):
selected=[bool(mask>>i&1) for i in range(graph['vertices'])]
word=extract(graph,selected)
assert all(is_subsequence(word,s) for s in strings)
assert mask.bit_count()<=offset+best
maximum=max(maximum,mask.bit_count())
audit['all_feasible_target_witnesses']+=1
else:
target={'type':'MaximumIndependentSet','variant':{'graph':'SimpleGraph','weight':'One'},
'data':{'graph':{'num_vertices':graph['vertices'],'edges':graph['edges']},'weights':[1]*graph['vertices']}}
process=subprocess.run([PRED,'solve','-','--solver','ilp','--json','--timeout','30'],
input=json.dumps(target),text=True,capture_output=True,check=True,timeout=35)
solved=json.loads(process.stdout)
assert solved['status']=='optimal'
maximum=sum(solved['solution'])
assert len(extract(graph,solved['solution']))==best
audit['real_ilp_target_checks']+=1
assert maximum==best+offset==reference['optimum']
audit['optimum_equivalence']+=1
assert audit['graph_cross_comparison']==9488
result={'verdict':'VERIFIED','audit':dict(audit),'disagreements':0,
'limits':['No resource-impossible numeric allocation','Sparse large-alphabet source reference uses subsequence enumeration']}
(ROOT/'hybrid-constructor-result.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result,indent=2))
if __name__=='__main__':
verify()Fresh independent adversary"""Independent adversary: construction source is anchor-proof.typ only."""
from collections import Counter
from itertools import combinations, product
from math import prod
from pathlib import Path
import json
import time
from hypothesis import given, settings, strategies as st, Phase, HealthCheck
OUT = Path(__file__).parent
STATS = Counter()
def subsequence(needle, haystack):
cursor = iter(haystack)
return all(any(x == y for y in cursor) for x in needle)
def source_optimum(strings):
if not strings:
return 0
a = min(strings, key=len)
for size in range(len(a), -1, -1):
for chosen in combinations(range(len(a)), size):
candidate = tuple(a[p] for p in chosen)
if all(subsequence(candidate, s) for s in strings):
return size
raise AssertionError("empty subsequence must exist")
def feasible_words(strings):
if not strings:
return {()}
anchor = min(strings, key=len)
return {word for mask in range(1 << len(anchor))
for word in [tuple(c for p, c in enumerate(anchor) if mask & (1 << p))]
if all(subsequence(word, s) for s in strings)}
def raw_prune(strings):
if not strings:
return []
anchor_index = min(range(len(strings)), key=lambda i: len(strings[i]))
anchor = tuple(strings[anchor_index])
retained, seen = [anchor], {anchor}
for i, raw in enumerate(strings):
s = tuple(raw)
if i == anchor_index or s in seen:
continue
seen.add(s)
if not subsequence(anchor, s):
retained.append(s)
return retained
def preprocess(strings):
retained = raw_prune(strings)
if not retained:
return []
common = set(retained[0]).intersection(*(set(s) for s in retained[1:]))
anchor = tuple(c for c in retained[0] if c in common)
return [anchor] + [s for s in retained[1:] if not subsequence(anchor, s)]
def bounds(strings):
if not strings:
return 0, 0
a = min(strings, key=len)
# Count pairs directly, rather than using the reducer's position maps.
index = next(i for i, s in enumerate(strings) if s is a)
f = sum(x == y for i, s in enumerate(strings) if i != index
for x in a for y in s)
return len(a) * (len(strings) + 2) + f, f
def tuple_count(strings):
if not strings:
return 0
counts = [Counter(s) for s in strings]
common = set(counts[0]).intersection(*(set(c) for c in counts[1:]))
return sum(prod(c[symbol] for c in counts)
for symbol in common)
def capped_tuple_count(strings, cap):
if not strings:
return 0
positions = [{c: [j for j, d in enumerate(s) if d == c] for c in set(s)}
for s in strings]
common = set(positions[0]).intersection(*(set(p) for p in positions[1:]))
count = 0
for symbol in sorted(common):
term = 1
for p in positions:
if term > cap // len(p[symbol]):
return cap + 1
term *= len(p[symbol])
if term > cap - count:
return cap + 1
count += term
return count
def graph(kind, strings, records, edges, x=None, y=None):
return {'kind': kind, 'strings': strings, 'records': records,
'edges': sorted(edges), 'x': x or [], 'y': y or [],
'padding': len(strings[0]) if strings else 0}
def anchor_graph(retained):
if not retained or not retained[0]:
return graph('empty', retained, [], set())
a = retained[0]
records, edges, x, y = [], set(), [], []
def vertex(record):
records.append(record)
return len(records) - 1
def connect(u, v):
edges.add((min(u, v), max(u, v)))
for p in range(len(a)):
u = vertex(('active', p))
v = vertex(('active', p))
skip = vertex(('anchor_skip', p))
x.append((u, v, skip))
connect(u, skip)
connect(v, skip)
for r, s in enumerate(retained[1:], 1):
groups = []
for p, symbol in enumerate(a):
matching = [(j, vertex(('match', r, p, j)))
for j, c in enumerate(s) if c == symbol]
skip = vertex(('embedding_skip', r, p))
ids = [v for _, v in matching] + [skip]
for u, v in combinations(ids, 2):
connect(u, v)
u, v, anchor_skip = x[p]
connect(u, skip)
connect(v, skip)
for _, chosen in matching:
connect(anchor_skip, chosen)
groups.append((matching, skip))
for p, q in combinations(range(len(a)), 2):
for j, u in groups[p][0]:
for jj, v in groups[q][0]:
if j >= jj:
connect(u, v)
y.append(groups)
return graph('anchor', retained, records, edges, x, y)
def tuple_graph(retained, symbols=None):
records = []
if retained:
common = set(retained[0]).intersection(*(set(s) for s in retained[1:]))
if symbols is not None:
common.intersection_update(symbols)
for c in sorted(common):
lists = [[j for j, d in enumerate(s) if d == c] for s in retained]
records.extend((c, positions) for positions in product(*lists))
edges = set()
for u, v in combinations(range(len(records)), 2):
a, b = records[u][1], records[v][1]
if not (all(x < y for x, y in zip(a, b)) or
all(x > y for x, y in zip(a, b))):
edges.add((u, v))
return graph('tuple', retained, records, edges)
def reduce(strings):
padding = min(map(len, strings)) if strings else 0
retained = preprocess(strings)
if padding == 0:
return graph('empty', retained, [], set())
cap, _ = bounds(retained)
if capped_tuple_count(retained, cap) > cap:
chosen = anchor_graph(retained)
else:
tg = tuple_graph(retained)
slack = cap - len(tg['records'])
if len(tg['edges']) <= slack:
chosen = tg
else:
ag = anchor_graph(retained)
chosen = tg if (len(tg['edges']) <= len(ag['edges']) or
len(tg['edges']) - len(ag['edges']) <= slack) else ag
chosen['padding'] = padding
return chosen
def exact_mis(g):
"""Maximum clique of the complement, using independent greedy coloring bounds."""
n = len(g['records'])
full = (1 << n) - 1
adjacent = [full ^ (1 << v) for v in range(n)]
for u, v in g['edges']:
adjacent[u] &= ~(1 << v)
adjacent[v] &= ~(1 << u)
best = []
def visit(candidates, chosen):
nonlocal best
if not candidates:
if len(chosen) > len(best):
best = chosen[:]
return
# Independent color classes in complement bound its clique size.
order, upper = [], []
uncolored, color = candidates, 0
while uncolored:
color += 1
available = uncolored
while available:
bit = available & -available
v = bit.bit_length() - 1
uncolored ^= bit
available ^= bit
available &= ~adjacent[v]
order.append(v)
upper.append(color)
for i in range(len(order) - 1, -1, -1):
if len(chosen) + upper[i] <= len(best):
return
v = order[i]
visit(candidates & adjacent[v], chosen + [v])
candidates &= ~(1 << v)
visit(full, [])
return len(best), set(best)
def extract(g, witness):
if len(witness) != len(g['records']):
raise ValueError('dimension')
selected = {i for i, b in enumerate(witness) if b}
if any(u in selected and v in selected for u, v in g['edges']):
raise ValueError('independence')
if g['kind'] == 'empty':
return [None] * g['padding']
anchor = g['strings'][0]
if g['kind'] == 'tuple':
ordered = sorted(selected, key=lambda i: g['records'][i][1][0])
answer = [g['records'][i][0] for i in ordered]
else:
answer = []
for p, (u, v, _) in enumerate(g['x']):
if (u in selected) != (v in selected):
raise ValueError('partial twins')
if u in selected and all(any(chosen in selected for _, chosen in groups[p][0])
for groups in g['y']):
answer.append(anchor[p])
return answer + [None] * (g['padding'] - len(answer))
def check_decoded(strings, result, expected=None):
nonpadding = [x for x in result if x is not None]
assert result == nonpadding + [None] * (len(result) - len(nonpadding))
assert len(result) == (min(map(len, strings)) if strings else 0)
assert all(subsequence(nonpadding, s) for s in strings)
if expected is not None:
assert len(nonpadding) == expected
def serialize(strings, g, optimum, source):
return {'strings': [list(s) for s in strings], 'vertices': len(g['records']),
'edges': [list(e) for e in g['edges']], 'optimum': optimum,
'source_optimum': source, 'branch': g['kind']}
def check(strings, export=None, force_anchor=False):
strings = [tuple(s) for s in strings]
source = source_optimum(strings)
retained = preprocess(strings)
assert source_optimum(retained) == source
assert feasible_words(strings) == feasible_words(retained)
STATS['full_feasible_set_checks'] += 1
raw = raw_prune(strings)
fixed_common = set(raw[0]).intersection(*(set(s) for s in raw[1:])) if raw else set()
assert not retained or set(retained[0]) == fixed_common
original_cap, original_f = bounds(strings)
cap, f = bounds(retained)
assert cap <= original_cap and f <= original_f
count = tuple_count(retained)
assert count <= tuple_count(strings)
capped = capped_tuple_count(retained, cap)
assert (capped <= cap) == (count <= cap)
if count <= cap:
assert capped == count
g = reduce(strings)
assert len(g['records']) == (count if g['kind'] == 'tuple' else cap)
assert len(g['records']) <= original_cap
assert len(g['edges']) <= original_cap ** 2
if not strings or min(map(len, strings)) == 0:
assert g['kind'] == 'empty'
elif count > cap:
assert g['kind'] == 'anchor'
STATS['anchor_cap_exceeded'] += 1
else:
# Independent expected policy uses full integer sums, not subtraction.
candidate_t = tuple_graph(retained)
candidate_a = anchor_graph(retained)
# Original positions and compact surviving positions have equal edges.
original_positions = tuple_graph([raw[0]] + retained[1:], fixed_common)
assert original_positions['edges'] == candidate_t['edges']
assert len(original_positions['records']) == len(candidate_t['records'])
STATS['anchor_position_isomorphisms'] += 1
total_t = len(candidate_t['records']) + len(candidate_t['edges'])
total_a = len(candidate_a['records']) + len(candidate_a['edges'])
assert g['kind'] == ('tuple' if total_t <= total_a else 'anchor')
if g['kind'] == 'anchor':
STATS['anchor_with_admitted_tuples'] += 1
if total_t == total_a:
assert g['kind'] == 'tuple'
STATS['graph_size_ties'] += 1
if len(candidate_t['edges']) <= cap-count:
assert g['kind'] == 'tuple'
STATS['fast_tuple_wins'] += 1
optimum, chosen = exact_mis(g)
expected = source + (len(retained) * len(retained[0]) if g['kind'] == 'anchor' else 0)
assert optimum == expected, (strings, optimum, expected, g['kind'])
check_decoded(strings, extract(g, [i in chosen for i in range(len(g['records']))]), source)
STATS['checks'] += 1
STATS[g['kind']] += 1
if export:
export.write(json.dumps(serialize(strings, g, optimum, source), separators=(',', ':')) + '\n')
if force_anchor:
ag = anchor_graph(retained)
ag['padding'] = min(map(len, strings)) if strings else 0
optimum, chosen = exact_mis(ag)
expected = source + (len(retained) * len(retained[0]) if retained else 0)
assert optimum == expected
check_decoded(strings, extract(ag, [i in chosen for i in range(len(ag['records']))]), source)
STATS['forced_anchor_checks'] += 1
if len(ag['records']) <= 15:
# Independent enumeration checks the exact solver and every optimum.
brute_optimum = 0
for mask in all_independent_sets(ag):
brute_optimum = max(brute_optimum, mask.bit_count())
if mask.bit_count() == optimum:
check_decoded(strings, extract(ag, [bool(mask & (1 << i))
for i in range(len(ag['records']))]), source)
STATS['all_small_anchor_optima'] += 1
assert brute_optimum == optimum
STATS['brute_target_crosschecks'] += 1
return g, source
def ordered_binary_families(max_k=5, total=5):
def build(k, remaining):
if k == 0:
yield []
return
for length in range(remaining + 1):
for s in product((0, 1), repeat=length):
for suffix in build(k - 1, remaining - length):
yield [s] + suffix
for k in range(max_k + 1):
yield from build(k, total)
def all_independent_sets(g):
neighbors = [0] * len(g['records'])
for u, v in g['edges']:
neighbors[u] |= 1 << v
neighbors[v] |= 1 << u
def visit(available, selected):
if not available:
yield selected
return
bit = available & -available
v = bit.bit_length() - 1
yield from visit(available ^ bit, selected)
yield from visit((available ^ bit) & ~neighbors[v], selected | bit)
yield from visit((1 << len(g['records'])) - 1, 0)
def targeted():
# Equal-length, distinct permutations survive anchor containment pruning.
fallback = [
[(0,0,0,1,1), (0,0,1,0,1), (0,1,0,0,1), (1,0,0,0,1), (1,1,0,0,0)],
[(0,0,0,1,1,1), (0,0,1,0,1,1), (0,1,0,1,0,1), (1,1,1,0,0,0)],
[(0,0,0,0,1), (0,0,0,1,0), (0,0,1,0,0)],
[(0,0,0,0,0,0,1,2), (1,0,0,0,0,0,0,2), (2,0,0,0,0,0,0,1)],
]
# Include anchor at later original index, duplicates, and containing inputs.
fallback += [fallback[0] + [fallback[0][0], (9,) + fallback[0][0] + (8,)],
[(9,) + fallback[1][0] + (8,), *fallback[1][1:], fallback[1][0]]]
with (OUT / 'targeted.jsonl').open('w') as export:
for strings in fallback:
g, _ = check(strings, export, force_anchor=True)
assert g['kind'] == 'anchor'
# Exact cap equality admits enumeration, then compares graph totals.
boundary = [(1,0,1), (0,1,1,1,1), (1,1,1,1,0)]
g, _ = check(boundary, export, force_anchor=True)
assert tuple_count(preprocess(boundary)) == bounds(preprocess(boundary))[0] == 33
STATS['exact_cap_boundary'] += 1
selector_cases = [
('fast', [(0,0), (0,1)], 'tuple'),
('tuple_compared', [(0,0,0), (0,0,1), (0,1,0)], 'tuple'),
('anchor_admitted', [(0,0,0), (0,0,1), (0,1,0), (1,0,0)], 'anchor'),
('tie', [(0,0,0,1), (0,1,0,1), (1,1,0,0)], 'tuple'),
]
selector_report = []
for label, strings, branch in selector_cases:
g, _ = check(strings, export, force_anchor=True)
assert g['kind'] == branch
retained = preprocess(strings)
tg, ag = tuple_graph(retained), anchor_graph(retained)
selector_report.append({'case': label, 'strings': strings, 'branch': branch,
'C': len(tg['records']), 'B':len(ag['records']),
'E_T':len(tg['edges']), 'E_A':len(ag['edges'])})
(OUT / 'selector_cases.json').write_text(json.dumps(selector_report, indent=2) + '\n')
normalization_cases = [
('filtered_anchor_bound', [(0,0,1,2), (1,1,1,0,0,0,0,0),
(1,1,1,1,0,0,0,0,0,0)], 'anchor', 44, 249, 2),
('filtered_containing', [(0,0,1), (0,)*5, (0,)*6], 'tuple', 2, 0, 2),
('absent_letter_reinsertion', [(0,1,2), (0,0,0,1,1), (0,0,0,0)],
'tuple', 1, 0, 1),
('empty_filtered_anchor_padding', [(0,1), (2,3)], 'tuple', 0, 0, 0),
('gapped_original_anchor_positions', [(0,2,1,2,0), (1,1,0,0,0),
(1,0,0,0,0)], 'anchor', 32, 97, 2),
]
normalization_report = []
for label, strings, branch, vertices, edges, source in normalization_cases:
g, observed_source = check(strings, export, force_anchor=True)
assert (g['kind'],len(g['records']),len(g['edges']),observed_source) == (branch,vertices,edges,source), label
normalized = preprocess(strings)
normalization_report.append({'case': label, 'strings': strings,
'retained': normalized, 'branch':g['kind'],
'vertices':vertices, 'edges':edges,
'source_optimum':source, 'padding':g['padding']})
(OUT / 'normalization_cases.json').write_text(json.dumps(normalization_report, indent=2) + '\n')
# Keeping original labels after dropping the blocker would revive 1,2.
adversary = normalization_cases[2][1]
naive = tuple_graph([tuple(adversary[0])])
assert exact_mis(naive)[0] == 3
assert source_optimum(adversary) == 1
assert preprocess(adversary) == [(0,)]
STATS['absent_letter_reinsertion_regressions'] += 1
# Worked YES/NO after preprocessing ABC, BAC, ABC -> ABC, BAC.
strings = [(0,1,2), (1,0,2), (0,1,2)]
g, source = check(strings, force_anchor=True)
optimum, _ = exact_mis(g)
assert source == 2 and optimum >= 2 and optimum < 3
ag = anchor_graph(preprocess(strings))
optimum, _ = exact_mis(ag)
assert optimum == 8 and optimum >= 6 + 2 and optimum < 6 + 3
# Gap at anchor p=1 yields AC; explicitly test packed padding.
selected = {ag['x'][0][0], ag['x'][0][1], ag['x'][1][2],
ag['x'][2][0], ag['x'][2][1]}
for p, (matches, skip) in enumerate(ag['y'][0]):
selected.add(skip if p == 1 else next(v for j, v in matches if j == (1 if p == 0 else 2)))
assert extract(ag, [i in selected for i in range(len(ag['records']))]) == [0,2,None]
STATS['gapped_anchor'] += 1
# This is an actual hybrid fallback optimum with an empty embedding group.
missing_strings = fallback[3]
mg = reduce(missing_strings)
assert mg['kind'] == 'anchor'
selected = {v for p, group in enumerate(mg['x'])
for v in (group[:2] if p < 7 else group[2:])}
for r, groups in enumerate(mg['y']):
for p, (matches, skip) in enumerate(groups):
if p == 7:
selected.add(skip)
elif p < 6:
selected.add(next(v for j, v in matches if j == p + 1))
elif r == 1:
selected.add(next(v for j, v in matches if j == 7))
assert len(selected) == 30 == exact_mis(mg)[0]
assert extract(mg, [i in selected for i in range(len(mg['records']))]) == [0]*6 + [None]*2
STATS['hybrid_missing_group_optimum'] += 1
# Bounded hybrid can select the anchor graph with a missing embedding group.
# Search all independent sets of a small anchored instance independently.
small = [(0,1), (1,0)]
ag = anchor_graph(preprocess(small))
optimum, _ = exact_mis(ag)
missing_optima, all_optima = 0, 0
for mask in all_independent_sets(ag):
witness = [bool(mask & (1 << i)) for i in range(len(ag['records']))]
partial = any(witness[u] != witness[v] for u, v, _ in ag['x'])
if partial:
try:
extract(ag, witness)
except ValueError as e:
assert str(e) == 'partial twins'
STATS['partial_twins_rejected'] += 1
else:
raise AssertionError('partial twins accepted')
else:
result = extract(ag, witness)
check_decoded(small, result, 1 if mask.bit_count() == optimum else None)
STATS['arbitrary_independent_decodes'] += 1
if mask.bit_count() == optimum:
all_optima += 1
empty_group = any(not any(witness[v] for _, v in matches) and not witness[skip]
for groups in ag['y'] for matches, skip in groups)
if empty_group:
missing_optima += 1
assert result in ([0,None], [1,None])
assert missing_optima > 0
STATS['small_all_optima'] = all_optima
STATS['missing_group_optima'] = missing_optima
# Empty families, empty anchors, and one retained string are exact cases.
for strings in ([], [()], [(0,1), ()], [(1,)], [(1,1,1)], [(0,1),(9,0,1,8),(0,1)]):
check(strings, force_anchor=True)
STATS['zero_or_single_cases'] += 1
# A later absent symbol must suppress a huge earlier Cartesian factor.
assert capped_tuple_count([(0,)*80, (0,)*80, (1,)*80], 1) == 0
assert capped_tuple_count([(0,)*80, (0,)*80, (0,)*80], 50) == 51
STATS['capped_count_regressions'] += 2
# Trust-boundary checks operate on graph witnesses, not graph internals.
try:
extract(ag, [False])
except ValueError as e:
assert str(e) == 'dimension'
else:
raise AssertionError('bad dimension accepted')
edge = ag['edges'][0]
try:
extract(ag, [i in edge for i in range(len(ag['records']))])
except ValueError as e:
assert str(e) == 'independence'
else:
raise AssertionError('conflicting vertices accepted')
STATS['validation_regressions'] += 2
DENSE = st.lists(st.lists(st.integers(0, 1), min_size=3, max_size=7).map(tuple),
min_size=2, max_size=5)
SPARSE = st.lists(st.lists(st.integers(0, 31), min_size=0, max_size=9).map(tuple),
min_size=0, max_size=6)
HYP_SETTINGS = settings(max_examples=1500, deadline=None, derandomize=True,
phases=[Phase.generate], suppress_health_check=[HealthCheck.too_slow])
@HYP_SETTINGS
@given(DENSE)
def dense(strings):
check(strings)
STATS['dense_hypothesis'] += 1
@HYP_SETTINGS
@given(SPARSE)
def sparse(strings):
check(strings)
STATS['sparse_hypothesis'] += 1
def main():
start = time.monotonic()
targeted()
with (OUT / 'exhaustive.jsonl').open('w') as export:
for strings in ordered_binary_families():
check(strings, export, force_anchor=True)
STATS['exhaustive'] += 1
assert STATS['exhaustive'] == 9472, STATS
print('exhaustive complete', dict(STATS), flush=True)
dense()
print('dense complete', dict(STATS), flush=True)
sparse()
assert STATS['dense_hypothesis'] >= 1500
assert STATS['sparse_hypothesis'] >= 1500
assert STATS['checks'] > 5000
report = {'status': 'PASS', 'counts': dict(STATS), 'seconds': time.monotonic() - start,
'construction_source': 'anchor-proof.typ',
'source_solver': 'descending enumeration of anchor subsequences',
'target_solver': 'maximum clique in complement with greedy coloring bounds',
'exports': ['exhaustive.jsonl', 'targeted.jsonl']}
(OUT / 'result.json').write_text(json.dumps(report, indent=2) + '\n')
print(json.dumps(report, indent=2), flush=True)
if __name__ == '__main__':
main() |
Collaborator
Author
Verification certificate — production reproductionHead Rust structural and optimal witness probeuse problemreductions::models::misc::LongestCommonSubsequence;
use problemreductions::models::graph::MaximumIndependentSet;
use problemreductions::rules::{ReduceTo, ReductionResult, ReductionGraph};
use problemreductions::solvers::{BruteForce, ILPSolver};
use problemreductions::topology::{Graph, SimpleGraph};
use problemreductions::traits::Problem;
use problemreductions::types::{Max, One};
use serde_json::{Value, json};
use std::io::BufRead;
fn main() {
let mut graphs = 0usize;
let mut witnesses = 0usize;
let mut fallback = 0usize;
let graph = ReductionGraph::new();
let entry = graph.find_entry("LongestCommonSubsequence", &Default::default(),
"MaximumIndependentSet", &problemreductions::export::variant_to_map(MaximumIndependentSet::<SimpleGraph, One>::variant())).unwrap();
let transform = entry.parameter_contract.as_ref().unwrap().transform().unwrap();
for line in std::io::stdin().lock().lines() {
let reference: Value = serde_json::from_str(&line.unwrap()).unwrap();
let strings: Vec<Vec<usize>> = serde_json::from_value(reference["strings"].clone()).unwrap();
let alphabet = strings.iter().flatten().max().map_or(0, |symbol| symbol + 1);
let source = LongestCommonSubsequence::new(alphabet, strings);
let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
let target = reduction.target_problem();
assert_eq!(target.num_vertices(), usize::try_from(reference["vertices"].as_u64().unwrap()).unwrap(), "{reference}");
let mut actual = target.graph().edges();
actual.sort_unstable();
let expected: Vec<(usize,usize)> = serde_json::from_value(reference["edges"].clone()).unwrap();
assert_eq!(actual, expected, "{reference}");
let predicted = transform.evaluate(&source.parameters()).unwrap();
assert!(u64::try_from(target.num_vertices()).unwrap() <= predicted.get("num_vertices").unwrap());
assert!(u64::try_from(target.num_edges()).unwrap() <= predicted.get("num_edges").unwrap());
let expected_source = reference["source_optimum"].as_i64().unwrap();
if alphabet <= 4 {
let witness = BruteForce::new().solve(&source).unwrap().unwrap();
assert_eq!(source.evaluate(&witness).unwrap(), Max(Some(expected_source)));
}
let solutions = if target.num_vertices() <= 16 {
BruteForce::new().find_all_witnesses(target).unwrap()
} else {
vec![ILPSolver::new().solve(target).unwrap()]
};
for solution in solutions {
assert_eq!(target.evaluate(&solution).unwrap(), Max(reference["optimum"].as_i64()));
let decoded = reduction.extract_solution(&solution).unwrap();
assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(expected_source)), "{reference}");
witnesses += 1;
}
graphs += 1;
fallback += usize::from(reference["branch"] == "anchor");
}
assert_eq!(graphs, 9488);
assert_eq!(fallback, 10);
println!("{}", json!({"graphs":graphs,"optimal_witnesses":witnesses,"fallback_graphs":fallback,"disagreements":0,"verdict":"VERIFIED"}));
}Production single-rule corpus verifier"""Production single-rule corpus gate with independent source truth and graph oracle."""
import concurrent.futures
import hashlib
import json
import statistics
import subprocess
import sys
import time
from collections import Counter
from pathlib import Path
from hybrid_constructor import reduce, preprocess, cap, tuple_count, is_subsequence
ROOT = Path(__file__).parent
OUTPUT = ROOT / 'corpus-final'
OUTPUT.mkdir(exist_ok=False)
CORPUS = Path('/Users/xiweipan/Codes/pred-validation-corpus')
WORKTREE = Path('/Users/xiweipan/Codes/problem-reductions-worktrees/lcs-polynomial-mis')
PRED = WORKTREE / 'target/debug/pred'
sys.path.insert(0,str(CORPUS/'scripts'))
import verify_rules
accuracy=verify_rules.load_accuracy_helpers(CORPUS)
truth=sorted((r for r in accuracy.load_truth().values() if r['problem']=='LongestCommonSubsequence'),key=lambda r:r['instance'])
assert len(truth)==100 and all(r['verified'] for r in truth)
routes,unavailable=verify_rules.discover_routes(PRED,[{'source':'LongestCommonSubsequence','target':'MaximumIndependentSet/SimpleGraph/One'}],OUTPUT)
assert len(routes)==1 and not unavailable
route=routes[0]
def run_one(row):
started=time.monotonic()
source=json.loads((CORPUS/row['instance']).read_text())['data']
strings=source['strings']
expected=reduce(strings)
bundle,error=verify_rules.run_json([str(PRED),'reduce',str(CORPUS/row['instance']),'--via',str(route['route']),'--quiet','--json'],timeout=30)
assert not error,(row['instance'],error)
graph=bundle['target']['data']['graph']
assert graph['num_vertices']==expected['vertices']
assert sorted(map(tuple,graph['edges']))==sorted(expected['edges'])
result,error=verify_rules.run_json([str(PRED),'solve','-','--quiet','--json','--timeout','30'],timeout=40,input_text=json.dumps(bundle))
assert not error,(row['instance'],error)
correct,classification,actual=verify_rules.compare_source(accuracy,CORPUS,row,result)
assert correct,(row['instance'],classification,result)
word=[x for x in result['solution'] if x is not None]
assert len(word)==row['value'] and all(is_subsequence(word,s) for s in strings)
retained=expected['retained']
offset=len(retained[0])*len(retained) if expected['branch']=='anchor' else 0
target_value=accuracy.parse_evaluation(result['intermediate']['evaluation'])
assert result['intermediate']['status']=='optimal' and target_value==offset+row['value']
assert graph['num_vertices']<=cap(strings) and len(graph['edges'])<=cap(strings)**2
return {'instance':row['instance'],'correct':correct,'expected':row['value'],'actual':actual,
'vertices':graph['num_vertices'],'edges':len(graph['edges']),'legacy_vertices':tuple_count(strings),
'branch':expected['branch'],'retained_strings':len(retained),'original_strings':len(strings),
'seconds':time.monotonic()-started}
started=time.monotonic()
rows=[]
with concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool, (OUTPUT/'results.jsonl').open('w') as stream:
for count,result in enumerate(pool.map(run_one,truth),1):
rows.append(result)
stream.write(json.dumps(result)+'\n')
stream.flush()
if count%20==0:
print(json.dumps({'completed':count,'seconds':round(time.monotonic()-started,2)}),flush=True)
report={'instances':len(rows),'correct':sum(r['correct'] for r in rows),'jobs':2,
'seconds':round(time.monotonic()-started,3),'branches':dict(Counter(r['branch'] for r in rows)),
'vertices':{'min':min(r['vertices'] for r in rows),'median':statistics.median(r['vertices'] for r in rows),'max':max(r['vertices'] for r in rows)},
'edges':{'min':min(r['edges'] for r in rows),'median':statistics.median(r['edges'] for r in rows),'max':max(r['edges'] for r in rows)},
'total_vertices':sum(r['vertices'] for r in rows),'total_edges':sum(r['edges'] for r in rows),
'vs_legacy_vertices':{'smaller':sum(r['vertices']<r['legacy_vertices'] for r in rows),
'equal':sum(r['vertices']==r['legacy_vertices'] for r in rows),
'larger':sum(r['vertices']>r['legacy_vertices'] for r in rows)},
'pred_sha256':hashlib.sha256(PRED.read_bytes()).hexdigest(),
'corpus_commit':subprocess.check_output(['git','-C',str(CORPUS),'rev-parse','HEAD'],text=True).strip(),
'scope':'Real Rust reduction bundle, target solve and original source recovery; independent corpus objective and greedy witness checks; exact graph crosscomparison with independent prototype.',
'not_checked':['Large-instance solver performance','Full corpus composed SAT path sweep']}
(OUTPUT/'report.json').write_text(json.dumps(report,indent=2)+'\n')
print(json.dumps(report,indent=2),flush=True)Composed K3SAT route verifier"""Representative composed K3SAT path: actual route, solve, recovery, evaluation."""
import json, subprocess
from pathlib import Path
ROOT=Path(__file__).parent
PRED='/Users/xiweipan/Codes/problem-reductions-worktrees/lcs-polynomial-mis/target/debug/pred'
OUT=ROOT/'sat-path-final'
OUT.mkdir(exist_ok=True)
def run(args):
p=subprocess.run([PRED,*args,'--json'],capture_output=True,text=True,check=True,timeout=60)
return json.loads(p.stdout) if p.stdout.strip() else None
source=OUT/'source.json'
run(['create','KSatisfiability/K3','--num-vars','3','--clauses','1,2,3;-1,-2,-3','-o',str(source)])
paths=run(['path','KSatisfiability/K3','MaximumIndependentSet/SimpleGraph/One','--limit','all'])
(OUT/'paths.json').write_text(json.dumps(paths,indent=2))
names=['KSatisfiability','DecisionMinimumVertexCover','MinimumVertexCover','LongestCommonSubsequence','MaximumIndependentSet']
route=next(p for p in paths['paths'] if [p['path'][0]['from']['name']]+[s['to']['name'] for s in p['path']]==names)
fields=route['overall_parameters']['fields']
assert {f['field'] for f in fields}=={'num_vertices','num_edges'}
assert all(f['relation']=='upper_bound' and f.get('formula') for f in fields)
route_file=OUT/'route.json';route_file.write_text(json.dumps(route))
bundle_file=OUT/'bundle.json'
bundle=run(['reduce',str(source),'--via',str(route_file),'-o',str(bundle_file)])
bundle=json.loads(bundle_file.read_text())
solved=run(['solve',str(bundle_file),'--solver','ilp','--timeout','30'])
assert solved['status']=='optimal' and solved['evaluation']=='Or(true)',solved
assignment=solved['solution']
assert len(assignment)==3 and any(assignment) and not all(assignment)
evaluated=run(['evaluate',str(source),'--config',json.dumps(assignment)])
assert evaluated['result']=='Or(true)',evaluated
graph=bundle['target']['data']['graph']
N,M=12,15
bound=3*N+3*M*N-2*M
assert bound==546 and graph['num_vertices']<=bound and len(graph['edges'])<=bound**2
report={'verdict':'VERIFIED','source_evaluation':solved['evaluation'],'source_solution':assignment,
'vertices':graph['num_vertices'],'edges':len(graph['edges']),
'vertex_bound':bound,'edge_bound':bound**2,'overall_parameters':fields,
'scope':'One satisfiable composed K3SAT route with target solve, source recovery and original source reevaluation.'}
(OUT/'report.json').write_text(json.dumps(report,indent=2)+'\n')
print(json.dumps(report,indent=2))Final validation: 6,892 workspace runtime tests and 148 library doctests passed; formatting, all-feature Clippy, Please kindly check the following items (PR #1193):
Join the discussion on Zulip. |
Normalize the input (common anchor letters, drop strings containing the filtered anchor, dedupe), then build a reward-anchored graph with one reward vertex per slot. Use the match-tuple graph instead only when it has neither more vertices nor more edges, so one explicit polynomial bound over registered parameters covers both branches: V <= L(k+T-L), E <= A(S-A) + L(k-1), A = L(L+1)/2. Both encodings share one decoder. Drop the rule-internal anchor_matching_pairs and cross_frequency_product parameters, restore the generic unavailable-field CLI test on another path, and rewrite the paper entry for the new construction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
isPANN
marked this pull request as ready for review
October 12, 2026 15:53
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Keep small LCS conflict graphs while bounding repeated-symbol expansion by a polynomial. The previous polynomial encoding inflated the canonical example to 124 vertices; the final construction restores its six-vertex tuple graph and reduces 64 copies of
AAto two isolated vertices.Remove duplicate strings and strings containing the shortest input string, filter impossible letters from that anchor, and remove constraints containing the filtered anchor. Keep the common-symbol set fixed so pruning cannot revive an unavailable letter. Count common-symbol tuples only up to the anchored vertex cap, before allocating any Cartesian expansion. When tuples fit, choose the smaller graph by vertices plus edges, with tuple ties preferred; clearly smaller tuple graphs skip constructing a second candidate. Otherwise use the anchored encoding. There are no new dependencies or CLI options.
For the first shortest input string of length
L,koriginal strings, andFequal-symbol position pairs against that string:V ≤ B = L(k+2)+FandE ≤ B², withF ≤ L(T−L)for total lengthT.L'*k' + LCS, whereL'is the filtered anchor length andk'counts retained strings. Every target optimum decodes optimally, including optima with missing embedding groups; partial twin pairs are rejected.anchor_matching_pairsis cached and recomputed on deserialization. The exact MVC relation isF=2M(N−1), givingB=3N+3MN−2M. The original K3SAT→DecisionMVC→MVC→LCS→MIS path has quadratic vertex and quartic edge upper bounds after substitutingN=2n+3m,M=n+6m; neither field is unavailable.Both constructions and the selection rule have independent mathematical verification, exact graph crosscomparison against Rust, real target solves, and source witness checks. The paper describes the construction, missing-group proof, extraction, selection tradeoff, and composable upper bounds.
/simplifyreuses the model's subsequence helper and one shared anchored builder.Validation:
make paper, and full workspace instrumented coverage passed. LCS→MIS coverage: 96.93% lines, 97.76% regions.Complete constructor/adversary scripts, proof, actual Rust/corpus reproduction and a fresh review report are recorded in the PR conversation.
Known limits: selection minimizes representation size among these admitted constructions, not solver runtime or all possible reductions. It may trade additional vertices for substantially fewer edges. No large-instance solver benchmark or full composed SAT corpus sweep was performed. Existing LCS→MIS routes, bundles, and witnesses need regeneration because the parameter schema and encoding changed. The unchanged ignored macro doctest at
problemreductions-macros/src/lib.rs:211remains a known local gate failure.