pith. sign in

arxiv: 2407.04924 · v4 · submitted 2024-07-06 · 🧮 math.RA · cs.CC· cs.LO

Symmetric Linear Arc Monadic Datalog and Gadget Reductions

Manuel Bodirsky , Florian Starke This is my paper

Pith reviewed 2026-05-23 22:50 UTC · model grok-4.3

classification 🧮 math.RA cs.CCcs.LO
keywords symmetric linear arc monadic Dataloggadget reductionunfolded caterpillar dualityquasi Maltsev operationsk-absorptive operationsconstraint satisfaction problemsfinite-domain CSPDatalog fragments
0
0 comments X

The pith

CSPs solvable by symmetric linear arc monadic Datalog are exactly those with a gadget reduction to one Boolean CSP.

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

The paper gives three equivalent ways to identify which finite-domain constraint satisfaction problems admit a solution via a symmetric linear arc monadic Datalog program. The central claim equates this solvability with the existence of a gadget reduction to a fixed Boolean constraint satisfaction problem. Equivalent descriptions are supplied through a homomorphism duality called unfolded caterpillar duality and through the presence of quasi Maltsev operations together with k-absorptive operations of every arity nk. The same equivalences immediately yield that membership in this Datalog class is decidable for any finite template.

Core claim

A finite-domain CSP can be solved by a slam Datalog program if and only if it has a gadget reduction to a particular Boolean constraint satisfaction problem. Equivalently, the CSP satisfies unfolded caterpillar duality and its polymorphism clone contains quasi Maltsev operations and k-absorptive operations of arity nk for all positive integers n and k. These equivalences also imply that it is decidable whether any given finite-domain CSP can be expressed by a slam Datalog program.

What carries the argument

gadget reduction to a fixed Boolean CSP, which equates Datalog solvability with unfolded caterpillar duality and the listed algebraic minor conditions

If this is right

  • Expressibility of a finite-domain CSP in slam Datalog is decidable.
  • The algebraic conditions on quasi Maltsev and k-absorptive operations are necessary and sufficient for slam Datalog solvability.
  • Unfolded caterpillar duality exactly captures the CSPs solvable in this Datalog fragment.
  • slam Datalog sits at the intersection of the arc-monadic, linear, and symmetric-linear fragments.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The gadget-reduction view may let researchers transfer tractability results between the Boolean target and other templates.
  • Checking the algebraic conditions on small domains offers a practical route to decide slam Datalog expressibility.
  • Analogous gadget or duality characterizations could be sought for the larger fragments that omit one of the three restrictions.

Load-bearing premise

The three characterizations remain equivalent for every finite-domain template.

What would settle it

A concrete finite template that possesses quasi Maltsev and k-absorptive operations yet admits no gadget reduction to the Boolean target CSP.

Figures

Figures reproduced from arXiv: 2407.04924 by Florian Starke, Manuel Bodirsky.

