[inline-graphic not available: see fulltext]: A Tool to Transform Feature Models with Numerical Features and Arithmetic Constraints

Real-world [inline-graphic not available: see fulltext] need [inline-graphic not available: see fulltext] whose features not only have boolean values satisfying boolean constraints, but also have numeric attributes satisfying arithmetic constraints. A key operation on [inline-graphic not available: see fulltext]s finds near-optimal performing products, which requires counting the number of SPL products. Typical constraint satisfaction solvers perform poorly on counting. [inline-graphic not available: see fulltext] (Numbers, features, models) supports [inline-graphic not available: see fulltext] by [inline-graphic not available: see fulltext], the technique that encodes arithmetic as boolean clauses. [inline-graphic not available: see fulltext] translates [inline-graphic not available: see fulltext]s to propositional formulas whose products can be counted efficiently by #SAT solvers, enabling near-optimal products to be found. We evaluate [inline-graphic not available: see fulltext] with a diverse set of real-world [inline-graphic not available: see fulltext], complex arithmetic constraints, and counting experiments in this paper.