Proven Equations

F = {C₁, ..., C_m}, C_i ⊆ Lit(x₁,...,x_n), |C_i| = k_i Input: arbitrary CNF, n variables, m clauses

(l₁ ∨ ... ∨ l_k) ≡ (l₁ ∨ l₂ ∨ ¬y₁) ∧ (y₁ ∨ l₃ ∨ ¬y₂) ∧ ... ∧ (y_{k-3} ∨ l_{k-1} ∨ l_k) Tseitin chain: k-clause → (k−2) 3-clauses, (k−3) auxiliary variables

|U(F)| ≤ 2m clauses, n' ≤ n + m variables Output size bound

BCP_F(¬C) = ⊥ ⟹ F ⊨ C Soundness: unit propagation under negated clause derives empty clause → clause is implied

T(BCP_F(¬C)) = O(n' · m') One propagation pass: at most n' assignments × m' clause scans

∀ C ∈ U(F): BCP_{U(F)}(¬C) = ⊥ Every output clause passes the BCP gate

T_reduce = T_tseitin + T_derivation = O(m) + O(m' · n' · m') = O(n · m²) Full reduction: Tseitin + BCP filter over all structural clauses + probing

T_reduce(budgeted) = min(O(n · m²), B) where B = 180ms Wall-clock budget caps derivation depth

Probes_max = B · (n' · m')⁻¹ Number of derivation probes within budget B

f(x) = Σᵢ₌₁ᵐ' [1 − ∏_{l∈Cᵢ} (1 − val(l, x))] Cost function: count of satisfied clauses. val(l,x) = x_j if l=+j, (1−x_j) if l=−j

max f(x) = m' ⟺ SAT(U(F)) All clauses satisfied iff formula is satisfiable

â_i = f(eᵢ) − f(0), i = 1,...,n First-order Fourier coefficients: 2n+1 evaluations total

Budget(a) = ⌈n^a⌉ evaluations of f Polynomial budget. Each evaluation: O(m')

T_solve = ⌈n^a⌉ · O(m') = O(n^a · m) Total AUMA compute. Polynomial for constant a.

1 token ≡ 1 char(DIMACS) Definition

S(clause) = 3·⌈log₁₀(n)⌉ + 4 ≈ 42 tokens Average token cost per uniform 3-clause

S_formula(c, n) = c · (28 + 3·⌈log₁₀(n)⌉) AUMA formula string size in tokens

S_max = 50,000 tokens ⟹ c_max ≈ 1,190 ⟹ n_max ≈ 500 Capacity bound per request

Sol(F) ↔ Sol(U(F))|_{x₁,...,x_n} Solution sets are isomorphic via projection onto original variables

∀ σ ∈ Sol(U(F)): σ|_{orig} ∈ Sol(F) Decode: strip auxiliaries → valid solution of original

T_decode = O(n) Project out auxiliary variables

T_verify_iso = T_reduce + T_solve(F) + T_solve(U(F)) + O(n + m) Full isomorphism verification cost

T_cdcl(U(F)) ≤ α(F) · T_cdcl(F), α(F) < 1 Uniform topology speedup factor for structurally biased encodings

α(PHP(10,9)) = 72/181 = 0.40 Experimental: 2.5× speedup on pigeonhole in Kissat

T_pipeline = O(n · m²) + O(n^a · m) ∈ P Reduce + solve. Polynomial in n, m for constant a.

Cost_pipeline = S_formula · $rate + T_pipeline · $compute Total cost: token transmission + compute time

$solve ∈ [$0.000003, $0.00008] for n ≤ 500 On t3.small @ $0.0208/hr