{"id":"acd71a30-f7d4-4c0a-8145-56d90119c1b0","arxiv_id":"2504.15417","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A transfer of Boolean network results to Datalog^neg yields structural conditions for existence, uniqueness, and counting bounds of stable, stable partial, and regular models, plus a characterization of regular models as minimal stable trap spaces.","lead":"This paper builds a formal bridge between Datalog^neg logic programs and Boolean network theory, then uses graph conditions on cycles to control the number and nature of stable and regular models. It proves that cycle parity in the dependency graph determines when regular models collapse to stable models and when models are unique, and it gives model-count upper bounds based on feedback vertex sets.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central regular/stable and trap-space results depend on unproved same-group lemmas; the false Theorem 4.8 shows the transferred graph argument is not universally safe, so independent verification is needed.","rationale":"I read the paper as establishing a formal bridge between Datalog^neg and Boolean networks, then using that bridge to transfer results on cycles, feedback vertex sets, and trap spaces. The central claims are coherent and largely plausible, and the reader's conditional verdict is appropriate. The most load-bearing risk is not a single internal step in the proof of a headline theorem but the chain of dependencies on unproved results from the same group, especially Lemma 3.1 and Proposition 5.8 of Trinh et al. 2025a. These lemmas are used in multiple places, including the proof that regular models correspond to minimal trap spaces and the proof that all regular models are two-valued in the absence of odd cycles. The paper does not prove these lemmas, and no formal verification is provided. The false Theorem 4.8 is a concrete, localized error; its proof transfers the minimum in-degree property from the atom dependency graph to the influence graph, which fails for constant update functions. This does not directly break the central odd/even-cycle theorems, but it shows that the graphics-transfer methodology is not fail-safe, so external dependence becomes more concerning. Because the central results appear to hold and the paper already flags the problematic theorem, I would not change the reader's 'conditional' verdict: the paper should be accepted only after the false theorem is corrected or removed and the cited same-group lemmas are either independently proved or replaced by self-contained proofs.","tokens_in":602,"tokens_out":12430,"duration_ms":457514,"concrete_test":"Independently verify Lemma 3.1 and Proposition 5.8. One concrete computational check: for all Boolean networks up to n=5 variables (or a random sample of 10^5 DNF-defined networks), enumerate all subspaces m, test (i) whether every trap space has a complete trap space m̂ ≤s m, and (ii) whether m is a trap space iff m(f_v) ≤s m(v) for all v. If any counterexample appears, Theorem 3.2, Corollary 3.1, Corollary 5.5, and Theorem 5.4 fail. Additionally, re-derive both lemmas from first principles without citing Trinh et al. 2025a.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's headline results, especially Lemma 4.2 (regular models of P coincide with ≤s-minimal trap spaces of the encoded BN of lfp(P)) and Theorem 5.4 (regular models are exactly the ≤s-minimal stable trap spaces), both rely on Lemma 3.1 from Trinh et al. 2025a and, for Theorem 5.4, also on Proposition 5.8 from the same paper. These two lemmas are cited without proof and are not independently verified or machine-checked. In particular, Theorem 3.2 and Corollary 3.1 depend directly on Lemma 3.1, and Corollary 5.8 depends on Proposition 5.8. If either lemma is false, the bridge between Datalog^neg semantics and Boolean-network trap spaces collapses, taking with it part of the odd-cycle existence result and the main trap-space characterization. The paper's own Theorem 4.8 is false as stated, and its proof assumes that minimum in-degree transfers from adg(P) to G(f); this is invalid when an update function is constant. That mistake does not by itself refute the central theorems, but it demonstrates that the paper's transfer of graph properties from adg(P) to G(f) is not always sound, which raises the stakes for the unproved same-group results.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper establishes a formal correspondence between Datalog programs and Boolean networks: each program is encoded as a BN via its Clark completion, and the atom dependency graph is related to the BN's influence and syntactic influence graphs. Using this bridge, the authors transfer Boolean-network theorems to derive structural conditions on Datalog model theory. The main claims are: (i) if adg(P) has no odd cycle then all regular models are two-valued, hence, with existence of regular models, they coincide with stable models; (ii) if adg(P) has no even cycle then there is a unique stable partial model and a unique regular model; (iii) new upper bounds on the number of stable, stable partial, and regular models in terms of feedback vertex sets of adg(P); (iv) stronger results for uni-rule programs using delocalizing triples; and (v) a trap-space semantics for Datalog in which the subset-minimal stable trap spaces coincide with regular models. The paper also revisits and partially corrects earlier claims of You and Yuan (1994) on well-founded stratification.","tokens_in":39505,"tokens_out":15613,"duration_ms":132746,"significance":"If the results hold, the paper provides a valuable and novel conceptual transfer that yields new graph-based sufficient conditions for existence and uniqueness of canonical models, new counting bounds using feedback vertex sets, and a trap-space characterization linking regular models to program dynamics. The main derivations are coherent and transparent given the cited Boolean-network theorems, and the paper is explicit about the scope of its claims for general versus uni-rule programs. However, the manuscript contains a false stated theorem and several central results rely on unproved lemmas from the authors' own recent preprints, so the correctness risk is material. No software or machine-checked proofs accompany the paper; the main strength is the conceptual unification and the new FVS bounds.","major_comments":[{"comment":"Theorem 4.8 is false as stated. Consider the Datalog program P = {a; b←a; c←not b; a←not c}. Its atom dependency graph has arcs a⊕→b, b⊖→c, and c⊖→a, so it is strongly connected, contains no odd cycle, and has at least one arc; P is tight because there is no positive cycle. Yet the unique stable model of P is {a,b}, so there is no pair of complementary stable models A,B with A∪B = HB_P. The proof's step \"The graph adg(P) has the minimum in-degree of at least one ... Hence, fj cannot be constant for every variable j\" is invalid: the minimum in-degree of adg(P) does not transfer to G(f). In this example fa = 1∨¬c = 1 is a constant function, so G(f) has a vertex of in-degree zero. The theorem should be corrected, e.g., by adding an explicit assumption that no update function of the encoded BN is constant, or it should be removed as a stated result.","section":"Section 4.3, Theorem 4.8"},{"comment":"The central bridge between Datalog trap spaces and regular models relies on unproved external results from the same group: Lemma 3.1 (Proposition 3 of Trinh et al. 2025a) is used in Theorems 3.2, Corollary 3.1, Lemma 4.1, Lemma 4.2, Corollary 5.7, Corollary 5.8, and Theorem 5.4; Proposition 5.8 (Proposition 2 of Trinh et al. 2025a) is used in Corollaries 5.5 and 5.6; and Theorems 4.15 and 4.25 of the arXiv preprint Trinh et al. 2025b are used in Theorems 4.16 and 4.26. The manuscript provides no proofs of these statements. Because they are load-bearing for the main trap-space characterization and for the odd/even-cycle results, the paper should either include complete proofs (an appendix would suffice), state them explicitly as assumptions with precise hypotheses and verifiable public references, or otherwise make the dependency transparent; as written, a false statement in any of them would invalidate several headline claims.","section":"Sections 3 and 5, Lemmas 3.1 and 5.8"}],"minor_comments":[{"comment":"The abstract claims that in the absence of odd cycles the regular models coincide with the stable models, but Theorem 4.7 only proves that all regular models are two-valued. Please add the explicit corollary that a two-valued stable partial model is a stable model (and that every stable model is a regular model), so the coincidence is stated and proved in the body.","section":"Abstract and Section 4.3"},{"comment":"The proofs of Theorems 4.1 and 4.2 are omitted with only \"By mimicking the proof ... we can prove\". In a formal journal these claims should be proved or cited to a precise published source.","section":"Section 4.1, Theorems 4.1 and 4.2"},{"comment":"Typo: \"If adg(P) is has no odd cycle\" should read \"If adg(P) has no odd cycle\".","section":"Section 4.3, Lemma 4.3"},{"comment":"The word \"interpreration\" appears twice; please correct to \"interpretation\".","section":"Section 4.2, Lemmas 4.1 and 4.2"},{"comment":"The statement \"we always find an even feedback vertex set U such that |U| ≤ k\" where k is the number of even cycles deserves a one-sentence justification: choose one vertex from each even cycle to form U.","section":"Section 4.5, Remark 4.6"},{"comment":"The phrase \"two distinct regular models are separated\" is informal; please state precisely that they are not consistent, i.e., S(I1) ∩ S(I2) = ∅.","section":"Section 5.3.3, after Theorem 5.4"},{"comment":"The entry \"You, J. 2025. personal communication\" is not a citable public source; the claims supported by this reference should be verified against a published work or removed.","section":"References"},{"comment":"The term \"syntatic\" is a typo for \"syntactic\" throughout this subsection (also in Proposition 4.4 and Theorem 4.11).","section":"Section 4.2, Definitions 4.7-4.8"},{"comment":"Minor wording: \"It is to see that\" should be \"It is easy to see that\".","section":"Example 4.2"},{"comment":"There is a stray closing parenthesis in the last line \"adg(P ))\"; should be \"adg(P)\".","section":"Proposition 3.1 proof"}],"recommendation":"major_revision","confidential_remarks":"The manuscript's heavy reliance on the authors' own recent preprints and unpublished statements (Trinh et al. 2025a, 2025b; You 2025, personal communication) is a concern, especially because one of the paper's own transfer arguments (Theorem 4.8) is demonstrably false. The editor may wish to request that the external lemmas be proved in an appendix or replaced by fully verified public results before acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear X,\n\nHere is my read. The paper is worth taking seriously. It builds on Inoue's earlier Boolean-network encoding and pushes much further: regular models are characterized as ≤s-minimal stable trap spaces (Thm 5.4), odd-cycle-free programs have two-valued regular models and hence stable models (Thm 4.7), even-cycle-free programs have unique stable partial and regular models (Cor 4.5/4.6), and there are feedback-vertex-set upper bounds for model counts. Those are real results if the proofs hold, and the trap-space connection is the most interesting conceptual contribution.\n\nWhere I part ways with the authors: Theorem 4.8 is false as stated. The program {a; b←a; c←not b; a←not c} has a strongly connected, tight atom dependency graph with no odd cycle, but its only stable model is {a,b}; there is no complementary pair. The proof assumes minimum in-degree transfers from adg(P) to the influence graph, which fails when update functions are constant. This is a local flaw — the theorem should be dropped or its hypotheses strengthened — but it matters because it shows the adg-to-G(f) transfer is not generally sound.\n\nThe bigger concern is the dependency chain. Lemma 4.2 and Theorem 5.4 both lean on Lemma 3.1 and Proposition 5.8 from Trinh et al. 2025a, and on Theorems 4.15 and 4.25 from 2025b, all same-group preprints whose proofs are not included or machine-checked here. If any of those is wrong, several central statements collapse with it. That does not make the paper circular — the main theorems are genuinely derived from stated definitions and classical BN results — but it does make the foundation a house of cards until those external lemmas are independently checked.\n\nThe rest of the proof I sampled is coherent, and the citation pattern is not abusive: heavy self-citation, but to results that are actually load-bearing. The paper is honest about You and Yuan's issues and states its conjectures cleanly.\n\nVerdict: send it to referees, but demand that Theorem 4.8 be fixed or removed and that the imported lemmas be either proved in an appendix or replaced by statements with available proofs. If the authors do that, this becomes a solid contribution to the logic programming and non-monotonic reasoning literature.","headline":"A genuinely useful bridge between Datalog^neg and Boolean networks, with one false theorem and an unproved same-group dependency chain that need fixing before the central claims are fully reliable.","tokens_in":40079,"tokens_out":3592,"would_cite":false,"duration_ms":33210,"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":"Cycle parity in a Datalog¬ program's dependency graph decides whether stable models exist or are unique.","keywords":["Datalog negation","Boolean network","trap space","stable model","regular model","atom dependency graph","feedback vertex set","model counting"],"falsifier":"Find a Datalog$\\neg$ program whose atom dependency graph has no odd cycle but whose unique regular model is three-valued, which would refute Theorem 4.7. Alternatively, search for a program with no even cycle that has two distinct stable partial models, which would contradict Corollary 4.5. Both are finite syntactic searches checkable with any Datalog$\\neg$ solver.","tokens_in":39029,"feed_emoji":"🌀","tokens_out":10057,"duration_ms":75735,"temperature":0.7,"pith_summary":"This paper establishes a formal bridge between Datalog$\\neg$ programs and Boolean network theory, the framework originally introduced for gene regulatory networks. Encoding each ground atom as a Boolean variable whose update function is the disjunction of the rule bodies that derive it lets the authors transfer structural results from Boolean networks to logic-programming semantics. The central findings are parity laws: if the atom dependency graph has no odd cycle, every regular model is two-valued and stable models are guaranteed to exist; if it has no even cycle, the stable partial model and the regular model are unique. The bridge also yields counting bounds in terms of feedback vertex sets, and a new characterization: the regular models of a Datalog$\\neg$ program are exactly its subset-minimal stable trap spaces. A sympathetic reader should care because these results give graph-theoretic answers to long-standing questions about model existence, uniqueness, and enumeration in non-monotonic logic programming.","feed_headline":"Datalog¬: odd cycles force stable models, even cycles force uniqueness","feed_subtitle":"A translation to Boolean networks shows regular models are minimal trap spaces and yields counting bounds.","key_machinery":"The load-bearing construction is the encoded Boolean network: for each ground atom $v$ of a Datalog$\\neg$ program $P$, define a Boolean variable $v$ with update function $f_v$ equal to the disjunction, over all rules with head $v$, of the conjunction of their body literals, and $f_v = 0$ if no rule derives $v$. The encoded network's influence graph is a subgraph of the atom dependency graph (equal for uni-rule programs), its fixed points are exactly the supported models, and its complete trap spaces are exactly the supported partial models. The second key object is the trap space, a set of states closed under the network's dynamics; the paper shows that subset-minimal stable trap spaces coincide with regular models. These identifications let the authors import Boolean-network theorems about attractors, fixed points, and feedback vertex sets directly into Datalog$\\neg$.","core_discovery":"The paper's central claim is that the model theory of Datalog$\\neg$ programs is governed by the parity of cycles in the atom dependency graph, through an exact correspondence with Boolean networks. Theorem 4.7 proves that if the atom dependency graph has no odd cycle, then every regular model of the program is two-valued, which immediately yields the existence of at least one stable model. Conversely, Theorem 4.12 and Corollary 4.6 prove that if the atom dependency graph has no even cycle, then the program has a unique supported partial model, a unique stable partial model, and therefore a unique regular model. Finally, Theorem 5.4 proves that a three-valued interpretation is a regular model if and only if it is a subset-minimal stable trap space of the program, tying the regular-model semantics to the dynamics of the stable transition graph.","pith_inferences":["This suggests a practical pre-processing step: checking cycle parity in the atom dependency graph can tell a solver whether model enumeration is trivial (zero or one) or potentially exponential before invoking general answer-set machinery.","The trap-space characterization may let existing Boolean-network algorithms for minimal trap spaces be reused to enumerate regular models of Datalog$\\neg$ programs, a task that currently lacks dedicated algorithms.","The paper leaves open whether the odd/even-cycle results extend to general normal logic programs with function symbols; the correction of You and Yuan (1994) suggests the infinite-Herbrand-base setting needs genuinely new arguments.","One could test the tightness of the $3^{|U|}$ and $2^{|U|}$ bounds by generating random Datalog$\\neg$ programs with prescribed even feedback vertex sets and comparing actual model counts to the bounds."],"forward_implications":["If a Datalog$\\neg$ program's atom dependency graph has no odd cycle, all its regular models are two-valued and at least one stable model exists.","If the atom dependency graph has no even cycle, the program has exactly one stable partial model and exactly one regular model, and at most one stable model.","With $U$ an even feedback vertex set of the atom dependency graph, the program has at most $3^{|U|}$ supported and stable partial models and at most $2^{|U|}$ stable models; for tight programs the same $2^{|U|}$ bound applies to regular models.","Regular models of any Datalog$\\neg$ program are exactly its subset-minimal stable trap spaces, so every regular model contains a strict stable class and the number of regular models bounds the number of strict stable classes from below.","For uni-rule Datalog$\\neg$ programs the atom dependency graph and the influence graph coincide, so stronger results based on delocalizing triples apply to stable-model existence and uniqueness."],"supporting_citations":[{"why":"Supplies the tight-program equivalence between stable and supported models and the lemma that least fixed points preserve absence of odd cycles.","marker":"Fages (1994)"},{"why":"Gives the Boolean-network theorem that an influence graph without odd cycles has no cyclic asynchronous attractor, used to prove Theorem 4.7.","marker":"Richard (2010)"},{"why":"Defines trap spaces and the result that every minimal trap space contains an attractor, used throughout Sections 4 and 5.","marker":"Klarner et al. (2015)"},{"why":"Provides Lemma 3.1 and Proposition 5.8, which the paper imports to relate trap spaces to complete trap spaces and to characterize trap spaces equationally.","marker":"Trinh et al. (2025a)"},{"why":"Supplies Theorems 4.15 and 4.25 on asynchronous attractors and counting in AND-NOT Boolean networks, underpinning the uni-rule results.","marker":"Trinh et al. (2025b)"},{"why":"Establishes that the least fixed point transformation preserves stable partial, regular, and stable models, a key step in several proofs.","marker":"Aravindan and Dung (1995)"},{"why":"Provides the stable and supported transition graph and class semantics used to define and analyse trap spaces for Datalog$\\neg$.","marker":"Inoue and Sakama (2012)"},{"why":"Introduces delocalizing triples and fixed-point existence and uniqueness theorems for AND-NOT Boolean networks used for uni-rule programs.","marker":"Richard and Ruet (2013)"},{"why":"Defines well-founded stratification and the original claims about odd and even cycles that the paper corrects and refines.","marker":"You and Yuan (1994)"},{"why":"Provides the $2^{|U|}$ bound on fixed points of a Boolean network used to bound stable models.","marker":"Aracena (2008)"}],"fun_headline_variants":["Cycle parity decides Datalog¬ model existence and uniqueness","Datalog¬ regular models are minimal stable trap spaces","Datalog¬: odd-cycle-free ensures stable models; even-cycle-free ensures uniqueness","Datalog¬: cycle parity dictates stable-model existence and uniqueness","Datalog¬: cycle parity and trap spaces govern model theory"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the recent Boolean-network theorems imported from Trinh et al. (2025a) and Trinh et al. (2025b) are correct, since the paper gives no proof of them; if any fails, the Datalog$\\neg$ theorems that call on them fail too. A second fragile step is the proof of Theorem 4.8, which assumes that a strongly connected atom dependency graph forces every variable of the encoded network to be non-constant, whereas constant update functions can break that transfer.","fun_headline_variants_meta":{"raw":{"variants":["Cycle parity decides Datalog¬ model existence and uniqueness","Datalog¬ regular models are minimal stable trap spaces","Datalog¬: odd-cycle-free ensures stable models; even-cycle-free ensures uniqueness","Datalog¬: cycle parity dictates stable-model existence and uniqueness","Datalog¬: cycle parity and trap spaces govern model theory"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001189,"raw_usage":{"total_tokens":4893,"prompt_tokens":917,"completion_tokens":3976,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":533,"completion_tokens_details":{"reasoning_tokens":3890}},"tokens_in":533,"tokens_out":3976,"duration_ms":28407,"temperature":1.0,"reasoning_tokens":3890,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T11:28:48.252071+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a Datalog$\\neg$ program whose atom dependency graph has no odd cycle but whose unique regular model is three-valued, which would refute Theorem 4.7. Alternatively, search for a program with no even cycle that has two distinct stable partial models, which would contradict Corollary 4.5. Both are finite syntactic searches checkable with any Datalog$\\neg$ solver.","supporting_citations":[],"review_version":1}