The encoding looks fine, but the algorithm isn't polynomial. Examine the following:
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.
Comments
The encoding looks fine, but the algorithm isn't polynomial. Examine the following:
@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.