Say that I'm required to build a CNF formula with k "variables" (literals), is it legal to set, for example, k/2 of the variables to be zeros (or ones)?
If you set some of the variables to constants (T/F) you get a different formula with a different semantics.
Also, any constants (T/F) can always be eliminated, leaving a shorter formula. Thus our formulas
have only literals and no constants.