An algorithm for matching contextualized schemas via SAT