# Re: SAT: Equivalency vs. Transitivity

**From:** Daniel A. Jimenez (*djimenez_at_cs.utexas.edu*)

**Date:** 07/08/04

**Next message:**Arthur J. O'Dwyer: "Re: paper claiming p=np and soap bubbles"**Previous message:**Dr A. N. Walker: "Re: Efficient bounded heap without 'overflow' ?"**In reply to:**Lash Rambo: "SAT: Equivalency vs. Transitivity"**Next in thread:**Lash Rambo: "Re: SAT: Equivalency vs. Transitivity"**Reply:**Lash Rambo: "Re: SAT: Equivalency vs. Transitivity"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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

**Next message:**Arthur J. O'Dwyer: "Re: paper claiming p=np and soap bubbles"**Previous message:**Dr A. N. Walker: "Re: Efficient bounded heap without 'overflow' ?"**In reply to:**Lash Rambo: "SAT: Equivalency vs. Transitivity"**Next in thread:**Lash Rambo: "Re: SAT: Equivalency vs. Transitivity"**Reply:**Lash Rambo: "Re: SAT: Equivalency vs. Transitivity"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]