wu :: forums - Print Page


    
      
        wu :: forums
        (http://www.ocf.berkeley.edu/~wwu/cgi-bin/yabb/YaBB.cgi)
      

        riddles >> cs >> NEW PROBLEM: 1-1SAT
        
(Message started by: Pietro K.C. on Sep 30^th, 2002, 1:53pm)

Title: NEW PROBLEM: 1-1SAT
Post by Pietro K.C. on Sep 30^th, 2002, 1:53pm

Let F₁₁ be a boolean formula in conjunctive normal form (that is, F₁₁ = C₁ AND ... AND C_m, where each C_i is of the form x_i1 OR ... OR x_in, where each literal x_ik is either a variable or its negation). Suppose each variable appears in the formula exactly once as x and once as NOT x. Find a polynomial-time algorithm that decides whether F₁₁ can be true for some attribution of variables, OR show that this problem is NP-complete.

Title: Re: NEW PROBLEM: 1-1SAT
Post by william wu on Jan 7^th, 2003, 4:15pm

My proposed polytime algorithm (highlight below area with mouse pointer to see):

We will repeatedly reduce the SAT expression, iterating through the literals and throwing them out. If we ever see a literal x and its complement ~x in the same OR clause, we can throw out x and ~x. And if x and ~x are in different clauses, we can still reduce by noting that (x OR y) AND (~x OR z) = (y OR z). (Note that y and z don't have to be individual variables, but rather could be logical expressions themselves.) So with each iteration we throw out a literal. In the end, if everything is thrown out, a satisfying assignment exists. But if we end up with any terms like x AND ~x, it's not satisfiable.

?

// edited to correct a small typo

Title: Re: NEW PROBLEM: 1-1SAT
Post by towr on Jan 8^th, 2003, 1:46am

on 01/07/03 at 16:15:10, william wu wrote:

If we ever see a literal x and its complement ~x in the same OR clause, we can throw out x and ~x.

You can throw out the whole OR-clause, since it evaluates to true.

Quote:

And if x and ~x are in different clauses, we can still reduce by noting that (x OR y) AND (x OR z) = (y OR z).

but (x OR y) AND (x OR z) == x OR (y AND z), isn't it? Besides x only occurs once..
and if you meant
(x OR y) AND (~x OR z)
it would still be (x AND z) OR (y AND ~x) OR (y AND z)

Title: Re: NEW PROBLEM: 1-1SAT
Post by william wu on Jan 8^th, 2003, 10:18am

on 01/08/03 at 01:46:01, towr wrote:

You can throw out the whole OR-clause, since it evaluates to true.

Ah that's right, thanks. So we remove a clause with every iteration.

Quote:

but (x OR y) AND (x OR z) == x OR (y AND z), isn't it? Besides x only occurs once..
and if you meant
(x OR y) AND (~x OR z)
it would still be (x AND z) OR (y AND ~x) OR (y AND z)

I meant the latter, (x OR y) AND (~x OR z). But I claim that's still (y OR z). We're trying to find a truth assignment that satisfies the formula, so you can assign x accordingly such that (x AND z) OR (y AND ~x) OR (y AND z) becomes (y OR z). Let 1 = true and 0 = false. Then:

If we assign YZ = 11, then assign X to be anything.
If we assign YZ = 10, then assign X to be 0.
If we assign YZ = 01, then assign X to be 1.

Using these mappings you end up with y OR z.

Title: Re: NEW PROBLEM: 1-1SAT
Post by towr on Jan 8^th, 2003, 12:25pm

I don't think it's a good idea to fill in the variables before you've simplified the whole formula..
I don't think you should fill in anything, since the question is only if there exists an assignment, and you don't need to give one.
So if you can show it's not a logical contradiction, it will have an assignment that satisfies it.

But maybe you're right and it will work.. I'll have to think about it..

Title: Re: NEW PROBLEM: 1-1SAT
Post by towr on Jan 8^th, 2003, 12:57pm

if it's a contradiction, the onyl case in which there isn't an assignment that satisfices it, then the opposite must evalute to true..
so, flip all AND's to OR's, all (original) OR's to AND flip x to not(x), and vice versa. simplify the now disjunctive normalform (so much easier). If it simplifies to true there isn't a satisfiying assignment, else there is..
(it's late, so I may be wrong, but I think I'm not..)

Title: Re: NEW PROBLEM: 1-1SAT
Post by william wu on Jan 8^th, 2003, 1:27pm

Well, I'm not really filling in anything yet. I don't know what Y and Z will become in the end, so I can't use those mappings for X. I listed the mappings just to argue that I can reduce the formula such that X disappears, because if there's a satisfying assignment for the original form, there will also be one for the reduced form, and vice versa.

Suppose we have a formula F that includes the expression (x AND z) OR (y AND ~x) OR (y AND z). Now I replace that part of the formula with (y OR z) to get F'. (Note that in F, the variable x and its complement each only appear once, and in F', they are both nowhere to be found.)

If there exists a satisfying assignment to F, then there also exists a satisfying assignment to F'. Let's look at F clause by clause. Clearly if (y AND z) is true, then F' is satisfied regardless of what x is. If (y AND ~x) is true, then y must be true and thus (y OR z) must also be true. Similarly, if (x AND z) is true, then x must be true and thus (y OR z) must also be true.

If there exists a satisfying assignment to F', then there also exists a satisfying assignment to F. Just choose x accordingly depending on whether YZ = 11 or 01 or 10.

As for actually finding the truth assignment, I think we could get it by looking backwards after all clauses are thrown out.

Yes, in the event of a contradiction, the inverse of our formula will evaluate to true, but I'm not sure I see the point ... is storing in a computer the tautology (x AND ~x) = FALSE harder than storing (x OR ~x) = TRUE ?

Title: Re: NEW PROBLEM: 1-1SAT
Post by towr on Jan 9^th, 2003, 12:37am

on 01/08/03 at 13:27:19, william wu wrote:

Yes, in the event of a contradiction, the inverse of our formula will evaluate to true, but I'm not sure I see the point ...

Having slept on it I'm inclined to agree there isn't much of a point.. Though I still prefer working with disjunctive normal form over conjunctive normal form..

Anyway, I think your algorithm should work nicely..