{"id":"7388bd70-ab2c-4d91-a18d-e282220dedc1","arxiv_id":"2608.06820","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"For hypergraph Horn functions, enumerating all coatoms (equivalently minimal stopping sets) is not output-polynomial unless P=NP when hyperedge size and element frequency are both at least three, and becomes output-linear when either is at most two.","lead":"This paper studies when it is possible to efficiently list all the minimal stopping sets (equivalently all the antikeys or coatoms) of a hypergraph Horn function. It proves that complete enumeration is conditionally intractable as soon as hyperedges and element frequencies both reach size three, while rank-two or frequency-two cases can be listed in output-linear time.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the central representation theorem and hardness transfer are internally sound, and the one external cycle-listing dependency does not threaten the main results.","rationale":"The reader's ACCEPT verdict is justified. I checked the central representation theorem line by line: the local gadgets satisfy the stated feasibility characterizations; the disjunction tree has the claimed unique-extension property; the root construction correctly separates the represented branch from the empty stopping set; and the inclusion-order isomorphisms are established by monotonicity and uniqueness. The hardness transfer from maximal Horn models is sound because the KSS reduction is fully reproduced in Appendix A, including the no-instance characterization used in Lemma 4.6. The frequency-splitting and three-uniform replacements preserve the stopping-set poset exactly and have the stated linear size bounds. The frequency-two graphic-circuit correspondence is correct. The only genuinely external component is the cited output-linear cycle-listing algorithm of Birmelé et al.; however, this affects only the positive Delta(H)<=2 boundary, not the main hardness theorem or the rank-three representation. Moreover, even a conservative reading of that algorithm as O(m+c), where c is the number of cycles, is enough for the claimed output-linear bound because c is always at most the total output length sum |S|. Thus the most load-bearing assumptions of the paper are either proved internally or supported by standard, independently verifiable results. I found no internal inconsistency, no circular step, and no unsupported assumption that would change the verdict.","tokens_in":35412,"tokens_out":32966,"duration_ms":383022,"concrete_test":"Run a brute-force verifier on all normalized Horn CNFs with up to five variables: build C(Gamma) by Theorem 3.11, enumerate all nonempty stopping sets by brute force, and confirm the bijection with False(Gamma) together with inclusion-order preservation. Independently, inspect Birmelé et al. [4] to confirm the cycle-listing bound is at least O(m+c) for c the number of cycles, and check that c <= sum_{S in MinStop(H)} |S| so that the Corollary 5.7 output-linear claim follows.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I re-derived the main construction in detail. The equality, implication, and OR gadgets (Lemmas 3.1-3.4) realize the claimed Boolean relations with unique private extensions; the root construction forces r=1 in every nonempty stopping set and eliminates the all-zero branch; Lemmas 3.6-3.10 therefore establish the poset isomorphism of Theorem 3.11. The obstruction-free transfers in Section 4 use only the Kavvadias-Sideri-Stavropoulos reduction, which is reproduced and verified in Appendix A, plus standard NP-completeness of Positive 1-in-3 3SAT. The splitting and three-uniform replacements preserve the full stopping-set poset with linear size; the frequency-two graphic-circuit correspondence is correct. The only external tool is the Birmelé et al. output-linear cycle listing used for the Delta(H)<=2 positive boundary. Even if that bound is read as O(m+c) with c the number of cycles rather than total cycle length, the inequality c <= sum |S| makes the stated O(L+sum|S|) bound follow after explicit expansion of each listed cycle. This dependency is isolated to the frequency-two boundary; Theorem 4.9 and the rank-three representation stand independently.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the closure systems defined by hypergraph Horn CNFs and the enumeration of their coatoms, equivalently the minimal nonempty stopping sets of the underlying hypergraph. Its central structural result (Theorem 3.11) is a linear-time, linear-size construction C(Γ) of rank at most three from any normalized Horn CNF Γ, such that nonempty stopping sets of C(Γ) are in inclusion-order bijection with the false-variable sets of models of Γ, with all auxiliary coordinates uniquely determined. This is used to transfer the Kavvadias–Sideri–Stavropoulos lower bounds for maximal Horn model enumeration: HH-Coatom-Enum is not in OutputP unless P=NP, even when every hyperedge has size two or three, and the incremental and extension problems are NP-complete under the same restrictions. Incidence splitting and a local three-uniform replacement extend the hardness to maximum element frequency three, while rank-two and frequency-two classes are shown to admit output-linear total-time enumeration (and polynomial delay with polynomial space in the frequency-two case). Constrained extension is NP-complete even for three-uniform hypergraphs of exact frequency two. The paper also contains a linear-size output-bijective reduction from explicit minimal-transversal enumeration as a separate appendix.","tokens_in":35609,"tokens_out":16571,"duration_ms":177326,"significance":"If correct, the main theorem is a genuine structural representation result: it embeds an arbitrary Horn model poset into the proper-model poset of a rank-three hypergraph Horn function with unique extensions, and it turns maximal-model hardness into coatom hardness without changing the output family. The proof is unusually complete: the gadget lemmas are explicit, the uniqueness and inclusion preservation are checked, the incidence counts are given, and the external KSS reduction is reproduced and verified in Appendix A. The positive algorithms are also concrete, with Appendix C giving a self-contained polynomial-delay, polynomial-space implementation for the frequency-two case. The complexity thresholds are sharp and the classification is falsifiable. The only external algorithmic dependency is the output-linear cycle-listing algorithm of Birmelé et al. used in Corollary 5.7; even if that theorem is read as O(m+c) rather than O(m+total cycle length), the stated O(L+Σ|S|) bound follows by expanding each listed cycle, and the DelayP claim is independent of that dependency. I therefore do not regard the stress-test concern as a threat to the central claims.","major_comments":[],"minor_comments":[{"comment":"Several mathematical symbols appear as corrupted characters in the typeset text, notably the isomorphism symbol in Corollary 3.13 and the disjoint-union symbol in Eq. (4); these should be cleaned up in the final version.","section":"§3.3, Corollary 3.13 and §5.4, Theorem 5.11"},{"comment":"The paper should state explicitly whether the linear-time guarantee imported from [4] is in terms of number of cycles or total cycle length, and, if the former, add one sentence showing that O(m+c) implies the displayed O(L(H)+Σ(|S|+1)) bound after expanding each cycle.","section":"§5.3, Corollary 5.7"},{"comment":"In Eq. (4), the notation MinStop(H) ¤∪ D(H) would be clearer as a disjoint union with an explicit note that members of MinStop(H) are viewed as subsets of the enlarged ground set; the current symbol is ambiguous.","section":"§5.4, Theorem 5.11"},{"comment":"The edge labels EEq, EImp, and EOR use an unexplained prefix; if these denote the hyperedge families, they should be defined in the caption or in the surrounding text.","section":"Figure 1"}],"recommendation":"accept","confidential_remarks":"The manuscript is carefully written and the main proofs are checkable in detail. The single-author paper has no self-citations, and the external algorithmic dependencies are isolated and, where load-bearing for the hardness results, reproduced and verified in the appendices. The remaining concerns are typographical and notational and can be handled at the proof stage; I see no substantive obstacle to publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Good paper, worth a serious referee. The headline result is the rank-three representation: any Horn CNF can be converted in linear time to a hypergraph of rank at most three whose proper-model poset is order-isomorphic to the original model poset, with each source model having a unique extension. The local equality/implication/OR gadgets are simple, but their composition into a linear-size encoding is genuinely new, and the corollary that every finite lattice embeds as a proper-model poset of a rank-three hypergraph Horn function is a nice structural payoff. The transfer of the Kavvadias–Sideri–Stavropoulos maximal-model lower bound to coatom enumeration is clean, and the threshold classification (rank/frequency at most two tractable, at least three conditionally hard) is coherent.\n\nThe proofs are detailed and, as far as I checked, internally consistent. The gadget lemmas, representation theorem, incidence splitting, and three-uniform replacement all hold up. The hardness results are conditional on P≠NP and inherit from the reproduced KSS reduction in Appendix A, which is standard practice. Appendix D, the output-bijective embedding of minimal-transversal enumeration, is a nice extra even though it is not used for the main lower bounds.\n\nSoft spots: the only external dependency that deserves a flag is the output-linear cycle-listing algorithm of Birmelé et al. used for the frequency-two positive case. The paper cites it without reproducing the output-linear bound, but Appendix C gives a direct polynomial-delay, polynomial-space implementation, so the DelayP part is self-contained. If the Birmelé bound were wrong, the frequency-two boundary would weaken to polynomial total time, leaving the rank-two result and all lower bounds intact. That is a minor concern, not a load-bearing flaw. Also minor: the exact-frequency-two extension hardness uses Hamiltonian cycle in planar cubic 3-connected graphs, a standard hard problem.\n\nThe paper is for researchers in closure systems, Horn functions, and output-sensitive enumeration. It answers a natural question and gives a representation tool that will likely be reused. I would send it to peer review; a serious referee will find the construction worth engaging with.","headline":"A solid, genuinely new representation theorem for Horn model posets that transfers known hardness to coatom enumeration, with a clean threshold classification; worth a serious referee.","tokens_in":36120,"tokens_out":1414,"would_cite":true,"duration_ms":15139,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A new construction converts any Horn CNF into a rank-three hypergraph whose coatoms are exactly the maximal models, yielding sharp complexity thresholds for coatom enumeration.","keywords":["Horn CNF","hypergraph Horn function","coatom","stopping set","antikey","output-sensitive enumeration","closure system","minimal stopping set"],"falsifier":"Take a small Horn CNF such as $\\Gamma=(\\{a,b\\}\\to c)\\land(\\{d\\}\\to\\bot)$, construct $C(\\Gamma)$ by the rules of Theorem 3.11, and list all nonempty stopping sets; if any set fails to be a false-variable set of a model of $\\Gamma$, or any model's false-variable set fails to extend to a stopping set, the central representation claim is false.","tokens_in":35194,"feed_emoji":"🧮","tokens_out":9536,"duration_ms":78801,"temperature":0.7,"pith_summary":"The paper proves that every Horn formula can be re-encoded as a rank-at-most-three hypergraph Horn function with only linear blow-up, in such a way that the inclusion order of the models is preserved and every model gets a unique extension to a target model. This makes the maximal models of the original formula correspond one-to-one to the coatoms of the hypergraph closure system, which are the complements of the minimal nonempty stopping sets. The encoding is a bridge that transfers known hardness of maximal Horn model enumeration: unless P=NP, listing all coatoms from the hypergraph incidence representation is not output-polynomial, even when every hyperedge has size two or three and every element occurs at most three times. On the positive side, the paper shows that rank at most two and maximum element frequency at most two both admit output-linear total-time enumeration, so these thresholds are conditionally sharp. The same representation also implies that every finite lattice is isomorphic to the proper-model poset of a rank-three hypergraph Horn function.","feed_headline":"Rank-3 hypergraphs encode every Horn model poset","feed_subtitle":"Coatom enumeration is then hard unless rank or frequency drops to two.","key_machinery":"The machinery is a library of hyperedge gadgets that realize Boolean relations through the stopping-set condition $|A\\cap S|\\neq 1$. A single edge $\\{p,q\\}$ enforces equality; the implication gadget $\\mathrm{Imp}(x,y;q)=\\{\\{y,q\\},\\{x,y,q\\}\\}$ enforces $x\\to y$ with $q=y$; and the OR gadget $\\mathrm{OR}(a,b;c,q)=\\{\\{c,q\\},\\{a,b,c\\},\\{a,c,q\\}\\}$ enforces $c=a\\lor b$ with $q=c$, each with a unique extension of the private elements. These gadgets are chained into OR-trees for clause premises, capped by a root construction that separates the all-zero assignment, and assembled into $C(\\Gamma)$ so that nonempty stopping sets are exactly the false-variable sets of models. The companion reductions use incidence splitting to cap element frequency at three, the apex multigraph whose graphic circuits are the minimal stopping sets when $\\Delta(H)\\le 2$, and a local four-triple replacement that turns two-element hyperedges into three-element ones.","core_discovery":"The central claim is Theorem 3.11: for every normalized Horn CNF $\\Gamma$ on variables $X$, one can construct in $O(\\|\\Gamma\\|_{\\mathrm{inc}})$ time a normalized hypergraph $C(\\Gamma)$ of rank at most three, with $L(C(\\Gamma))=O(\\|\\Gamma\\|_{\\mathrm{inc}})$, such that every false-variable set of a model of $\\Gamma$ extends uniquely to a nonempty stopping set of $C(\\Gamma)$, and this correspondence is an inclusion-order isomorphism. Equivalently, the model poset of $\\Gamma$ is isomorphic to the proper-model poset of the hypergraph Horn function $\\Phi_{C(\\Gamma)}$, so maximal models map bijectively to coatoms. The representation transfers the maximal-Horn-model lower bound of Kavvadias, Sideri, and Stavropoulos: enumerating coatoms from a hypergraph incidence list is not in OutputP unless P=NP, even when every hyperedge has size two or three; after incidence splitting, the same lower bound holds with maximum element frequency at most three, and a local replacement makes the hard hypergraphs three-uniform. The paper also proves the matching positive endpoints: rank at most two and maximum element frequency at most two admit output-linear total-time enumeration, with a polynomial-delay, polynomial-space algorithm in the frequency-two case, while coatom extension is NP-complete already for three-uniform hypergraphs in which every element has frequency exactly two.","pith_inferences":["If the representation theorem is applied to any tractable subclass of Horn formulas, it yields a general reduction template: output-polynomial coatom enumeration for the corresponding rank-three hypergraphs would give output-polynomial maximal-model enumeration for that subclass.","Because the paper embeds minimal-transversal enumeration into coatom enumeration by a linear, output-bijective reduction, any future output-polynomial algorithm for HH-Coatom-Enum would also settle the long-open question of output-polynomial minimal-transversal enumeration; the converse does not follow.","The paper leaves linear three-uniform hypergraphs (Tanner graphs of girth at least six) and (3,3)-regular inputs open, and a plausible next step is to test whether the lower-bound construction can be made girth-preserving, which the current triangle-replacement method cannot do.","From the coding-theory side, the frequency-two positive result suggests that variable-node degree exactly two makes stopping-set enumeration structurally graphic; extending to variable-node degree three may require a different combinatorial characterization than graphic circuits."],"forward_implications":["Any Horn CNF can be compiled in linear time into a rank-three hypergraph Horn function whose incidence length is linear in the input, so Horn model posets are represented inside hypergraph Horn posets with no output-size blow-up.","Listing all coatoms, equivalently all minimal nonempty stopping sets, from the incidence representation is not in OutputP unless P=NP, even for hypergraphs whose edges have size two or three and whose elements have frequency at most three.","For rank at most two, coatoms can be listed in output-linear total time after normalization, because the closure system decomposes into equality components.","For maximum element frequency at most two, coatoms correspond to graphic circuits of an apex multigraph, giving output-linear total-time enumeration and a polynomial-delay, polynomial-space algorithm.","Coatom extension is NP-complete already on three-uniform, exact-frequency-two hypergraphs, while enumerating all coatoms on that same class is output-linear; the same representation also shows every finite lattice is isomorphic to the proper-model poset of a rank-three hypergraph Horn function."],"supporting_citations":[{"why":"Defines hypergraph Horn functions and the all-but-one implication representation that is the paper's target class.","marker":"[2]"},{"why":"Supplies the maximal Horn model lower bound that the representation transfers to coatom enumeration hardness.","marker":"[15]"},{"why":"Provides the optimal cycle-listing algorithm that yields output-linear total time in the frequency-two case.","marker":"[4]"},{"why":"Establishes NP-completeness of bounded-size stopping set existence, used for the minimum-complement coatom problem.","marker":"[17]"},{"why":"Identifies Positive One-in-Three 3SAT as the NP-complete source problem inside the KSS reduction.","marker":"[23]"},{"why":"Gives NP-completeness of Hamiltonian cycle in planar cubic 3-connected graphs, the base of the exact-frequency-two extension lower bound.","marker":"[13]"}],"fun_headline_variants":["All Horn posets are rank-3 hypergraph models","Coatom enumeration hard unless rank or frequency ≤2","Every Horn model poset from a rank-3 hypergraph","Rank-3 hypergraph encoding makes coatom enumeration hard"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The sharp frequency-two positive result assumes that the cycle-listing algorithm of Birmelé et al. runs in time linear in the input plus the total length of all listed cycles; if that external fact fails, the frequency-two boundary degrades from output-linear to merely polynomial total time, while the paper's self-contained polynomial-delay bound remains.","fun_headline_variants_meta":{"raw":{"variants":["All Horn posets are rank-3 hypergraph models","Coatom enumeration hard unless rank or frequency ≤2","Every Horn model poset from a rank-3 hypergraph","Rank-3 hypergraph encoding makes coatom enumeration hard"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001475,"raw_usage":{"total_tokens":6023,"prompt_tokens":1134,"completion_tokens":4889,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":750,"completion_tokens_details":{"reasoning_tokens":4821}},"tokens_in":750,"tokens_out":4889,"duration_ms":31902,"temperature":1.0,"reasoning_tokens":4821,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T20:13:25.926703+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a small Horn CNF such as $\\Gamma=(\\{a,b\\}\\to c)\\land(\\{d\\}\\to\\bot)$, construct $C(\\Gamma)$ by the rules of Theorem 3.11, and list all nonempty stopping sets; if any set fails to be a false-variable set of a model of $\\Gamma$, or any model's false-variable set fails to extend to a stopping set, the central representation claim is false.","supporting_citations":[{"cited_title":"Kavvadias, Martha Sideri, and Elias C","cited_arxiv_id":null,"evidence_quote":"Supplies the maximal Horn model lower bound that the representation transfers to coatom enumeration hardness."},{"cited_title":"Ferreira, Roberto Grossi, Andrea Marino, Nadia Pisanti, Romeo Rizzi, andGustavoSacomoto","cited_arxiv_id":null,"evidence_quote":"Provides the optimal cycle-listing algorithm that yields output-linear total time in the frequency-two case."},{"cited_title":"Garey, David S","cited_arxiv_id":null,"evidence_quote":"Gives NP-completeness of Hamiltonian cycle in planar cubic 3-connected graphs, the base of the exact-frequency-two extension lower bound."}],"review_version":1}