Repetition in Literals

[Sherman]

Hi.
It is prefered to check the redundancy of a literal before inserting into a
clause? Example: in the case of (x1 + x2 + !x4 + x2), x2 is repeated and
when evaluating satisfiability it does not affect the result at all if
written as (x1 + x2 + !x4). So for memory-saving, would it be recommended to
check before inserting?
Thank you.

Sherman

[Alexander Smith]

Hello,

You do not need to check for redundancy before inserting it into a clause.
You are correct in pointing out that it would be more efficient to
eliminate them, but you do not have to do that for this lab.

There are other things you could also do to be more efficient. For
example, if a clause has both x1 and !x1, then it is automatically
satisfied. In this case, it would be more efficient not to store the
clause at all. Again, this is something you don't need to do for this lab.

Alexander

Post by Sherman
Hi.
It is prefered to check the redundancy of a literal before inserting into a
clause? Example: in the case of (x1 + x2 + !x4 + x2), x2 is repeated and
when evaluating satisfiability it does not affect the result at all if
written as (x1 + x2 + !x4). So for memory-saving, would it be recommended to
check before inserting?
Thank you.
Sherman