by Daniel-Jesús Munoz and Lidia Fuentes (Universidad de Málaga)

Industrial variability models routinely reach thousands of options, and counting their valid configurations governs almost every other analysis performed on them. Search-based counters cope well until they do not. We are designing a contraction engine that counts by algebra rather than by search.

A Software Product Line (SPL) is a family of systems built from shared assets, with their differences made explicit. A feature model organises those differences as a tree of features plus cross-tree constraints, and a configuration is valid when its selected features satisfy all of them. Determining whether such a configuration exists is known as the Boolean satisfiability (SAT) problem; #SAT, or model counting, goes a step further by asking how many valid configurations exist. In practice, that number lets engineers draw test configurations uniformly at random, measure how often each feature appears across the valid products, and spot options that no valid product can ever include.

Regarding who needs those counts, the stakeholders are concrete: automotive suppliers, operating-system distributors, and industrial control vendors whose certification obligations make the count auditable rather than interesting. While the question sounds arithmetic, it is #P-complete, the counting counterpart of NP-completeness, and the configuration spaces at hand are colossal.

Nevertheless, the usual motivation for physically inspired hardware is not the one the evidence supports. Boolean analysis of industrial feature models is empirically easy, and counters built on knowledge compilation count most industrial models quickly, although a few systems remain on which every counter tested so far times out. Substrates that sample return low-energy solutions without certificates, and annealing hardware pays twice, since its sparse qubit graph forces minor embedding, whose qubit overhead and chain breaks have so far kept densely constrained models well short of industrial size. Gate-based formulations are elegant, but are restricted to sizes no practitioner would call industrial: in [3], the authors report at most 16 features. Work tackling exact counting is rare.

Aiming to preserve the exactness counting demands, we plan to build on tensor networks, the formalism devised for weakly entangled quantum states and now used to simulate quantum circuits classically. Each clause becomes a small tensor, joining two legs means summing over a shared index, and contracting the whole network yields the number of models [1]. No bond dimension is truncated. The contraction is therefore exact as mathematics, whatever precision stores its intermediate tensors; the arithmetic required to represent such large values is a separate design consideration.

Concretely, exact tensor-network counting is not new [1]; what is missing is its adaptation to realistic variability models, which is what we are designing. The pipeline has four stages: (1) a reader from variability formats to a hypergraph, (2) a contraction-order search [L1], (3) contraction on the GPU [L2] with slicing bounded by video memory, and (4) an accumulation scheme sized to the result. Figure 1 walks those stages, which plug into flamapy [L3] as a backend.

Figure 1: The four-stage counting pipeline, from feature model to configuration count, and the memory wall that governs it. Intermediate tensor size grows exponentially with the treewidth of the primal graph, which makes that parameter the primary model-side determinant, while device memory and bandwidth, contraction order and slicing decide practical feasibility. Sizes are memory estimates for the intermediates, not the precision of the final count.
Figure 1: The four-stage counting pipeline, from feature model to configuration count, and the memory wall that governs it. Intermediate tensor size grows exponentially with the treewidth of the primal graph, which makes that parameter the primary model-side determinant, while device memory and bandwidth, contraction order and slicing decide practical feasibility. Sizes are memory estimates for the intermediates, not the precision of the final count.

While quantum devices remain noisy, with few qubits and short coherence, the same algebra already runs on a graphics card. By dispensing with annealing hardware, we also avoid the need to accommodate a specific device topology: the treewidth, the main structural determinant of intermediate tensor size, is a property of the model, while memory, bandwidth, contraction order and slicing decide what is feasible in practice. Amplitude estimation, a quantum counter with a quadratic guarantee, would be the successor once circuit depth allows.

As for evaluation, the target operation is exact configuration counting and the corpus comes from public variability repositories and from Kconfig models of the Linux kernel, which run beyond 14,000 options. The baselines are the established exact counters d4, GANAK, sharpSAT and ddnnife, and the dimensions measured are wall-clock seconds, peak memory in gigabytes, and joules per completed count, read from hardware counters, not estimated. Metaheuristics do not count exactly.

Then, the structure of real feature models has to be measured first, because contraction cost grows exponentially with the treewidth of the primal graph, the main structural bound on the intermediate tensors. Our hypothesis, no more than that, puts the useful regime below a treewidth of 30 and the hopeless one above 45; off-the-shelf heuristics allow us to bound it over real models in a weekend. On the other hand, to our knowledge no published study reports them, so a negative result would settle a question answered today by intuition.

We are aware that the approach rests on a structural property we have not yet measured, and that numeric features, whose translation to logic no published approach covers completely [2], inflate any encoding through bit-blasting. That inflation, however, may be structured. At least, sums and comparisons admit bit-blasted encodings of low width, whereas products between decision variables are typically far costlier, so which arithmetic fragment stays tractable is an encoding question we intend to measure.

Continuing past that measurement, the next step parameterises the engine by semiring, so one kernel serves counting, family-wide reliability estimates and minimum-cost queries. The formalism is quantum, the hardware classical. Delivered as an open artefact in the community’s standard exchange format, it would matter most to smaller European vendors shipping configurable software under certification duties without large compute budgets. Our central hypothesis is that feature models, built by people to stay comprehensible, carry the hierarchy and modularity that keep treewidth low, and that is the bet this line rests on.

Configuration counting underpins how configurable software, from the Linux kernel to automotive control units, is tested, analysed and certified, yet some industrial models still defeat every existing counter. We propose to take tensor networks, a formalism from quantum physics, and run them on classical GPUs, so that counting becomes an exact algebraic contraction rather than a search. The result would be a contraction engine that plugs into existing variability tools, together with a measurement of whether real feature models are structured enough for it to work.
This work is supported by the projects SAVIA PID2024-159945NB-I00 (co-financed by FEDER funds) and DUNE DGP_PIDI_2024_00092.

Links: 
[L1] https://github.com/jcmgray/cotengra  
[L2] https://developer.nvidia.com/cuquantum-sdk  
[L3] https://github.com/flamapy/flamapy  

References: 
[1] S. Kourtis et al., “Fast counting with tensor networks”, SciPost Physics, vol. 7, no. 5, art. 060, 2019. https://doi.org/10.21468/SciPostPhys.7.5.060 
[2] D. Fernandez-Amoros et al., “Pragmatic random sampling of Kconfig-based systems: A unified approach”, Journal of Systems and Software, vol. 230, art. 112577, 2025. https://doi.org/10.1016/j.jss.2025.112577 
[3] J. Ammermann et al., “Quantum Solution for Configuration Selection and Prioritization”, in Proceedings of the 5th ACM/IEEE International Workshop on Quantum Software Engineering (Q-SE 2024), ACM, New York, NY, USA, 2024, pp. 21–28. https://doi.org/10.1145/3643667.3648221 

Please contact: 
Daniel-Jesús Munoz 
ITIS Software, Universidad de Málaga, Spain 
This email address is being protected from spambots. You need JavaScript enabled to view it.