polynomial_time_3sat_algorithm
plain-language theorem explainer
Given the hypothesis for n variables, the result guarantees an algorithm that solves 3SAT exactly for any ProgramTarget n by returning a satisfying assignment or none. Complexity researchers examining SAT encodings through cellular automata or backpropagation would reference this when deriving deterministic polynomial-time procedures. The proof applies the hypothesis directly as a term.
Claim. Let $h$ be the hypothesis for natural number $n$. Then for any program target with $n$ variables there exists an algorithm mapping CNF formulas on $n$ variables to optional assignments such that satisfiable formulas map to a satisfying assignment and unsatisfiable ones map to none.
background
The module develops backpropagation for SAT problems using assignments as Boolean functions on variables. CNF formulas are lists of clauses evaluated by checking all clauses under an assignment. Satisfiability asserts existence of an assignment making the evaluation true. Upstream, the step function from cellular automata applies local rules to tapes, while RSatEncoding defines assignments for encoding. In the local setting, backpropagation states are built from total assignments to enable propagation under invariants for SAT completeness.
proof idea
This is a one-line wrapper that applies the hypothesis directly.
why it matters
The theorem demonstrates that the hypothesis for a polynomial time 3SAT algorithm suffices to produce the desired decision procedure. It forms part of the completeness argument in the SAT module, linking to backpropagation and isolation results. No downstream theorems are listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.