3 CNF SAT Fail.

So, at 2:00 am last night I decided I had completed my 3-CNF-SAT algorithm (which runs in polynomial time!!). Well, here is the pseudocode:

ROUTINE(P):
-> Make a hashtable 'h' of size 3 * no. of clauses
-> For clause p in P:
	for each 'distinct' variable x in p:
		h[x] += 1

-> Find the variable with max frequency by going through hashtable 'h'.
-> Set this variable to True and remove those clauses from P in which this variable is present. Let this set be P'
-> Run this routine on P'

I knew it, this is right, this would work and would not fail. I was sure I had the answer.

BUT…

You really can’t answer yes or no using this technique:

For example, (x1 v x1 v x1 ) ^ (~x1 v ~x1 v ~x1) has no solution. But the above algorithm has no way of figuring that out. So, I fixed it by doing:

ROUTINE(P):
-> Make a hashtable 'h' of size 3 * no. of clauses
-> For clause p in P:
	for each 'distinct' variable x in p:  //when I say distinct variable, x1 and ~x1 are distinct
		h[x] += 1

-> Find the variable with max freuqency by going through hashtable 'h'.
-> Set this variable to True (and the negation of this var to false) and remove those clauses from P in which this variable is present. Let this set be P'
-> Check all removed clauses to see if all these clauses return True. If not, there isn't a solution
-> Run this routine on P'

Now, I have no idea how to prove that this doesn’t work (it doesn’t and I know it).

Oh well whatever. Some day, I will find out why this is wrong.