On Tractability and Congruence Distributivity

LICS '06 Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science(2007)

引用 35|浏览0
暂无评分
摘要
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
正在生成论文摘要