Re: SAT: Equivalency vs. Transitivity

From: Daniel A. Jimenez (djimenez_at_cs.utexas.edu)
Date: 07/08/04 

Date: 8 Jul 2004 09:32:41 -0500

In article <Xns9520A57CE722lramboobmarlcom@68.12.19.6>,
Lash Rambo <lrambo@obmarl.com> wrote:
>It seems to me that equivalency is just a special case of transitivity.
>For instance, given the "defining clauses"
>
>{ (l_1, ~l_2), (~l_1, l_2) },
>
>we know l_1 and l_2 are equivalent. So, from the "target" clause
>
>(l_2, l_3),
>
>we can infer the "resultant" clause
>
>(l_1, l_3).
>
>However, we could have done the same via transitivity on the defining
>clause
>
>(l_1, ~l_2)
>
>and the target clause
>
>(l_2, l_3).
>
>I've noticed it is always that case that equivalency only lets us infer
>the same clauses we could infer from transitivity alone.
>
>Am I missing something? If not, what's so great about equivalence? What
>does equivalence let us do that transitivity does not?

Suppose we know l1 and l2 are equivalent. Then we can get rid of l2
everywhere in the formula, replacing it with l1. Now we have fewer
variables to keep track of, reducing the search space for e.g. the
Davis-Putnam splitting rule. 

-- 
Daniel Jiménez                     djimenez@cs.utexas.edu
"I've so much music in my head" -- Maurice Ravel, shortly before his death.
"                             " -- John Cage