1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.