Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR

Abstract. The union-find algorithm can be seen as solving simple equations between variables or constants. With a few lines of code change, we generalise its implementation in CHR from equality to arbitrary binary relations. By choosing the appropriate relations, we can derive fast incremental algorithms for solving certain propositional logic (SAT) problems and polynomial equations in two variables. In general, we prove that when the relations are bijective functions, our generalisation yields a correct algorithm. We also show that bijectivity is a necessary condition for correctness if the relations include the identity function. The rules of our generic algorithm have additional properties that make them suitable for incorporation into constraint solvers: from classical union-find, they inherit a compact solved form and quasi-linear time and space complexity. By nature of CHR, they are anytime and online algorithms. They solve and simplify the constraints in the problem, and can t...

• Type: Conference
• Year: 2007
• Where: CSCLP
• Authors: Thom W. Frühwirth
• Keywords: Algorithm, Arbitrary Binary Relations, Artificial Intelligence, Certain Propositional Logic, CSCLP 2007