Native polynomial-time explicit relation tables #
The alphabet is the infinite type CSP.Table: every active relation is supplied as an explicit
list of rows. No finite-alphabet lookup or assumed solver appears in these certificates.
encTable frames the binary arity before the doubly framed Boolean rows. Indices and variable
names are binary; list traversal counters are unary. Contraction ranges over the explicit
reference row, so malformed huge binary arities do not cause huge loops.
Exactly-one generation takes a scope list, whose length pays for its quadratic output. This is polynomial in that list's framed encoding, not in a binary arity supplied alone. The bounds below charge actual framing, binary arity and binary names. They are explicit encoding calculations for the Section 5.3 update in [KKR18]; they do not assert the paper's full solver or its combinatorial instance-size estimate.
A table's binary arity, framed, followed by its framed list of framed Boolean rows.
Each Boolean row bit uses three bits under encList encBool; each row is framed again.
Instances For
Reading the binary arity is a projection of the encoded field tuple.
Reading all rows preserves their actual doubly framed Boolean encoding.
Scanning a table for width errors is native polynomial-time, with binary arity.
Native row membership uses an actual scan of the supplied row table.
Binary coordinate lookup charges only the binary index, even beyond the row's end.
Counting deviations scans binary positions and uses bounded binary lookup.
Validate positions without expanding their binary values into unary indices.
Enumerating outside positions is polynomial in the unary width and binary selection list.
Local contraction, including malformed cases, is native polynomial-time in actual input bits.
One-hot row generation uses unary width and index.
Exactly-one generation is polynomial in the framed scope list, with binary variable names.
Exact full encoded table size, including binary arity, bit framing and row framing.
At least two distinct internal coordinates make the full encoded local table no larger, including its binary arity. This is a local bound, not a whole-solver complexity theorem.
Replacing any sublist of old names by that sublist followed by one binary connector name costs at most the connector's full framed name. Table framing is included twice by the enclosing constraint encoding. The caller supplies the outside scope and proves its sublist property.
Exactly-one's full encoded size is quadratic in the connector count, with binary arity.
Actual binary constraint size includes every supplied variable name, in addition to the quadratic exactly-one table.
A concrete quadratic bound in the actual framed binary scope encoding. This resource pays for both the quadratic table and the binary names; binary arity alone would not suffice.