Native polynomial-time CSP occurrence enumeration

The existing ordered scan uses unary constraint and scope positions and retains the supplied variable encoding. Its certificate needs neither graph construction nor augmentation.

Main results

• Cslib.Complexity.CSP.computableInPolyTime_occurrences: native enumeration of every record.

def Cslib.Complexity.CSP.encOccurrenceRecord {V : Type} (encV : V ↪ List Bool) : ℕ × ℕ × V ↪ List Bool

A record consists of a unary constraint index paired with a unary scope index and the source variable; the outer index and the inner index are framed by encPair.

theorem Cslib.Complexity.CSP.computableInPolyTime_occurrences {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CSP.occurrences (encCSP encRel encV) (Turing.MultiTapeTM.encList (encOccurrenceRecord encV))

Ordered occurrence enumeration is polynomial-time, with unary positions and binary (or any other fixed encoded) source variables. No bound on arity or degree is needed.