On Tractability and Congruence Distributivity
LICS '06 Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science(2007)
摘要
Constraint languages that arise from finite algebras have recently been the
object of study, especially in connection with the Dichotomy Conjecture of
Feder and Vardi. An important class of algebras are those that generate
congruence distributive varieties and included among this class are lattices,
and more generally, those algebras that have near-unanimity term operations. An
algebra will generate a congruence distributive variety if and only if it has a
sequence of ternary term operations, called Jonsson terms, that satisfy certain
equations.
We prove that constraint languages consisting of relations that are invariant
under a short sequence of Jonsson terms are tractable by showing that such
languages have bounded relational width.
更多查看译文
关键词
tractability,universal algebra,formal verification tool,congruence distributivity. ∗,state variable,model checking tool,congruence distributivity,constraint satisfaction problem,infinite-state system,finitestate system,uclid project,uclid modeling language,process algebra,satisfiability,datalog,sequences,theorem proving
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要