This paper presents a system based on new operators for handling sets of propositional clauses represented by mean s of ZBDDs. The high compression power of such data struc- tures allows efficient encodings of structured instances. A specialized operator for the distribution of sets of clause s is introduced and used for performing multi-resolution on clause sets. Cut eliminations between sets of clauses of ex- ponential size may then be performed using polynomial size data structures. TheZRES system, a new implementation of the Davis-Putnam procedure of 1960, solves two hard prob- lems for resolution, that are currently out of the scope of th e best SAT provers.