In search-based software engineering, one of the active research topics is the many-objective optimal software selection from software product lines. Previous works in this area mainly dealt with the preference from software engineers and end users in a posteriori way (namely selection after search). Different from that, this study integrates users' preference into the optimization process and proposes a new algorithm that can conduct a directed search for software products in which users are most interested. In the new algorithm, the users' preference is expressed as a weight vector, and an achievement scalarizing function (ASF) is used to aggregate all the optimization objectives. In addition, a new relation is defined to compare different individuals. To enhance the ability of the algorithm when searching for valid solutions, a substitution operator and a repair operator are implemented by using DPLL/CDCL-type and SLS-type SAT solvers, respectively. To verify the effectiveness of the new algorithm, 21 feature models widely used before are adopted to conduct simulation experiments. In these models, the largest number of features and that of constraints are 62 482 and 343 944, respectively. As shown by the experimental results, the substitution operator, which is based on a DPLL/CDCL-type SAT solver, is beneficial for returning valid software products, while the repair operator implemented by an SLS-type SAT solver contributes to find products that can satisfy the preference of users as much as possible. In summary, the simultaneous use of two types of SAT solvers is a feasible and effective way to handle the many-objective optimal software product selection problem where users' preference should be considered.