III.D34 — τ-CDCL Architecture

Constructive solver for τ-admissible 3SAT: (i) ABCD encoding, (ii) CRT decomposition into prime-level sub-instances, (iii) per-prime exhaustive search O(pᵢ), (iv) reconstruction via R_k. Total time polynomial in n for bounded interface width. Gadget library: Wire, AND, OR, NOT, Copy.