SAT-Problems and Reductions with Respect to the Number of Variables
ETIENNE GRANDJEAN, Hans Kleine Büning · Journal of Logic and Computation · 1997
We consider polynomial time bounded reductions, in particular between k – SAT, SAT and SAT*, in order to obtain the minimal number of variables. As an example we prove that SAT and Unique SAT have, for deterministic algorithms, the same upper bound of the form O( Π c n) for some c > 1, where n is the number of variables of Π. We show that k – Unique SAT is not harder than k – SAT, but not easier than k(r) – SAT (formulas in k – CNF with at most r positive or negative clauses). Finally we present a proof that for each problem in NTlME(n) there is a polynomial reduction to SAT such that the number of variables in f(Π) is only O(n) improving Schnorr–Cook's reduction with O(n log n) variables.