# How can we reduce variables when converting from 3-SAT to 4-SAT?

If we suppose that we'd like to convert an instance of 3-SAT to an instance of 4-SAT, by how much can we reduce the amount of variables?

CONVERSION METHODS FOR PRODUCTS OF SUMS

If we are given a 3-SAT clause $(A \lor B \lor C)$, we can readily convert this to 4-SAT by rewriting it as $(A \lor B \lor C \lor x) \land (A \lor B \lor C \lor \overline{x})$, where $x$ is a free variable. In other words, $x$ can be any one of the existing variables, or a completely new variable. This entails that we can gaurantee that 3-SAT can be converted to 4-SAT without adding any new variables.

Additionally, we can convert 3-SAT into 4-SAT and eliminate one variable, given a special set of clauses. The 3-SAT clauses

$$(x \lor B \lor D) \land (\overline{A} \lor \overline{C} \lor x) \land (A \lor C \lor \overline{x}) \land (A \lor \overline{C} \lor x) \land (\overline{A} \lor C \lor x)$$

readily "reduce" to $(A \lor B \lor C \lor D)$. This eliminates the free variable $x$, assuming it only appears in these clauses, and also greatly reduces the number of clauses. The significance of this is that we may be able to eliminate some variables using this technique.

THE MAIN QUESTION

What are some other techniques for reducing the number of variables when converting from 3-SAT to 4-SAT?

Note that converting from product-of-sums to sum-of-products form may also be useful.

2. Distribution, in which all clauses containing a negated literal of $x$ are resolved against all clauses containing a positive literal of $x$. The produced resolvents are kept (minus any tautological clauses) and the original clauses containing $x$ are discarded. The resulting formula is satisfiable iff the original formula was satisfiable.