A SAT-based algorithm for context matching