On the Complexity Dichotomy for the Satisfiability of Systems of Term Equations over Finite Algebras

For a fixed finite algebra A, we consider the decision problem SysTerm(A): does a given system of term equations have a solution in A? This is equivalent to a constraint satisfaction problem (CSP) for a relational structure whose relations are the graphs of the basic operations of A. From the complexity dichotomy for CSP over fixed finite templates due to Bulatov [4] and Zhuk [18], it follows that SysTerm(A) for a finite algebra A is in P if A has a not necessarily idempotent Taylor polymorphism and is NP-complete otherwise. More explicitly, we show that for a finite algebra A in a congruence modular variety (e.g. for a quasigroup), SysTerm(A) is in P if the core of A is abelian and is NP-complete otherwise. Given A by the graphs of its basic operations, we show that this condition for tractability can be decided in quasi-polynomial time.