Figure 1
Figure 1. Figure 1: An example of the incidence graph of a caterpillar ( [PITH_FULL_IMAGE:figures/full_fig_p012_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example of an (a, b)-unfolding T ′ of a tree T. Definition 2.12. Let T be an (injective) tree and let a and b be distinct elements of T that are not leaves. The (a, b)-unfolding of T is the canonical database of the formula φ1(a) ∧ ψ(a, b′ ) ∧ ψ(a ′ , b′ ) ∧ ψ(a ′ , b) ∧ φ2(b) where φ1, φ2, and ψ are as defined above. A unfolding of T is a structure T ′ that is obtained by a sequence T = T1,T2, . . . ,Tn =… view at source ↗
Figure 3
Figure 3. Figure 3: At the top there is a picture of a caterpillar [PITH_FULL_IMAGE:figures/full_fig_p025_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The lattice of 2-element structures with respect t [PITH_FULL_IMAGE:figures/full_fig_p031_4.png] view at source ↗
read the original abstract

A Datalog program solves a constraint satisfaction problem (CSP) if and only if it derives the goal predicate precisely on the unsatisfiable instances of the CSP. There are three Datalog fragments that are particularly important for finite-domain constraint satisfaction: arc monadic Datalog, linear Datalog, and symmetric linear Datalog, each having good computational properties. We consider the fragment of Datalog where we impose all of these restrictions simultaneously, i.e., we study \emph{symmetric linear arc monadic (slam) Datalog}. We characterise the CSPs that can be solved by a slam Datalog program as those that have a gadget reduction to a particular Boolean constraint satisfaction problem. We also present exact characterisations in terms of a homomorphism duality (which we call \emph{unfolded caterpillar duality}), and in universal-algebraic terms (using known minor conditions, namely the existence of quasi Maltsev operations and $k$-absorptive operations of arity $nk$}, for all $n,k \geq 1$). Our characterisations also imply that the question whether a given finite-domain CSP can be expressed by a slam Datalog program is decidable.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The manuscript characterizes the finite-domain CSPs solvable by symmetric linear arc monadic (slam) Datalog as those that admit a gadget reduction to a particular Boolean CSP. Equivalent characterizations are given in terms of unfolded caterpillar duality and algebraic minor conditions (existence of quasi Maltsev operations and k-absorptive operations of arity nk for all n, k ≥ 1). These results imply that membership in this class is decidable.

Significance. If the equivalences hold for arbitrary finite-domain templates, the work supplies three independent characterizations of slam Datalog solvability, connecting a restricted Datalog fragment to gadget reductions, a new form of homomorphism duality, and known minor conditions from universal algebra. The implied decidability result is a concrete strength, as it converts an apparently infinite family of minor conditions into a finite check.

major comments (1)
  1. [Main equivalence theorem (Section 3 / Theorem 3.4 and Section 5)] The central theorem equating the three characterizations (gadget reduction to the Boolean CSP, unfolded caterpillar duality, and the quasi Maltsev + k-absorptive minor conditions) is stated for arbitrary finite-domain templates. The gadget-reduction direction and the duality definition must be shown to impose no hidden restrictions on signature arity or relation arities; otherwise the equivalence fails to hold uniformly and the decidability claim does not follow.
minor comments (2)
  1. [Abstract] The abstract refers to 'a particular Boolean constraint satisfaction problem' without naming the target template; the introduction should state the target explicitly.
  2. [Introduction] The definition of 'unfolded caterpillar duality' appears only after the main theorem; a brief informal description in the introduction would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and for identifying the need to confirm uniformity of the characterizations. We address the concern below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [Main equivalence theorem (Section 3 / Theorem 3.4 and Section 5)] The central theorem equating the three characterizations (gadget reduction to the Boolean CSP, unfolded caterpillar duality, and the quasi Maltsev + k-absorptive minor conditions) is stated for arbitrary finite-domain templates. The gadget-reduction direction and the duality definition must be shown to impose no hidden restrictions on signature arity or relation arities; otherwise the equivalence fails to hold uniformly and the decidability claim does not follow.

    Authors: The definitions of gadget reduction (Section 2) and unfolded caterpillar duality (Section 4) are formulated for arbitrary finite signatures and arbitrary relation arities; the gadget construction replaces each constraint with a fixed Boolean gadget whose size depends only on the template relations, not on any global arity bound. The algebraic conditions (quasi-Maltsev and k-absorptive operations of all arities nk) are likewise stated without arity restrictions. The proofs of Theorem 3.4 and the equivalences in Section 5 proceed by direct translation between these notions and never invoke an upper bound on arities. To make this explicit we will insert a short clarifying paragraph after Definition 2.3 and before Theorem 3.4 stating that all three characterizations apply uniformly to any finite-domain template. With this addition the decidability claim remains valid, as the finite check for the minor conditions is independent of signature size. revision: yes

Circularity Check

0 steps flagged

No circularity: three independent characterizations proven equivalent without reduction to inputs or self-citation chains

full rationale

The paper states three characterizations of slam Datalog-solvable CSPs (gadget reduction to a fixed Boolean CSP, unfolded caterpillar duality, and algebraic minor conditions on quasi Maltsev plus k-absorptive operations) and claims they are equivalent, with decidability as a corollary. No quoted step reduces a 'prediction' or central claim to a fitted parameter, self-definition, or load-bearing self-citation. The algebraic conditions are explicitly 'known minor conditions,' indicating external reference. The derivation chain is self-contained against external benchmarks (standard CSP duality and minor-condition techniques) with no exhibited construction that forces equivalence by renaming or ansatz smuggling. This is the normal non-finding for a theoretical equivalence proof.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only abstract available; no explicit free parameters, axioms, or invented entities can be extracted. The characterizations rest on background results from universal algebra and CSP theory whose details are not supplied.

pith-pipeline@v0.9.0 · 5737 in / 1079 out tokens · 26472 ms · 2026-05-23T22:50:32.795983+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

  1. [1]

    F. N. Afrati and S. S. Cosmadakis. Expressiveness of rest ricted recursive queries (extended abstract). In D. S. Johnson, editor, Proceedings of the 21st Annual ACM Symposium on Theory of Computing, May 14-17, 1989, Seattle, Wa shigton, USA , pages 113–126. ACM, 1989

    work page 1989

  2. [2]

    Atserias, A

    A. Atserias, A. A. Bulatov, and A. Dawar. Affine systems of e quations and counting infinitary logic. Theoretical Computer Science , 410(18):1666–1683, 2009

    work page 2009

  3. [3]

    Barto and M

    L. Barto and M. Kozik. Constraint satisfaction problems of bounded width. In Proceedings of Symposium on Foundations of Computer Science (FOCS), pages 595–603, 2009

    work page 2009

  4. [4]

    Barto and M

    L. Barto and M. Kozik. Constraint satisfaction problems of bounded width. In Pro- ceedings of the Annual Symposium on Foundations of Computer S cience (FOCS) , pages 595–603, 2009

    work page 2009

  5. [5]

    Barto, M

    L. Barto, M. Kozik, and R. Willard. Near unanimity constr aints have bounded pathwidth duality. In Proceedings of the 27th ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 125–134, 2012

    work page 2012

  6. [6]

    Barto, J

    L. Barto, J. Oprˇ sal, and M. Pinsker. The wonderland of re flections. Israel Journal of Mathematics , 223(1):363–398, 2018

    work page 2018

  7. [7]

    Bodirsky

    M. Bodirsky. Graph homomorphisms and universal algebra . Lecture Notes, https://wwwpub.zih.tu-dresden.de/ ~bodirsky/GH-UA.pdf, 2023

    work page 2023

  8. [8]

    Bodirsky, J

    M. Bodirsky, J. Bul ´ ın, F. Starke, and M. Wernthaler. The smallest hard trees. Constraints, abs/2205.07528, 2022. 32

    work page arXiv 2022

  9. [9]

    Bodirsky and H

    M. Bodirsky and H. Chen. Oligomorphic clones. Algebra Universalis, 57(1):109–125, 2007

    work page 2007

  10. [10]

    Bodirsky and V

    M. Bodirsky and V. Dalmau. Datalog and constraint satis faction with infinite tem- plates. Journal on Computer and System Sciences , 79:79–100, 2013. A preliminary version appeared in the proceedings of the Symposium on Theo retical Aspects of Computer Science (STACS’05)

    work page 2013

  11. [11]

    Bodirsky and F

    M. Bodirsky and F. Starke. Maximal digraphs with respec t to primitive positive constructability. Combinatorica, 42:997–1010, 2022

    work page 2022

  12. [12]

    Bodirsky, F

    M. Bodirsky, F. Starke, and A. Vucaj. Smooth digraphs mo dulo primitive positive constructability and cyclic loop conditions. International Journal on Algebra and Computation, 31(5):939–967, 2021. Preprint available at ArXiv:1906.0 5699

    work page 2021

  13. [13]

    Bodirsky and A

    M. Bodirsky and A. Vucaj. Two-element structures modul o primitive posi- tive constructability. Algebra Universalis , 81(20), 2020. Preprint available at ArXiv:1905.12333

    work page arXiv 2020

  14. [14]

    A. A. Bulatov. A dichotomy theorem for nonuniform CSPs. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berk eley, CA, USA, October 15-17, pages 319–330, 2017

    work page 2017

  15. [15]

    A. A. Bulatov, A. Krokhin, and B. Larose. Dualities for Constraint Satisfaction Problems, pages 93–124. Springer Berlin Heidelberg, Berlin, Heidel berg, 2008

    work page 2008

  16. [16]

    Bul ´ ın, A

    J. Bul ´ ın, A. A. Krokhin, and J. Oprˇ sal. Algebraic appr oach to promise constraint satisfaction. In Proceedings of the 51st Annual ACM SIGACT Symposium on The- ory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019 , pages 602– 613, 2019

    work page 2019

  17. [17]

    Carvalho, V

    C. Carvalho, V. Dalmau, and A. Krokhin. CSP duality and t rees of bounded pathwidth. Theoretical Computer Science , 411:3188–3208, 2010

    work page 2010

  18. [18]

    Carvalho, V

    C. Carvalho, V. Dalmau, and A. A. Krokhin. Two new homomo rphism dualities and lattice operations. J. Log. Comput. , 21(6):1065–1092, 2011

    work page 2011

  19. [19]

    A. K. Chandra and P. M. Merlin. Optimal implementation o f conjunctive queries in relational data bases. In Proceedings of the Symposium on Theory of Computing (STOC), pages 77–90, 1977

    work page 1977

  20. [20]

    Chen and B

    H. Chen and B. Larose. Asking the metaquestions in const raint tractability. TOCT, 9(3):11:1–11:27, 2017

    work page 2017

  21. [21]

    V. Dalmau. Linear Datalog and bounded path duality of re lational structures. Logical Methods in Computer Science , 1(1), 2005. 33

    work page 2005

  22. [22]

    Dalmau and B

    V. Dalmau and B. Larose. Maltsev + Datalog → symmetric Datalog. In Proceed- ings of the Twenty-Third Annual IEEE Symposium on Logic in Comput er Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA , pages 297–306. IEEE Computer Society, 2008

    work page 2008

  23. [23]

    Dalmau and J

    V. Dalmau and J. Oprˇ sal. Local consistency as a reducti on between constraint satisfaction problems, 2023

    work page 2023

  24. [24]

    Dalmau and J

    V. Dalmau and J. Pearson. Closure functions and width 1 p roblems. In Proceedings of the International Conference on Principles and Practice of Constraint Program- ming (CP) , pages 159–173, 1999

    work page 1999

  25. [25]

    L. Egri, B. Larose, and P. Tesson. Symmetric Datalog and constraint satisfaction problems in logspace. In Proceedings of the Symposium on Logic in Computer Science (LICS) , pages 193–202, 2007

    work page 2007

  26. [26]

    L. Egri, B. Larose, and P. Tesson. Directed st-connecti vity is not expressible in symmetric Datalog. In Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Pro ceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, pages 17...

    work page 2008

  27. [27]

    Feder and M

    T. Feder and M. Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: a study through Datalog an d group theory. SIAM Journal on Computing , 28:57–104, 1999

    work page 1999

  28. [28]

    Hell and J

    P. Hell and J. Neˇ setˇ ril. Graphs and Homomorphisms . Oxford University Press, Oxford, 2004

    work page 2004

  29. [29]

    P. Hell, J. Neˇ setˇ ril, and X. Zhu. Duality and polynomi al testing of tree homomor- phisms. TAMS, 348(4):1281–1297, 1996

    work page 1996

  30. [30]

    W. Hodges. A shorter model theory . Cambridge University Press, Cambridge, 1997

    work page 1997

  31. [31]

    Jeavons, D

    P. Jeavons, D. Cohen, and M. Cooper. Constraints, consi stency and closure. Arti- ficial Intelligence , 101(1-2):251–265, 1998

    work page 1998

  32. [32]

    P. C. Kanellakis. Logic programming and parallel complexity , page 547–585. Mor- gan Kaufmann Publishers Inc., San Francisco, CA, USA, 1988. Book chapter in ‘Foundations of Deductive Databases and Logic Programming ’

    work page 1988

  33. [33]

    A. Kazda. n-permutability and linear Datalog implies symmetric Datal og. Logical Methods in Computer Science , Volume 14, Issue 2, Apr. 2018

    work page 2018

  34. [34]

    Kozik, A

    M. Kozik, A. Krokhin, M. Valeriote, and R. Willard. Char acterizations of several Maltsev conditions. Algebra universalis, 73(3):205–224, 2015. 34

    work page 2015

  35. [35]

    Larose and P

    B. Larose and P. Tesson. Universal algebra and hardness results for constraint satisfaction problems. Theoretical Computer Science , 410(18):1629–1647, 2009

    work page 2009

  36. [36]

    Larose and L

    B. Larose and L. Z´ adori. Bounded width problems and alg ebras. Algebra Univer- salis, 56(3-4):439–466, 2007

    work page 2007

  37. [37]

    Meyer and F

    S. Meyer and F. Starke. Finite simple groups in the primi tive positive constructabil- ity poset. 2024

    work page 2024

  38. [38]

    P¨ oschel and L

    R. P¨ oschel and L. A. Kaluˇ znin. Funktionen- und Relationenalgebren . Deutscher Verlag der Wissenschaften, Berlin, 1979

    work page 1979

  39. [39]

    B. Rossman. Homomorphism preservation theorems. Journal of the ACM , 55(3), 2008

    work page 2008

  40. [40]

    T. J. Schaefer. The complexity of satisfiability proble ms. In Proceedings of the Symposium on Theory of Computing (STOC) , pages 216–226, 1978

    work page 1978

  41. [41]

    F. Starke. Digraphs modulo primitive positive constru ctability. Preprint, 2024. PhD dissertation, Institute of Algebra, TU Dresden

    work page 2024

  42. [42]

    Vucaj and D

    A. Vucaj and D. Zhuk. Submaximal clones over a three-ele ment set up to minor- equivalence, 2024

    work page 2024

  43. [43]

    D. Zhuk. A proof of the CSP dichotomy conjecture. J. ACM , 67(5):30:1–30:78, 2020

    work page 2020

  44. [44]

    D. N. Zhuk. A proof of CSP dichotomy conjecture. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, US A, October 15- 17, pages 331–342, 2017. https://arxiv.org/abs/1704.01914. 35

    work page arXiv 2017