Pith. sign in

REVIEW 2 major objections 10 minor 15 references

On the Boolean Network Theory of Datalog$^\neg$

T0 review · 2 major / 10 minor · reviewed 2026-08-16 · deepseek-v4-flash

Pith's one-line read Cycle parity in a Datalog¬ program's dependency graph decides whether stable models exist or are unique.

desk verdict 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. read the letter →

arxiv 2504.15417 v2 pith:PNYBR4WR submitted 2025-04-21 cs.LO cs.AI

classification cs.LOcs.AI
keywords DatalognegationBooleannetworktrapspacestablemodelregularatomdependencygraphfeedbackvertexsetcounting
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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$.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 10 minor

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.

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 (2)
  1. [Section 4.3, Theorem 4.8] 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.
  2. [Sections 3 and 5, Lemmas 3.1 and 5.8] 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.
minor comments (10)
  1. [Abstract and Section 4.3] 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.
  2. [Section 4.1, Theorems 4.1 and 4.2] 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.
  3. [Section 4.3, Lemma 4.3] Typo: "If adg(P) is has no odd cycle" should read "If adg(P) has no odd cycle".
  4. [Section 4.2, Lemmas 4.1 and 4.2] The word "interpreration" appears twice; please correct to "interpretation".
  5. [Section 4.5, Remark 4.6] 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.
  6. [Section 5.3.3, after Theorem 5.4] The phrase "two distinct regular models are separated" is informal; please state precisely that they are not consistent, i.e., S(I1) ∩ S(I2) = ∅.
  7. [References] 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.
  8. [Section 4.2, Definitions 4.7-4.8] The term "syntatic" is a typo for "syntactic" throughout this subsection (also in Proposition 4.4 and Theorem 4.11).
  9. [Example 4.2] Minor wording: "It is to see that" should be "It is easy to see that".
  10. [Proposition 3.1 proof] There is a stray closing parenthesis in the last line "adg(P ))"; should be "adg(P)".

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main theorems are derived from definitions and general Boolean-network lemmas; same-group citations are load-bearing but independent support.

full rationale

The paper's derivation chain does not assume its own conclusions. Theorem 3.1 is a direct equivalence by construction: a supported partial model is a three-valued model of comp(P), which is literally the complete-trap-space condition m(v)=m(fv). The later correspondences (Corollary 3.1, Lemma 4.2, Theorem 5.4) do import Lemma 3.1 and Proposition 5.8 from the authors' own Trinh et al. (2025a), and Theorems 4.15 and 4.25 from Trinh et al. (2025b), but those cited statements are parameter-free Boolean-network theorems whose assumptions concern arbitrary or AND-NOT Boolean networks and do not contain the Datalog^neg results being proved; they are therefore independent evidence under the hard rules rather than a circular dependence. Likewise, the odd-cycle and even-cycle results (Theorems 4.7 and 4.12, Corollaries 4.2, 4.5, and 4.6) are proved by transferring graph properties through Proposition 3.1 and applying external attractor theorems; no fitted parameter is renamed as a prediction and no definitional identity is disguised as a theorem. The known flaw in Theorem 4.8 (the transfer of minimum in-degree from adg(P) to G(f) is invalid when an update function is constant) is a correctness defect in one result, not a circularity in the derivation chain.

Assumptions & free parameters 0 free parameters · 8 assumptions · 2 invented entities

The paper is a pure mathematical theory paper with no fitted parameters or empirical data. Its central claims rest on standard logic programming semantics and on a set of external theorems from Boolean network theory, several of which come from the authors' own recent preprints. The newly introduced trap space notions are definitions with internal proofs, not entities with independent empirical handles.

assumptions (8)
  • domain assumption Standard Datalog^neg and normal logic program semantics: Clark's completion, supported, stable, stable partial, regular, and well-founded models, and standard properties such as every program having at least one stable class.
    Foundational definitions in Section 2.1, used throughout the paper.
  • domain assumption Fages' theorem (Theorem 4.3, Fages 1994) and Dietz et al.'s lemma (Theorem 4.4, Dietz et al. 2014): for tight programs, stable models coincide with supported models, and stable partial models coincide with supported partial models.
    Used in Lemma 4.1 and several main proofs.
  • domain assumption Aravindan and Dung's theorem (Theorem 4.5, Aravindan and Dung 1995): P and lfp(P) have the same stable partial, regular, and stable models.
    Load-bearing for Lemma 4.2 and Theorem 5.4.
  • domain assumption Richard's theorem (Theorem 4.6, Richard 2010): a Boolean network whose influence graph has no odd cycle has no cyclic asynchronous attractor.
    Core of Theorem 4.7, the main odd-cycle result.
  • domain assumption Aracena's bound (Theorem 4.21, Aracena 2008): a Boolean network with an even feedback vertex set U has at most 2^|U| fixed points.
    Core of Theorem 4.22, the stable-model counting bound.
  • domain assumption Richard and Ruet (2013) and Veliz-Cuba et al. (2012) theorems on AND-NOT Boolean networks and delocalizing triples (Theorems 4.9, 4.13, 4.23).
    Used for the uni-rule Datalog^neg results.
  • domain assumption Trinh et al. 2025a results on complete trap spaces and trap space characterization (Lemma 3.1 and Proposition 5.8), and Trinh et al. 2025b results on attractors in AND-NOT networks (Theorems 4.15 and 4.25).
    Used in Theorems 3.2, 4.16, 4.26, and Corollary 5.7; these are recent works by the same group, not independently verified here.
  • domain assumption Every Datalog^neg program has at least one stable partial model.
    Used without proof in Corollary 4.5; needed so that uniqueness of stable partial models is non-vacuous. Standard from three-valued stable model theory.
