jørgen k. s.
jørgen k. s.

Reputation: 145

Does resolution variable elimination modify the solutions of other variables?

So I have a cnf, and two lists of variables K and C. The variables of K is added to the cnf as unit clauses (either negated or not depending on a boolean array) before sending it of to a sat-solver. When the sat-solver returns a model I only care about the variables that also occur in C and all other variables in the model is discarded.

Since the cnf is to be run repeatedly (with different variables from K set to true or false) it would be worth it to spend several hours to simplify the cnf and remove unnecessary variables (unnecessary is any variables that are not in either K or C) if it means shaving a few minutes off each time it is to be solved.

My question is whether I can use resolution variable elimination as described in this pdf or this bloggpost to eliminate some variables as long as I don't eliminate any variable that occurs in either K or C. Or if this will change the resulting model with respect to the variables in C?

Upvotes: 0

Views: 109

Answers (0)

Related Questions