Related: CNF simplification (in fact, I think the submitter of that question might have been after what I want here)
A number of tools exist for simplifying (or "preprocessing" before solving) DIMACS format CNF formulas, and most SAT solvers incorporate some. However, all that I am aware of simplify a trivially satisfiable formula into a trivially satisfiable CNF with zero or one variables, i.e. they only attempt to preserve the satisfiability of the formula. I have tried at least SatELite and cryptominisat's preprocess mode.
However, for constructing CNF of a large problem, it seems to me that it would be quite useful to simplify a well-defined subset of the problem at a time, which may then be repeated a large number of times in the final CNF with additional constraints between some variables in these subformulas.
So, do any tools exist, or can ordinary SAT solvers (or other solvers like Z3, which I'm using to produce the CNF I would like to minimize) be somehow used with some cleverness, to simplify a CNF formula while preserving all solutions wrt a given set of variables?
The Coprocessor SAT preprocessor can do what you want. It can be given an optional variable scope and will only apply equivalence-preserving simplifications within that scope. Outside that scope, it will apply stronger, satisfiability-preserving simplifications. At least that was the case in version 2.