In this paper we solve the SAT problem (the satisfiability problem of propositional formulas in conjunctive normal form) by a polynomially uniform family of P systems with active membranes in linear time in the number of propositional variables occurring in the input formula. In those polynomially uniform existing solutions which do not employ non-elementary membrane division or membrane creation the computation time depends also on the number of the clauses in the formula. In our solution we do not use non-elementary membrane division, but we use such membrane division rules where the labels of the involved membranes can change. We also use membrane creation rules, but compared to existing solutions with membrane creation rules our systems use asymptotically less objects and membranes during their computations.