2026-05-30T22:53:44Zhttps://riuma.uma.es/rest/oai/request

oai:riuma.uma.es:10630/409912026-02-03T12:18:44Zcom_10630_2254col_10630_37959

00925njm 22002777a 4500 dc Muñoz-Guerra, Daniel Jesús author Oh, Jeho author Pinto-Alarcón, Mónica author Fuentes-Fernández, Lidia author Batory, Don author 2022-06-10 Real-world Software Product Lines (SPLs) need Numerical Feature Models (NFMs) whose features not only have boolean values satisfying boolean constraints, but also have numeric attributes satisfying arithmetic constraints. A key operation on NFMs finds near-optimal performing products, which requires counting the number of SPL products. Typical constraint satisfaction solvers perform poorly on counting. Nemo (Numbers, features, models) supports NFMs by bit-blasting, the technique that encodes arithmetic as boolean clauses. Nemo translates NFMs to propositional formulas whose products can be counted efficiently by #SAT solvers, enabling near-optimal products to be found. We evaluate Nemo with a diverse set of real-world NFMs, complex arithmetic constraints, and counting experiments in this paper. 978-3-031-08129-3 1611-3349 https://hdl.handle.net/10630/40991 10.1007/978-3-031-08129-3_4 Ingeniería del software Nemo: A Tool to Transform Feature Models with Numerical Features and Arithmetic Constraints.