Constraint Satisfaction Problems over Finitely Bounded Homogeneous Structures: a Dichotomy between FO and L-hard
Pith reviewed 2026-05-16 09:57 UTC · model grok-4.3
The pith
CSPs over first-order expansions of finitely bounded homogeneous model-complete cores are either first-order definable or L-hard under first-order reduction.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
CSPs over first-order expansions of finitely bounded homogeneous model-complete cores are either first-order definable and hence in non-uniform AC0 or L-hard under first-order reduction. The proof proceeds by first establishing a new proof of the Larose-Tesson theorem for finite structures and then generalizing that argument to the infinite case.
What carries the argument
A new proof of the Larose-Tesson theorem, first obtained for finite structures and then lifted to infinite structures, that separates the CSPs into first-order definable versus L-hard cases.
If this is right
- No CSP in this class can have complexity strictly between first-order logic and L.
- The dichotomy applies uniformly to every first-order expansion of any such core.
- The tractable cases admit non-uniform AC0 decision procedures.
- The result supplies the broadest complexity classification known for structures inside the Bodirsky-Pinsker conjecture.
Where Pith is reading between the lines
- The lifting technique may extend to other descriptive-complexity classifications that currently separate finite and infinite cases.
- Concrete homogeneous structures such as the random graph or the rational order can now be placed on one side or the other of the dichotomy by checking the model-complete-core condition.
- If the full Bodirsky-Pinsker conjecture holds, the present result would imply that all remaining NP-complete cases lie outside the model-complete-core class.
Load-bearing premise
The structures under consideration are model-complete cores and the new proof of the Larose-Tesson theorem for finite structures lifts directly to the infinite case without additional hidden assumptions on the reducts.
What would settle it
A concrete first-order expansion of a finitely bounded homogeneous model-complete core whose CSP is solvable in deterministic logarithmic space yet not first-order definable would falsify the claimed dichotomy.
read the original abstract
Feder-Vardi conjecture, which proposed that every finite-domain Constraint Satisfaction Problem (CSP) is either in P or it is NP-complete, has been solved independently by Bulatov and Zhuk almost ten years ago. Bodirsky-Pinsker conjecture which states a similar dichotomy for countably infinite first-order reducts of finitely bounded homogeneous structures is wide open. In this paper, we prove that CSPs over first-order expansions of finitely bounded homogeneous model-complete cores are either first-order definable (and hence in non-uniform AC$^0$) or L-hard under first-order reduction. It is arguably the most general complexity dichotomy when it comes to the scope of structures within Bodirsky-Pinsker conjecture. Our strategy is that we first give a new proof of Larose-Tesson theorem, which provides a similar dichotomy over finite structures, and then generalize that new proof to infinite structures.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proves that CSPs over first-order expansions of finitely bounded homogeneous model-complete cores are either first-order definable (hence in non-uniform AC^0) or L-hard under first-order reductions. The argument proceeds by first supplying a new proof of the Larose-Tesson theorem for finite structures and then generalizing that proof to the infinite case using homogeneity and finite boundedness.
Significance. If the generalization holds, the result supplies the broadest known complexity dichotomy inside the scope of the Bodirsky-Pinsker conjecture, linking FO definability directly to non-uniform AC^0 and establishing L-hardness under FO reductions for the complementary case. The new finite proof and its explicit lift constitute a reusable technical contribution that may accelerate further progress on the full conjecture.
major comments (1)
- [Generalization from finite to infinite case] The central generalization step (from the new finite Larose-Tesson proof to infinite homogeneous structures) must explicitly identify which arguments in the finite case rely on finiteness (e.g., enumeration of polymorphisms or exhaustive case analysis) and show how homogeneity plus finite boundedness of the age substitute for them; without this identification the lift risks hidden assumptions on the reducts beyond model-completeness.
minor comments (1)
- [Introduction] The abstract and introduction should include a brief pointer to the precise statement of the Larose-Tesson theorem being reproved, for readers unfamiliar with the finite-domain literature.
Simulated Author's Rebuttal
We thank the referee for the positive assessment of the result and its significance within the Bodirsky-Pinsker conjecture, as well as for the constructive major comment. We address the point below and agree to strengthen the exposition of the generalization.
read point-by-point responses
-
Referee: [Generalization from finite to infinite case] The central generalization step (from the new finite Larose-Tesson proof to infinite homogeneous structures) must explicitly identify which arguments in the finite case rely on finiteness (e.g., enumeration of polymorphisms or exhaustive case analysis) and show how homogeneity plus finite boundedness of the age substitute for them; without this identification the lift risks hidden assumptions on the reducts beyond model-completeness.
Authors: We agree that an explicit identification will improve clarity. Our new proof of the Larose-Tesson theorem (Section 3) deliberately avoids enumeration of polymorphisms and exhaustive case analysis; it instead reduces to the model-complete core via a direct construction of a witnessing polymorphism from the assumption that the CSP is not FO-definable, using finiteness only to guarantee that the core exists and that the domain is finite for the AC0 upper bound. The generalization (Section 4) substitutes homogeneity for finiteness by invoking the Fraïssé limit property that every finite substructure embeds into the homogeneous structure, allowing the same polymorphism to be lifted uniformly; finite boundedness of the age replaces exhaustive search by ensuring only finitely many minimal forbidden substructures exist, which bounds the local configurations that must be considered. We will revise by inserting a dedicated paragraph at the start of Section 4 that maps each step of the finite proof to its infinite counterpart and states precisely where homogeneity and finite boundedness substitute for finiteness. revision: yes
Circularity Check
No circularity: new finite proof is independent and generalization uses it as base without reduction to inputs
full rationale
The paper explicitly states it first derives a new proof of the Larose-Tesson theorem for finite structures and only then generalizes that proof to the infinite case of first-order expansions of finitely bounded homogeneous model-complete cores. No quoted step equates a prediction or central claim to a fitted parameter, self-citation chain, or definitional renaming; the finite-case proof is presented as freshly constructed rather than presupposing the infinite result. The derivation chain therefore remains self-contained against external benchmarks.
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Standard background results from model theory (homogeneous structures, model-complete cores) and complexity theory (first-order reductions, AC0, L).
Reference graph
Works this paper leans on
-
[1]
On digraph coloring problems and treewidth duality
[Ats05] Albert Atserias. On digraph coloring problems and treewidth duality. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings , pages 106–115. IEEE Computer Society,
work page 2005
- [2]
-
[3]
A conference version appeared in the Proceedings of the 34th Symposium on Theoretical Aspects of Computer Science (STACS 2006), pages 646–
work page 2006
-
[4]
[BKNP25] Johanna Brunar, Marcin Kozik, Tom´ as Nagy, and Michael Pinsker. The sorrows of a smooth digraph: the first hardness criterion for infinite di- rected graph-colouring problems. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025 , pages 403–416. IEEE,
work page 2025
-
[5]
Near unanimity constraints have bounded pathwidth duality
[BKW12] Libor Barto, Marcin Kozik, and Ross Willard. Near unanimity constraints have bounded pathwidth duality. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croa- tia, June 25-28, 2012 , pages 125–134. IEEE Computer Society,
work page 2012
-
[6]
[BN06] Manuel Bodirsky and Jaroslav Neˇ setˇ ril
A conference version appeared in the Proceedings of the 43rd International Colloquium on Au- tomata, Languages, and Programming, ICALP 2016, pages 119:1-119:14. [BN06] Manuel Bodirsky and Jaroslav Neˇ setˇ ril. Constraint satisfaction with countable homogeneous templates. Journal of Logic and Computation , 16(3):359–373,
work page 2016
-
[7]
A conference version appeared in the proceedings of Computer Science Logic (CSL 2003). [Bod21] Manuel Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction. Lecture Notes in Logic. Cambridge University Press, Cambridge,
work page 2003
-
[8]
[BPP21] Manuel Bodirsky, Michael Pinsker, and Andr´ as Pongr´ acz
A conference version appeared in the Proceedings of STOC 2011, pages 655-664. [BPP21] Manuel Bodirsky, Michael Pinsker, and Andr´ as Pongr´ acz. Projective clone homomorphisms. Journal of Symbolic Logic , 86(1):148–161,
work page 2011
-
[9]
[Bul17] Andrei A. Bulatov. A dichotomy theorem for nonuniform CSPs. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Com- puter Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017 , pages 319–330, Berkeley,
work page 2017
-
[10]
27 [CDK08] Catarina Carvalho, V´ ıctor Dalmau, and Andrei A
IEEE Computer Society. 27 [CDK08] Catarina Carvalho, V´ ıctor Dalmau, and Andrei A. Krokhin. Caterpil- lar duality for constraint satisfaction problems. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA , pages 307–316. IEEE Computer Society,
work page 2008
-
[11]
Triplet reconstruction and all other phylogenetic csps are approximation resistant
[CM23] Vaggos Chatziafratis and Konstantin Makarychev. Triplet reconstruction and all other phylogenetic csps are approximation resistant. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023 , pages 253–284. IEEE,
work page 2023
-
[12]
Descriptive complexity of list h-coloring problems in logspace: A refined dichotomy
[DEH+15] V´ ıctor Dalmau, L´ aszl´ o Egri, Pavol Hell, Benoˆ ıt Larose, and Arash Rafiey. Descriptive complexity of list h-coloring problems in logspace: A refined dichotomy. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015 , pages 487–498. IEEE Computer Society,
work page 2015
-
[13]
Space complex- ity of list H -colouring: a dichotomy
[EHLR14] L´ aszl´ o Egri, Pavol Hell, Benoˆ ıt Larose, and Arash Rafiey. Space complex- ity of list H -colouring: a dichotomy. In Chandra Chekuri, editor, Pro- ceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5-7, 2014 , pages 349–365. SIAM,
work page 2014
-
[14]
Satisfiability of ordering csps above average is fixed-parameter tractable
[MMZ15] Konstantin Makarychev, Yury Makarychev, and Yuan Zhou. Satisfiability of ordering csps above average is fixed-parameter tractable. In Venkate- san Guruswami, editor, IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 975–993. IEEE Computer Society,
work page 2015
-
[15]
Strict width for constraint satis- faction problems over homogeneous strucures of finite duality
[NP24] Tom´ as Nagy and Michael Pinsker. Strict width for constraint satis- faction problems over homogeneous strucures of finite duality. CoRR, abs/2402.09951,
-
[16]
[NPW25] Tom´ as Nagy, Michael Pinsker, and Michal Wrona. New sufficient alge- braic conditions for local consistency over homogeneous structures of finite duality. CoRR, abs/2502.02090,
-
[17]
[Wro20a] Micha l Wrona. On the relational width of first-order expansions of finitely bounded homogeneous binary cores with bounded strict width. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbr¨ ucken, Germany, July 8-11, 2020 , pages 958–971, Saarbr¨ ucken,
work page 2020
-
[18]
ACM. [Wro20b] Micha l Wrona. Relational width of first-order expansions of homogeneous graphs with bounded strict width. In Christophe Paul and Markus Bl¨ aser, editors, 37th International Symposium on Theoretical Aspects of Com- puter Science, STACS 2020, March 10-13, 2020, Montpellier, France, vol- ume 154 of LIPIcs, pages 39:1–39:16. Schloss Dagstuhl -...
work page 2020
-
[19]
A proof of CSP dichotomy conjecture
[Zhu17] Dmitriy Zhuk. A proof of CSP dichotomy conjecture. In Chris Umans, edi- tor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017 , pages 331–342, Berkeley,
work page 2017
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.