invented entities (2)
  • Stable trap space
    purpose: A three-valued interpretation whose set of two-valued completions is closed under the stable transition operator; used to characterize regular models (Theorem 5.4).
    Introduced as Definition 5.2; a formal mathematical notion with proofs in the paper, not an empirical postulate.
  • Supported trap space
    purpose: A three-valued interpretation whose completions are closed under the supported transition operator; used to connect supported partial models to trap spaces.
    Introduced as Definition 5.2; a formal mathematical notion with proofs in the paper, not an empirical postulate.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the Boolean Network Theory of Datalog$^\neg$." pith.science (2026). https://pith.science/paper/PNYBR4WR

@misc{pith2026250415417,
  author       = {Pith},
  title        = {Pith review of: On the Boolean Network Theory of Datalog$^\neg$},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PNYBR4WR}},
  note         = {Machine review of arXiv:2504.15417}
}
abstract

Datalog$^\neg$ is a central formalism used in a variety of domains ranging from deductive databases and abstract argumentation frameworks to answer set programming. Its model theory is the finite counterpart of the logical semantics developed for normal logic programs, mainly based on the notions of Clark's completion and two-valued or three-valued canonical models including supported, stable, regular and well-founded models. In this paper we establish a formal link between Datalog$^\neg$ and Boolean network theory first introduced for gene regulatory networks. We show that in the absence of odd cycles in a Datalog$^\neg$ program, the regular models coincide with the stable models, which entails the existence of stable models, and in the absence of even cycles, we prove the uniqueness of stable partial models and regular models. This connection also gives new upper bounds on the numbers of stable partial, regular, and stable models of a Datalog$^\neg$ program using the cardinality of a feedback vertex set in its atom dependency graph. Interestingly, our connection to Boolean network theory also points us to the notion of trap spaces. In particular we show the equivalence between subset-minimal stable trap spaces and regular models.

Figures

Figures reproduced from arXiv: 2504.15417 by the authors.

