For this one in particular it is very easy to find the flaw
Let @Unsolvable = (2 ^ (2 ^ Variables.Count)) - 1
@Unsolvable has 2^Variables bits, so it can't be computed in polynomial time.
This is a typical fallacy by novices: assume that all arithmetic operations can be computed in constant time and constant space, regardless of the precision. Let @Unsolvable = (2 ^ (2 ^ Variables.Count)) - 1
...
If @Result = @Unsolvable
Return FALSE /*the formula cannot be satisfied*/
End if
@Unsolvable is exponential in the number of variables in the CNF. Thus there's an assumption here that the machine has a data-type capable of containing arbitrarily large integers.For example, if there are 10 variables, then @Unsolvable is 2^2^10-1. And so on. It doesn't matter whether his loops are polynomial, within the loops he's got something exponential in the number of variables.
@Result = @Result | @ClauseResult
But @Result is 0 by default.