在基于搜索的软件工程研究领域，高维多目标最优软件产品选择问题是当前的一个研究热点.既往工作主要采用后验方式（即先搜索再选择）处理软件工程师或终端用户的偏好.与此不同，将用户偏好集成于优化过程，提出了一种新算法以定向搜索用户最感兴趣的软件产品.在算法中，运用权向量表达用户偏好，采用成就标量化函数（achievement scalarizing function，简称ASF）集成各个优化目标，并定义一种新关系比较个体之间的优劣.为了增强算法快速搜索到有效解的能力，分别采用DPLL/CDCL类型和随机局部搜索（SLS）类型可满足性（SAT）求解器实现了替换算子和修复算子.为了验证新算法的有效性，采用21个广泛使用的特征模型进行仿真实验，其中最大特征数为62482，最大约束数为343 944.实验结果表明，基于DPLL/CDCL类型SAT求解器的替换算子有助于算法返回有效软件产品；基于SLS类型SAT求解器的修复算子有助于快速搜索到尽可能满足用户偏好的最终产品.在处理带偏好的高维多目标最优软件产品选择问题时，综合运用两类SAT求解器是一种行之有效的方法.

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.

TP311

国家自然科学基金（61906069，61773410，61502464）；广东省基础与应用基础研究基金（2019A1515011411，2019A1515011700）；中国博士后科学基金（2019M662912）；中央高校基本科研业务费专项资金（x2rjD2190840/2019MS088）