A small vertex cover permits native constraint recognition
5 October 2026. Written native construction, independently audited.
For every fixed bound on vertex-cover size, arbitrary-order unary and binary constraints over a fixed finite domain have a native scaffold recognizer. The recognizer checks the graph restriction itself. The cover is not supplied, and components may contain arbitrarily many variables.
The mechanism is a growing set of selected variables. Once their values are fixed, every remaining variable can be treated independently. The important dynamic fact is that a newly selected variable has no earlier neighbors outside that set: promotion never requires a scan of old leaves.
Contents
Exact theorem
Written recognition theorem. Fix a nonempty finite domain D, a finite constraint language Γ of unary and binary relations on D, and an integer k≥0. There is one deterministic native scaffolding automaton recognizing exactly the ordinary finite-alphabet records that (i) are well formed, (ii) are jointly satisfiable, and (iii) have loopless primal graph of vertex-cover number at most k.
A unary record is U(w); and a binary record is B(u,v);, where the relation tag belongs to the fixed finite alphabet and every variable name is a nonempty literal binary word. Different tags may be represented by distinct alphabet symbols. A binary record with distinct names adds the undirected edge {u,v} to the primal graph, even when its relation is full; repeated edges are ignored in the graph. A repeated-name record B(u,u); adds no graph edge and imposes the diagonal unary restriction {a:(a,a)∈B}. Unary records add no edges. The empty conjunction is accepted. Invalid words are rejected. Nothing supplies a cover, order, handle, padding, or advice.
The machine constants depend on D, Γ, and k, not input length N or number b of distinct names. Names and every delimiter count toward N. Initialization is fixed. The machine reads forward and decides at the last input symbol, with no extra final computation. It uses the exact native fixed degree/radius/finite-label model. This statement does not claim a single fixed automaton when k is part of the input.
Imported implementation component
The proved finite-payload dictionary, with its arbitrary finite update extension, gives a serial immutable dictionary indexed by all nonempty binary words, with any fixed finite terminal payload and any fixed finite payload-update map. A name bit performs bounded pointer work. At the terminating delimiter, the current payload can be read and replaced; the path is committed through FIFO capsules, and traversal resets in the same bounded batch. Prefix-related and repeated names work. The payload map is not restricted to monotone intersection.
We use finitely many such dictionaries in parallel, and copy their root/cursor handles when starting a finite speculative branch. All handles are already in the current bounded header. We never compare pointer identity or inspect an address. Copies share immutable old nodes, while all new nodes on dead branches remain charged. Product control and the established bounded-batch native compilation apply because the total number of live and temporary branches below is a constant.
One stable branch: selected centers and finite elimination
A stable branch has t≤k ordered selected centers C=(c₁,…,c_t). Their names are NOT stored or compared in finite control. The dictionary terminal of c_i has permanent role Center(i). Every other terminal has role Leaf. Within a branch a name is promoted at most once; centers are never demoted or renumbered.
Each terminal stores a finite payload:
- a role Leaf or Center(i), plus a temporary Mark role used only inside one record;
- M_x⊆D, the intersection of unary restrictions seen on that variable (default D);
- B_x[i]⊆D×D for i=1,…,k, default D×D;
- marker bits A_x[i]∈{0,1}, initially 0, for i=1,…,k.
For a leaf x, B_x[i] is the intersection of the binary restrictions between x and c_i, always oriented as (leaf value, center value). The actual relation tag and endpoint order determine whether its relation or transpose is intersected. Unused slots i>t have full B_x[i]. Marker bits in already occupied slots are semantically inert. Marker bits in all unused slots are zero in every stable branch.
The control also stores a finite table R⊆D^t. For a center assignment a define
The invariant is that C covers every processed nonloop edge, the dictionary stores the indicated leaf restrictions, and R is exactly the set of center assignments extendible to a solution of the processed conjunction. Equivalently, R is the conjunction of all center-only constraints and all independent leaf predicates Φ_x. Leaves cannot have old edges between each other because C covers the processed graph. Center payload incidences may remain dormant after promotion: their old information is already included in R.
An ordinary restriction update on a leaf shrinks P_x. It therefore updates R to R∩{a:Φ_x^new(a)}. There is no need to remove the old Φ_x because the new predicate implies it. A unary restriction on a center or a binary restriction on two centers directly intersects R with the relevant coordinate predicate. These are finite table maps.
Promotion lemma
Suppose x is a leaf and t<k. Make it center j=t+1 and set
Set the terminal role of x to Center(j). This exactly represents the same formula with a larger selected cover. Indeed, the old formula factors into its center constraints, the factors for leaves other than x, and ∃z P_x(z;a); replacing the last existential factor by its displayed value gives the claimed table. Every old neighbor of x lies in C, so no other leaf has an old edge to the new center and no other terminal needs updating. Unused incidence slots of those terminals remain full. This observation is the essential no-scan property.
Deterministic speculation for a binary record B(u,v)
The relation B is known before either name. Read u under each stable branch. At the comma, terminal access and all updates below are bounded finite operations. A temporary branch then reads v from its updated dictionary. Every hypothesis is validated at the terminating delimiter of v; no prediction survives to the next record without validation.
First endpoint is already Center(i)
There is just one temporary plan. At v’s terminal:
- If its role is Center(j), intersect R with {(a):(a_i,a_j)∈B}. This includes i=j, so a repeated-name record is handled by its diagonal.
- If its role is Leaf, intersect B_v[i] with Bᵀ, update the terminal, and intersect R with its new Φ_v.
No promotion or cover split occurs. Role Mark cannot occur in a stable branch.
First endpoint is a Leaf
Start the following finite candidate plans, all from the old stable branch. The first-name update is committed in the candidate dictionary before reading v.
Existing second-center i, one candidate for each i≤t. At u, replace B_u[i] by B_u[i]∩B and intersect R with the new Φ_u. At v require role Center(i), otherwise discard. No further relation update is needed. Exactly one of these plans can validate.
Select the first endpoint, only if t<k. At u, apply the promotion lemma, with j=t+1. At v require role Leaf, otherwise discard. Then intersect B_v[j] with Bᵀ and impose the new Φ_v. The role test rejects old centers and also rejects u=v because the first update made that same terminal Center(j).
Select the second endpoint, only if t<k. Reserve j=t+1 and provisionally extend the table to R×D. At u, set A_u[j]=1, replace B_u[j] by B_u[j]∩B, and impose the resulting Φ_u using all t+1 coordinates. At v require role Leaf and A_v[j]=0, otherwise discard. Then bind the reserved coordinate z=a_j by intersecting with
, using only the old occupied slots ,
and set v’s role to Center(j). All unused-slot markers were zero before this record; only u was marked in this candidate. Thus the marker check is exactly the required u≠v check, without pointer identity or stored-name comparison. After this candidate survives, j is permanently occupied, so A_u[j] is ignored forever. It need not be reset. Future reserved slots are larger and still have zero markers.
The provisional table was R(a)∧Φ_u^new(a,z). Binding z to v’s old leaf predicate removes the existential freedom of v exactly as in the promotion lemma. Its previous existential predicate already in R is redundant under that binding. Since v≠u and both were old leaves, there was no old edge between them. This is therefore exactly the old formula plus B(u,v), with v promoted.
Repeated endpoint, one candidate. At u change its role to Mark and otherwise preserve the payload. At v require role Mark; no other terminal was marked in this candidate, so this validates exactly u=v. Intersect M_v with diag(B)={z:(z,z)∈B}, restore role Leaf, and impose its new Φ_v. If the second name differs, the candidate dies and its unreverted marker remains only in inaccessible dead history.
The use of explicit marker bits in plan3 is necessary for general binary CSP: testing whether its new incidence slot changed would fail for a full incoming relation. Temporary role Mark in plan4 is safe because the first and second accesses are functional updates of the same dictionary; no old node is mutated.
Exact survival classification
For first role Leaf there are only three actual cases:
- v is an old center: precisely its existing-center plan validates; both promotion plans reject its role, and the repeated-endpoint plan rejects.
- v is u: precisely the repeated-endpoint plan validates. The select-first plan sees the promoted center; select-second sees its fresh marker; existing-center plans see a leaf.
- v is a different old leaf: precisely the two promotion plans validate if t<k. Existing-center plans and the repeated-endpoint plan reject. If t=k, no plan survives.
Thus a covered edge never causes an extra stable branch; a loop never consumes cover budget; an uncovered nonloop edge causes exactly the two ordinary vertex-cover choices, each spending one unit. Empty semantic tables may be discarded at any time: adding constraints cannot restore their feasibility.
Unary records and syntax
For U(x), intersect M_x with U. If the role is Leaf impose its new Φ_x; if Center(i) restrict R to a_i∈M_x. Pin-only and isolated names are included, so inconsistent unary restrictions on an unused name still reject. For binary loops the diagonal update already has the same effect.
A finite parser checks tag, punctuation, nonempty name fields, and complete records. Candidate validation, dictionary commit, and reset occur at the relevant name-ending delimiter in a bounded batch. The semicolon completes the parser state. The machine accepts exactly complete-record parser states with at least one surviving branch having nonempty R. There is no traversal or calculation after the last input symbol. The empty conjunction has one branch t=0 and R={()}.
Cover completeness and bounded width
Fix any vertex cover C* of the final primal graph of size at most k. Follow a branch whose selected set is contained in C. For an uncovered nonloop edge, at least one endpoint belongs to C, and choosing that endpoint preserves containment. A new selected endpoint cannot already belong to the selected set, because the edge was uncovered. Hence this path never exhausts the budget prematurely. If the conjunction is satisfiable its restricted center assignments always leave R nonempty. Conversely, every surviving branch has selected a genuine cover of all processed edges and R nonempty precisely when the processed conjunction is satisfiable. This proves exact language recognition.
The stable branching bound holds over arbitrarily many records, not merely one edge. Give a stable branch with t centers weight 2^(k−t). Initially total weight is 2^k. An uncovered nonloop edge replaces one depth-t branch by at most two depth-(t+1) branches, preserving or decreasing total weight. Covered edges, unary records, and loops leave its depth unchanged and do not duplicate it. Discards decrease weight. Every branch has weight at least one; therefore at most 2^k stable branches exist at every record boundary.
A first-leaf record has at most t+3≤k+3 temporary plans per branch. A first-center record has one. Therefore temporary width is at most (k+3)2^k. At each second-name delimiter, all invalid plans die and surviving slots are compacted by a finite permutation of the bounded header. No global search, pointer comparison, or variable-size queue of branches is needed. Duplicate selected covers reached through different histories are allowed; the potential bound already counts each history separately.
Resource and hostile-input audit
For fixed parameters, terminal payloads, t, relation tables, plans, parsing flags, and branch slots are finite. Each symbol advances at most (k+3)2^k native dictionary clients, each having fixed bounded pointer radius, degree, fresh allocation, and number of cursor/header roots. At field delimiters only finite payload and table maps and bounded handle copies occur. This gives fixed constants q_{D,Γ,k}, r_{D,Γ,k}, A_{D,Γ,k}, s_{D,Γ,k} for the established bounded-batch compiler. All of these constants depend only on the fixed domain, relation language and cover bound. The reviewed simultaneous-record compiler gives one newly allocated native node per symbol, N+1 nodes including initialization, and O(N) bounded-record words/O(N log(N+2)) pointer bits; source logical history is O_{D,Γ,k}(N), including all dead speculation. No preprocessing of the particular word occurs.
Hostile late short names do not cause center scans or representative walks: the terminal directly says which permanent center slot, or stores the bounded interaction profile of a leaf. Huge stars and arbitrarily many leaves are allowed. A leaf promoted late can have arbitrarily many prior edge occurrences, but their intersections with the at most k old centers are its finite payload; the promotion lemma reads that payload only. All leaf interactions with old centers are already reflected in R, so a late pin can reject immediately by a finite-table change. Repeated names, prefix names, opposite orientations, duplicate edges, self-loops, isolated pins, and conflicting multiple relations are covered by the explicit transition cases. This solves the present bounded-cover family, not unrestricted equality component access.
Scope and consequence
In particular, for each fixed k, ordinary signed equality/pin SAT and ordinary implication/2SAT with primal vertex-cover number≤k have native recognizers, with the graph restriction checked by the recognizer. The family has arbitrarily many names and unbounded component sizes. It is not a bounded-size instance control or a decomposition supplied in the input. The unrestricted implication obstruction remains compatible: it ranges over graphs with unbounded cover number.
The semantic elimination and two-way vertex-cover branching are standard ideas. The added implementation content is maintaining an unsupplied cover under serial ordinary names, immutable local access and the exact final-symbol deadline. Finite terminal-update hypotheses resolve the endpoint-order problem; permanent center roles and the promotion lemma resolve the history problem. The proof is written, not formally verified.
Both input orientations and PEGs
A direct reversed-record construction gives both orientations. A reversed binary record has the form ;)rev(v),rev(u)(B, and a reversed unary record ;)rev(u)(U, where each fixed relation tag is one alphabet symbol. At the opening semicolon run finitely many hypotheses for the relation tag and arity. Read the literal reversed names with the same dictionary; use the transposed binary relation because the argument order has reversed. Validate punctuation and the actual tag at the final symbol of the record, discarding every incorrect hypothesis. Name reversal is a bijection on nonempty binary words, and reversing the order of conjuncts changes neither satisfiability nor the primal cover number.
At record boundaries only the unique correct tag/arity hypothesis survives. Within a record there are at most times as many plans as before, still a fixed constant (if the language is empty, only the empty word is valid). The final tag completes finite validation; no extra EOF step occurs. Malformed reversed records reject. Thus both the language and its string reversal are native. By Loff–Moreira–Reis, Theorem16, both also have PEGs. No general reversal closure is assumed.
Closest prior work and the next structural test
Bodlaender–Groenland–Pilipczuk, ICALP2023, Theorem1 and §3 Lemma8/Claim9, studies Binary CSP parameterized by vertex-cover number. Its hardness construction uses input-sized domains. Our domain and cover bound are fixed in the machine, and our question is strict serial recognition. The cover/independent-set factorization is familiar; parameterized tractability alone does not supply this native implementation.
Chitnis–Cormode–Hajiaghayi–Monemizadeh, §2 and §3.1–3.2, Theorem6 (pp.6–8 of the linked version), studies parameterized vertex cover in graph streams. Its insertion-only result maintains a small kernel and extracts a cover; this is a useful classical streaming control. Here all current feasibility information is kept in finite control while literal names arrive, so extraction at the end is unnecessary. Our proof uses the elementary two-endpoint branching rule directly and charges dead immutable history rather than claiming a small-memory kernel.
This result is an extension of standard structural CSP and vertex-cover methods with an explicit native realization, not a new offline tractability criterion. The strongest next test is whether a comparably strict representation can handle residual components that interact with one another, rather than independent leaves. Unrestricted equality remains open; an arbitrary unsupplied tree decomposition is not available for free. Compare this positive result with the unrestricted propagation obstruction and the unique late-value prediction control.
The independent review checked the actual transition plans and both input orientations. A separate finite program exhausts two-record Boolean examples and tests longer hostile streams against brute satisfiability and vertex-cover enumeration, including repeated full-relation self-loops. These corroborate the semantics; they do not verify the native compiler or prove the unbounded theorem.