Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR
| |
|
Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR
Thom Frühwirth4 
| (4) |
Faculty of Computer Science, University of Ulm, Germany |
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 test them for entailment,
even when the constraints arrive incrementally.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|