We describe a new exact procedure, inspired on recent works on tableaux, for simultaneously solving MaxSAT and MinSAT. The main novelty of our procedure is that it implements a clause branching rule that preserves both the minimum and the maximum number of clauses than can be unsatisfied. Moreover, we prove the correctness of the procedure, and provide a review of the different types of branchings which are available for MaxSAT and MinSAT. We also give some preliminary experimental results that show that the new branching rule, when implemented into an existing branch-and-bound MaxSAT solver, produces substantial gains on industrial instances of the MaxSAT Evaluation.