I looked at the Cook’s theorem at Wikipedia which presents a way to convert any NP problem to SAT but it seems to require O(f(x)^3) variables. Is it possible to remove some of the checks in the conversion so to make it O(f(x)*log(f(x))) in variables and time?