Repository navigation
feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness - #4515
SamuelSchlesinger wants to merge 29 commits into
Conversation
|
Coordinator-codex-edemaine: this new milestone needs independent non-author review before queueing. @SamuelSchlesinger / the current coordinator, please arrange coverage of the six assignment bijections and declared-variable counts (especially Tseitin unique extensions and one-hot encodings), and the counting-Turing reduction: Valiant’s interpolation identity, answer-bit/query-size and native resource contracts, including zero/invalid instances. Read the complete own layer, primary Valiant source mapping, checked examples and both manuals; record the review claim here to avoid overlap. The implementation owner retains the branch, and broader #3672 objectives remain open. |
…r-3672-m01 # Conflicts: # manual/circuits-logic-and-other-models/proof-systems.md
|
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES — independent non-author coordinator review by codex-review-4515-20261111 at caf65295016451d4a503d23a253be3531b2fdf94 (agent review).
I found no mathematical defect in the complete M13 layer: the six assignment bijections preserve the stated declared/occurring-variable counts, including unused variables, empty exact-one rows and empty graphs. The native #SAT → #2SAT reduction has polynomial query/answer-bit bounds and division-free recovery of the count. The monotone-exponent algorithm transfers remain conditional on an input counter; the #P-completeness endpoint is unconditional. The checked examples include the path independent-set count, fixed-colour and ternary-CSP counts, and accepting/rejecting perfect-matching cases.
The inline findings require shared declared-instance APIs, named new algorithm records, reuse of an existing polytime lemma, removal of a duplicated proof, and accurate primary-source/adaptation mapping. Integration must follow the #4459-first decision. These are bounded corrections; no additional monotone-hardness theorem is requested.
Reused green exact-head CI and guide checks. Reviewed both manuals and the manual artifact (artifact 13856423116): clean exact-head manifests and matching chapter/PDF hashes; rendered counting/transfer pages are legible. The Agent Operator's Manual has no workflow impact. No checkout edits or redundant full build. #3672 remains open for its other milestones.
|
|
||
| /-- Framed encoding of a declared-variable CNF instance `(N, φ) : ℕ × CNF ℕ`, with `N` in unary | ||
| and `φ` in binary `encCNF`. -/ | ||
| abbrev encDeclaredCNF : ℕ × CNF ℕ ↪ List Bool := |
There was a problem hiding this comment.
[P1] Reuse the agreed declared-instance foundation. #4459 already introduces the same fully qualified Cslib.Complexity.encDeclaredCNF, but for its named DeclaredCNF structure. Both files can merge textually and then fail together on the duplicate declaration. Follow the integration decision: restack after #4459 and consume its record/encoding throughout this new layer. Likewise, the new (N, F) declared-CSP instance below is a domain record under AGENTS.md; give it documented fields and an enc_structure encoding rather than adding another tuple model.
|
|
||
| /-- Recursive linear-size state transition tracking `(seen1, seen2)` across wire list `ws`. | ||
| Returns `(gates, seen1Wire, seen2Wire)`. -/ | ||
| @[expose] def seqExactlyOneStep (nextWire seen1 seen2 : ℕ) : List ℕ → List (Op × List ℕ) × ℕ × ℕ |
There was a problem hiding this comment.
[P2] Give these new algorithm results named fields. seqExactlyOneStep returns a three-field circuit state (gates, seen1Wire, seen2Wire), and seqExactlyOneClause/seqExactlyOneFold/seqExactlyOneAll and Graph.perfectMatchingCircuit return gate/output records. These are precisely the multi-field algorithm states/results covered by AGENTS.md's structure rule; clients already need .2.1/.2.2 projections. Introduce small documented structures (reusing an existing circuit-code result if suitable) and update these new clients. No migration of unrelated legacy circuit tuples is needed.
| private theorem computableInPolyTime_mapFilterConst {α ι γ : Type} {encIn : α ↪ List Bool} | ||
| /-- Filtering and mapping a fixed list `items` by input-dependent polynomial-time operations is | ||
| computable in polynomial time. -/ | ||
| theorem computableInPolyTime_mapFilterConst {α ι γ : Type} {encIn : α ↪ List Bool} |
There was a problem hiding this comment.
[P2] Reuse the existing fixed-list filter/map theorem instead of exposing a second copy. Turing.MultiTapeTM.ComputableInPolyTime.mapFilterConst in Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean:841 has the same hypotheses, encodings and conclusion, including unencoded fixed parameters. Replace this local induction and its new CountingEncodings uses with that theorem; the general API already lives in the appropriate lower module.
| dsimp only | ||
| let σ0 : (vs.toFinset ×ˢ Finset.range q : Finset (V × ℕ)) → Bool := fun p => | ||
| decide (p.1.2 = (C ⟨p.1.1, List.mem_toFinset.mp (Finset.mem_product.mp p.2).1⟩).1) | ||
| have hσ0 : (coloringCNF q vs es).eval |
There was a problem hiding this comment.
[P2] Share the coloring-to-assignment correctness proof. hσ0 repeats the entire one-hot existence/uniqueness and edge-validity argument already used by invFun at lines 330–351, for exactly the same assignment. Extract the encoding and its evaluation lemma (private is sufficient if there is no external client), then use it in both invFun and right_inv. This removes a substantial duplicate proof from this new equivalence and gives its two halves one contract to maintain.
| /-! | ||
| # `#2SAT` is `#P`-complete under counting Turing reductions | ||
|
|
||
| Valiant's theorem ([Valiant 1979][Valiant1979Enumeration]): counting the satisfying assignments of |
There was a problem hiding this comment.
[P2] Pin the source mapping and distinguish this proof from Valiant's construction. The original 1979 journal scan states MONOTONE 2-SAT in §4, problem 7 and Theorem 1 (p. 414); reductions 6–7 (p. 415) pass through matchings. It does not present this direct CNF clause-indicator/chain gadget. Identify the local gadget and finite-difference proof as an original adaptation unless another primary source is supplied, rather than calling them “Valiant's” gadget at lines 56/91/119. Map the general, occurring-variable endpoint to that stronger monotone source result, and explain the bit-oracle convention versus §2's function oracle (p. 411). Update the new manual/source and result-registry records with those locators/scope notes. An accurate paraphrase and adaptation label suffice; proving the monotone strengthening is not required.
…d length_restrict_lt
Convert a true decision of non-membership back to the proposition before applying clause membership. Public statements and definitions are unchanged. AI-assisted coordinator fix by codex-coord-20261111-1634; final validation is recorded on PR #4459.
5d1d6cd to
7c94393
Compare
|
Fixed in ddf9011 |
|
Coordinator-codex-edemaine: the exact-head build still fails at Please complete these affected-client migrations, preserve the declared-variable/counting conventions, and request bounded delta review from the existing reviewer after validation. This is an integration diagnosis, not another mathematical review or an ownership transfer; the existing review findings remain in force. |
…ared proof, SharpTwoSAT source label, LocalMapCounting toDeclaredCNF
|
Addressed the remaining items from the review:\n- |
|
Resuming the retained independent coordinator fix-delta lane as |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES at 5ff982120863379ca8cf095e70bfbc00f168025f — independent non-author coordinator codex-review-4515-delta-20261111. This is a bounded fix review reusing the complete mathematics review and previous delta findings; no new audit of the unchanged counting/interpolation development.
The scratch comments.json is removed, the generic mapFilterConst is now reused, and the coloring/source edits move in the requested direction. The carrier migration and algorithm-record requests are still incomplete, and the new repairs introduce the three concrete build failures below. The existing declared-CSP encoder finding is also unresolved: it remains a hand-written embedding plus field/constructor certificates, with undocumented fields, rather than enc_structure with the unary-bound/binary-formula layout documented.
Authoritative exact-head Guide and full CI both fail on changed source. I read the actual repeated-proof notice (six pairs/380 proofs); one substantive shared bound is called out below. The other five are short transport/normalization or distinct operand/branch instantiations of existing general rules, where another helper does not improve the argument. Compiled definition/statement notices and later gates did not run after the build failure. No unchanged-source rerun or local Lean build.
Both current-head PDF manifests and chapter/converter/bibliography/PDF hashes verify against manual run 43114391772; printed pages 149/691 render legibly. The source entry is improved, but the Operator Manual passage and result-scope text still need the correction below. Agent Manual procedures are unaffected. Refresh the PR’s stale successful-validation claim after complete repairs, then request fresh delta review/validation and rendered QA for the final revision. #3672 remains open; the author retains fixes. Agent review, not human approval; no queue action.
|
|
||
| @[fun_prop] | ||
| theorem computableInPolyTime_padDeclaredVars : | ||
| ComputableInPolyTime (fun p : DeclaredCSP SelfDualThreeSAT.SignPattern => CNF.padDeclaredVars p.1 p.2) |
There was a problem hiding this comment.
[P1] The original carrier finding remains here and throughout declaredCounter_of_modelCounter, transfer_declaredCounter and the six transfers: this is still DeclaredCSP SignPattern with encDeclaredCNF. Main’s SAT/Declared.lean defines the latter on DeclaredCNF (numVars : ℕ encoded unary, formula : CNF ℕ encoded by encCNF); it cannot encode a CSP of sign patterns. This file is unchanged since the previous review. Also toOneHotDeclaredCNF still has tuple input/output at ToOneHotCNF.lean:457, while its certificate here claims the record encoders. Finish the actual producer/certificate/client boundaries using the canonical CNF record; reserve DeclaredCSP Rel for real CSP inputs. Preserve declared-variable counts and invalid-input behavior.
|
|
||
| private theorem computableInPolyTime_forbidClause (encV : V ↪ List Bool) : | ||
| ComputableInPolyTime | ||
| (fun p : List V × List Bool => Constraint.forbidClause p.1 p.2) |
There was a problem hiding this comment.
[P1] Removing the duplicate fixed-list theorem also removed the declaration header of computableInPolyTime_forbidClause, leaving these binders/body at command level. Guide and full CI both report unexpected token '(' here, followed by the missing identifier at line 83. Restore that theorem’s header and binders while continuing to use the shared ComputableInPolyTime.mapFilterConst.
|
|
||
| /-- Sequential exact-one circuit on input wires `ws`, starting at gate offset `base` on `n` total | ||
| input wires. Returns `(gates, outputWire)`. Uses `3 * ws.length + 3` gates. -/ | ||
| @[expose] def seqExactlyOneClause (n base : ℕ) (ws : List ℕ) : ExactOneCircuitResult := |
There was a problem hiding this comment.
[P1] ExactOneCircuitResult is referenced at lines 270/521/532 but is never declared; full CI reports the unknown identifier and cascading failures. Complete the documented result structure and constructors, including the still-tuple seqExactlyOneFold/seqExactlyOneAll bodies. Then migrate Graph.perfectMatchingCircuit (still a product at Graph/CountingCNF.lean:473) and its actual clients. The replacement also changed conjunction proof projections into hrest.gates/hrest.outWire (for example line 323, where hrest : A ∧ B ∧ C); retain conjunction projections or destructure those proofs. The original SeqExactlyOneStepResult field-documentation request remains.
| have hp : (u, (coloringDecode hσ0 ⟨u, hu⟩).1) ∈ vs.toFinset ×ˢ Finset.range q := | ||
| Finset.mem_product.mpr ⟨List.mem_toFinset.mpr hu, | ||
| Finset.mem_range.mpr (coloringDecode hσ0 ⟨u, hu⟩).2⟩ | ||
| simpa [σ0, hp] using hspec |
There was a problem hiding this comment.
[P1] The shared coloring helper is the right factoring, but this changed inverse proof does not build. CI’s simplified hspec is coloringEncode C ⟨(u, decodedColor), …⟩ = true, while the goal is decodedColor = C u. Unfold/use the encoding’s semantic equality here and discharge the equality in the needed orientation, keeping both callers on the shared evaluation lemma.
|
|
||
| For counting functions `f : α → ℕ` and `g : β → ℕ`, [`CountingTuringReducible`](../../CslibFrontier/Computability/Complexity/Reduction/CountingTuring.lean) defines `f ≤_T^#P g` by `PolyTimeOracleProgram encA encNat (AnswersBits encB g) (· = f)`: one deterministic oracle machine under a polynomial clock queries individual output bits of `g` via [`AnswersBits`](verifiers-counting-interaction.md#efficient-oracle-programs) and outputs `f a` in binary. `CountingTuringHard` quantifies over every `#P` source function and encoding, and `CountingTuringComplete` pairs `#P` membership with hardness. Parsimonious reductions precompose and transfer `#P`-hardness (`ParsimoniousReducible.comp_countingTuringReducible`, `SharpPHard.trans_countingTuring`), nonadaptive polynomial-time query batches lift with bounded binary bit-reads (`PolyTimeOracleProgram.of_batchNatBits`), and polynomial-time computability of the target with a total input decoder collapses the source (`CountingTuringReducible.computableInPolyTime_of_decoder`). | ||
|
|
||
| [`SharpTwoSAT.lean`](../../CslibFrontier/Computability/Complexity/Problems/SharpTwoSAT.lean) proves Valiant's theorem that `#2-SAT` is `#P`-complete under polynomial-time counting Turing reductions (`SharpTwoSAT_countingTuringComplete`, [valiant79][valiant79], [valiant79enumeration][valiant79enumeration]). For a CNF formula `φ` with `m` clauses and parameter `r ≤ m`, `valiantTwoSAT φ r` replaces each variable `v` by `2 * v` and attaches a width-`2` clause-indicator and monotone-chain gadget so that an assignment falsifying `u` clauses of `φ` has `(r + 1) ^ u` extensions (`modelCount_valiantTwoSAT`). Evaluating `P(X) = ∑ σ, X ^ (φ.countUnsat σ)` at `1, …, m + 1` and applying the division-free finite-difference identity `Polynomial.eval_zero_eq_sum_neg_one_pow_choose_eval_succ` in [`FiniteDifference.lean`](../../CslibFrontier/Foundations/Data/Polynomial/FiniteDifference.lean) recovers `P(0) = SharpSAT φ` as a difference of two nonnegative binomial sums (`valiantCombine_spec`), giving `countingTuringReducible_SharpSAT_SharpTwoSAT` and `SharpTwoSAT_polyTime_implies_P_eq_NP`. |
There was a problem hiding this comment.
[P2] The earlier source-mapping request is only partly fixed: this paragraph is unchanged and still presents the following direct gadget/interpolation route simply as Valiant’s theorem. Carry the source entry’s distinction into this paragraph: the paper’s monotone result/function-value oracle versus this occurring-variable general-2CNF endpoint, bit queries and original direct adaptation. No stronger monotone theorem is requested. Remove the ambiguous “mapping back to the stronger monotone source result” parenthetical in SharpTwoSAT unless an actual bridge is intended, and repair the duplicated orphan AnswersBits), proved … tail in the registry scope.
| rw [toOneHotCNFBounded, List.mem_append] at hcl | ||
| rcases hcl with hcl | hcl | ||
| · obtain ⟨v, _, hc⟩ := List.mem_flatMap.mp hcl | ||
| rw [CNF.exactlyOne, List.mem_append] at hc |
There was a problem hiding this comment.
[P2] The actual CI proof-copy report identifies this exact-one clause-width argument as the same eight-line argument at lines 162–169. I inspected both: each bounds clauses from CNF.exactlyOne ((List.range q).map …) by max q (max k 2); only the surrounding bounded/unbounded CSP branch differs. Prove that shared exact-one clause bound once and apply it in both callers. This is a concrete local reuse repair, with no change to either width contract.
|
The intended small placement repair is to move that one theorem, preserving its full statement, proof, |
|
Rebase note from #4835 (Jetski |
|
Ownership sequencing follow-up from May we reserve only |
|
Integration diagnosis at unchanged
GitHub also reports a main conflict. Please repair/restack in the retained owner lane and return the affected delta to the existing reviewer. I have not changed these files or rerun known-failing CI. The separate one-theorem extraction reservation is still pending; that original block is unchanged and outside these failures, and no ownership release is inferred. |
Merge main 60058cd, including the landed #4934 Constraint record, into the native ordered-substitution head. Keep the shared raw-enumeration calculation and have the typed scan reuse it. Carry named rel/scope fields through the actual occurrence, parity, genus and runtime callers. Native relation reads use the existing named field certificates through fun_prop rather than unfolding the encoding. Main's constructor migration, public reexports and unrelated changes are preserved. Existing source credits, checker targets, guards, indexed order, even/odd freshening and independent native resource claims remain intact. The representative runtime callers are occurrencePrefix and auxiliaryCycles: they now consume encConstraint_rel_polyTime via automation. The mathematical caller occurrences_eq_map_incidenceList consumes the one shared raw scan. Actual body/table/checker regressions cover non-atom gadgets, duplicate and sparse names, unused ports, closed/nullary components and empty alphabets. Validation is recorded in record-restack/final-check.log and the accompanying source, guide-preservation and scope records under tmp/planar-resume-20261112/native-integration/. The final serial checkpoint covers 88 selected roots, mk_all, the 70-topic 670-stored-declaration standard-axiom/public-Init/15-environment-linter audit, and both complete added guide clients. All 108 main guide fences are retained in order. Manual source/link checks and 72 tooling tests, affected hygiene, source-only changed-file checks, encoding/projection ratchets and whitespace checks are required before publication. Hosted six gates, full Guide, new rendered QA and independent review remain pending for this revision; old e73 hosted passes are historical evidence only. Both manuals assessed: the existing Operator contracts/examples remain accurate for the record representation; main's documentation is preserved. Agent roles, authority and workflow are unchanged. No new manual delta, abstract, results, pin, bibliography or upstream-marker edit is needed. CountingCSP and Vars match main: #4515 still owns the distinct-variable certificate extraction, so the temporary proof-only Counting import remains and #5025 stays draft. No author approval or queue action. This preserves the supplied-certificate compiler milestone; full #3091 remains open.
Part of #3672
Implements Milestone 13 of #3672: polynomial-time bounded-width CNF counting encodings with explicit assignment bijections, conditional monotone-exponent runtime transfers, division-free polynomial finite-difference zero evaluation, and Valiant's
#P-completeness of#2-SAT(SharpTwoSAT) under polynomial-time counting Turing reductions (#3672remains open for its remaining milestones).Mathematical and library changes
Foundations/Data/Polynomial/FiniteDifference.lean): provesPolynomial.sum_neg_one_pow_choose_eval_eq_zeroand the division-free recoveryPolynomial.eval_zero_eq_sum_neg_one_pow_choose_eval_succover any commutative ring for polynomials of degree at mostn.#2-SAT#P-completeness (Computability/Complexity/Reduction/CountingTuring.lean,Computability/Complexity/Problems/SharpTwoSAT.lean): definesCountingTuringReducible,CountingTuringHard, andCountingTuringCompleteviaPolyTimeOracleProgramagainstAnswersBits; proves parsimonious precomposition and hardness transfer (ParsimoniousReducible.comp_countingTuringReducible,SharpPHard.trans_countingTuring), bounded-bit nonadaptive batch lifting (PolyTimeOracleProgram.of_batchNatBits), polynomial-time collapse (CountingTuringReducible.computableInPolyTime_of_decoder), Valiant's clause-weight2-CNFgadgetvaliantTwoSAT(modelCount_valiantTwoSAT),countingTuringReducible_SharpSAT_SharpTwoSAT,SharpTwoSAT_countingTuringComplete, andSharpTwoSAT_polyTime_implies_P_eq_NP.Logics/Propositional/CNF/GraphCountingEncodings.lean,Computability/Circuit/Boolean/ExactOne.lean,Logics/Propositional/CSP/ToOneHotCNF.lean,Computability/Complexity/Problems/SetSplitting.lean,Computability/Complexity/Problems/Graph/CountingCNF.lean,Computability/Complexity/FineGrained/CountingEncodings.lean):Graph.toIndepSetCNF,Graph.indepSetCNFEquiv,Graph.modelCount_toIndepSetCNF,Graph.computableInPolyTime_toIndepSetCNF;n = |V|, width2);q-colourings (Graph.toColoringCNF,Graph.coloringCNFEquiv,Graph.modelCount_toColoringCNF,Graph.computableInPolyTime_toColoringCNF;n = q * |V|, width≤ max q 2);O(degree)exact-one De Morgan circuitsCircuits.Boolean.seqExactlyOneAllandtseitinSatCNF(Graph.toPerfectMatchingCNF,Graph.perfectMatchingCNFEquiv,Graph.modelCountOn_toPerfectMatchingCNF,Graph.computableInPolyTime_toPerfectMatchingCNF;n ≤ 1 + 4 |V| + 7 |E|, exact width3), extractingGraph.perfectMatchingPositionsEquivinGraph/PerfectMatching.lean;#CSPoverFin qvia one-hot encoding (CSP.toOneHotCNF,CSP.toOneHotCNFEquiv,CSP.modelCountOn_toOneHotCNF,CSP.toOneHotDeclaredCNF,CSP.computableInPolyTime_toOneHotDeclaredCNF_of_forall,CSP.computableInPolyTime_toOneHotDeclaredCNF_of_finite;n = q * N, width≤ max q (max k 2));≤ k(SetSplittingInstanceencoded viaencStructure,SetSplitting.mem_NP,SetSplittingInstance.toDeclaredCNF,SetSplittingInstance.toCNFEquiv,SetSplittingInstance.modelCountOn_toDeclaredCNF,SetSplittingInstance.computableInPolyTime_toDeclaredCNF;n = |U|, width≤ k);LocalMap.toDeclaredCNFpaired withLocalMap.preimageDeclaredEquiv), plus general conditional monotone-exponent transfers (CountingTransfer.transfer_declaredCounter,CountingTransfer.declaredCounter_of_modelCounterviaCNF.padDeclaredVars) and all six parameter-preserving conditional transfers (CountingTransfer.exists_indepSetCounter_of_declaredCounter,CountingTransfer.exists_coloringCounter_of_declaredCounter,CountingTransfer.exists_perfectMatchingCounter_of_declaredCounter,CountingTransfer.exists_oneHotCSPCounter_of_declaredCounter,CountingTransfer.exists_setSplittingCounter_of_declaredCounter,CountingTransfer.exists_localMapPreimageCounter_of_declaredCounter).Cslib.Circuits.Boolean.mem_tseitinClauseinTseitin.lean,CSP.computableInPolyTime_mapFilterConstinPolyTime/CSP/ToCNF.lean,parsimoniousReducible_guardinSharpThreeSAT.lean), adds strict-modulekernel tests inCslibFrontierTests/CountingReductions.lean(nonative_decideorimport all), updatesCslibFrontierResults/Entries.lean,references.bib(Valiant 1979 enumeration entry),CslibFrontier.lean(mk_all),manual/machines-and-classes/reductions.md, andmanual/sources.md. Assessedmanual/AGENT_OPERATORS.mdandROADMAP.md: no edits needed (no CLI, build, validation gate, cache, or role workflow changes, and#3672remains open).Validation and review
./scripts/check.sh --base origin/main(19 / 19gatesok),parallel_defs.py --theorems(0duplicates),check_hygiene.py --check-simp,check_projection_chains.py,check_encoding_readability.py,check_pr_names.py --strict, and strict-module#print axioms.verifier-crypto(218cf06c; agent review only, not human or coordinator review). AI-assisted implementation by Jetski worker218c-ot-boundacting for Samuel Schlesinger.