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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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