Figure 1
Figure 1. (a) Atom dependency graph adg(P), (b) stable transition graph tgst(P), and (c) supported transition graph tgsp(P) of Datalog¬ program P of Example 2.1. 2.2 Boolean Networks 2.2.1 Definition A Boolean Network (BN) f is a finite set of Boolean functions on a finite set of Boolean variables denoted by varf . Each variable v ∈ varf is associated with a Boolean function fv : B |varf | → B. Function fv is called constant … view at source ↗
Figure 2
Figure 2. (a) G(f), (b) sstg(f), and (c) astg(f). The BN f is given in Example 2.2. faithful representation of Datalog¬ programs in terms of Boolean dynamics, and serves as a foundation for structural and dynamical analysis in the subsequent sections. Definition 3.1 Let P be a Datalog¬ program. We define a BN f that corresponds to P as follows: varf = HBP and for each v ∈ varf , fv = _ r∈gr(P ), v=h(r) bf(r). By convention, i… view at source ↗
Figure 3
Figure 3. (a) Atom dependency graph adg(P) of the Datalog¬ program P, (b) influence graph G(f) of the BN f. The details of P and f are given in Example 3.1 [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Atom dependency graph of the Datalog¬ program P given in Example 4.2. Uni-rule Datalog¬ Programs. We now turn our attention to a syntactic fragment of Datalog¬ programs, which we refer to as uni-rule Datalog¬ programs. These are pro￾grams in which each ground atom appe…
Figure 5
Figure 5. Figure 5: Signed directed graph G of Example 4.3. Cycles in the influence graph of an AND-NOT BN (or equivalently, the atom depen￾dency graph of a uni-rule Datalog¬ program) can critically impact the existence of fixed points or stable models. Richard and Ruet (2013) showed that…
Figure 6
Figure 6. Figure 6: Atom dependency graph of the Datalog¬ program of Remark 4.6 [PITH_FULL_IMAGE:figures/full_fig_p032_6.png]
Figure 7
Figure 7. Figure 7: Atom dependency graph of the uni-rule Datalog [PITH_FULL_IMAGE:figures/full_fig_p034_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 13 canonical work pages

  1. [6]

    Dung, P. M. and Kanchanasut, K. A fixpoint approach to declarative semantics of logic programs. In Proc. of NACLP 1989, pp. 604–625. MIT Press. Eiter, T. , Leone, N. , and Sacc `a, D. On the partial semantics for disjunctive deductive databases. Ann. Math. Artif. Intell. , 19(1-2):59–96

  2. [9]

    , Knorr, M

    Heyninck, J. , Knorr, M. , and Leite, J. Abstract dialectical frameworks are Boolean net- works. In Proc. of LPNMR 2024, pp. 98–111. Springer. Inoue, K. Logic programming for Boolean networks. In Proc. of IJCAI 2011, pp. 924–930. IJCAI/AAAI. Inoue, K. and Sakama, C. Oscillating behavior of logic programs. In Correct Reasoning - Essays on Logic-Based AI in...

  3. [14]

    On the number of asynchronous attractors in AND-NOT Boolean networks

    Trinh, V.-G. , Benhamou, B. , Soliman, S. , and F ages, F. Graphical conditions for the exis- tence, unicity and number of regular models. In Proc. of ICLP 2024b, pp. 175–187. Trinh, V.-G. , P astva, S., Rozum, J. , P ark, K. H. , and Albert, R. On the number of asynchronous attractors in AND-NOT Boolean networks. arXiv preprint arXiv:2503.19147 2025b. Ve...

  4. [15]

    and Yuan, L

    You, J. and Yuan, L. On the equivalence of semantics for normal logic programs. J. Log. Program., 22(3):211–222 1995

  5. [1973]

    Static Analysis of Logic Programs via Boolean Networks

    Trinh, V.-G. and Benhamou, B. Static analysis of logic programs via Boolean networks. CoRR, abs/2407.09015

  6. [1991]

    On the Boolean Network Theory of Datalog ¬ 45 Apt, K. R. , Blair, H. A. , and W alker, A. Towards a theory of declarative knowledge. In Foundations of Deductive Databases and Logic Programming 1988, pp. 89–148. Elsevier. Aracena, J. Maximum number of fixed points in regulatory Boolean network s. Bull. Math. Biol., 70(5):1398–1409

  7. [1994]

    and Hecher, M

    F andinno, J. and Hecher, M. Treewidth-aware complexity in ASP: not all positive cycles are equally hard. In Proc. of AAAI 2021, pp. 6312–6320. AAAI Press. F andinno, J. and Lifschitz, V. Positive dependency graphs revisited. Theory Pract. Log. Program., 23(5):1128–1137

  8. [1995]

    , Guti´errez, S

    Azpeitia, E. , Guti´errez, S. M. , Rosenblueth, D. A. , and Zapata, O. Bridging abstract dialectical argumentation and Boolean gene regulation. CoRR, abs/2407.06106

Show all 15 references
  1. [1999]

    Clark, K. L. Negation as failure. In Logic and Data Bases, Symposium on Logic and Data Bases 1977, pp. 293–322, New York. Plemum Press. Costantini, S. On the existence of stable models of non-stratified logic pro grams. Theory Pract. Log. Program., 6(1-2):169–212

  2. [2002]

    and Zhao, X

    Lin, F. and Zhao, X. On odd and even cycles in normal logic programs. In Proceedings of the Nineteenth National Conference on Artificial Intelligence , Sixteenth Conference on Innovative Applications of Artificial Intelligence 2004, pp. 80–85. AAAI Press / The MIT Press. Linke, ...

  3. [2006]

    and Provetti, A

    Costantini, S. and Provetti, A. Conflict, consistency and truth-dependencies in graph rep- resentations of answer set logic programs. In Second International Workshop on Graph Struc- tures for Knowledge Representation and Reasoning 2011, pp. 68–90. Springer. Dietz, E. , H¨olldo...

  4. [2014]

    , Dvor´ak, W

    Dimopoulos, Y. , Dvor´ak, W. , and K ¨onig, M. Connecting abstract argumentation and Boolean networks. In Proc. of COMMA 2024, pp. 85–96. IOS Press. Dimopoulos, Y. and Torres, A. Graph theoretical structures in logic programs and default theories. Theor. Comput. Sci. , 170(1-2...

  5. [2020]

    and Schlipf, J

    Seitzer, J. and Schlipf, J. S. Affordable classes of normal logic programs. In Proc. of LPNMR 1997, pp. 92–111. Springer. Thomas, R. Boolean formalisation of genetic control circuits. J. Theor. Biol. , 42:565–583

  6. [2023]

    Fichte, J. K. The good, the bad, and the odd: Cycles in answer-set programs . In Proc. of ESSLLI 2011, pp. 78–90. Springer. Gelfond, M. and Lifschitz, V. The stable model semantics for logic programming. In Proc. of ICLP/SLP 1988, pp. 1070–1080. MIT Press. Guessarian, I. and P...

  7. [2024]

    , Benhamou, B

    Trinh, V.-G. , Benhamou, B. , and P aulev´e, L. mpbn: a simple tool for efficient edition and analysis of elementary properties of Boolean networks. CoRR, abs/2403.06255 2024a. Trinh, V.-G. , Benhamou, B. , and Risch, V. Graphical analysis of abstract argumentation frameworks vi...

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.