# When using resolution variable elimination to simplify a cnf, does that change the truth values of the other variables?

When you use resolution variable elimination to preprocess/simplify a formula in cnf form the resulting formula is equisatisfiable.

What I wonder about is if I can use this technique to remove variables i don't care about while leaving the truth values of the variables I care about untouched in the final model I get from the sat solver.

## 1 Answer

Yes, you can. Any satisfying assignment for the simplified formula can be extended to a satisfying assignment for the original formula, by setting appropriate values to the eliminated variables (but not changing the values of the remaining variables), and vice versa.