Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Heuristics and Exact Methods for Pairwise Interaction Sampling

Sándor P. Fekete, Phillip Keldenich, Dominik Krupke, Michael Perk

TL;DR

This work studies pairwise interaction sampling in large configurable software spaces, formulating the $t$-wise interaction sampling problem ($t$-Isp) on CNF formulas and focusing on $t=2$. It proves BH-hardness and places $t$-Isp in $\P^{\NP[\log]}$ with logarithmically many Sat calls, while also presenting practical methods that scale to hundreds of millions of feasible interactions. The core contributions include an efficient initial heuristic, a suite of lower-bound tools (including a cut & price approach), and Sammy, a parallel Large Neighborhood Search framework that combines a core SAT model with multiple incremental strategies to compute provably optimal samples for large benchmarks, outperforming prior methods on several large instances. Extensive experiments demonstrate significant improvements in both solution quality and runtime, including provable optimality on the four largest PSPL Scalability Challenge instances and notable gains over SampLNS on a broad benchmark, highlighting the practical impact for software testing in highly configurable systems. The work also provides a detailed preprocessing and implementation toolkit (universe reduction, universe pruning, and advanced LNS components) to enable scalable exact and near-exact solving of $2$-Isp in realistic settings.

Abstract

We consider a class of optimization problems that are fundamental to testing in modern configurable software systems, e.g., in automotive industries. In pairwise interaction sampling, we are given a (potentially very large) configuration space, in which each dimension corresponds to a possible Boolean feature of a software system; valid configurations are the satisfying assignments of a given propositional formula $\varphi$. The objective is to find a minimum-sized family of configurations, such that each pair of features is jointly tested at least once. Due to its relevance in Software Engineering, this problem has been studied extensively for over 20 years. In addition to new theoretical insights (we prove BH-hardness), we provide a broad spectrum of key contributions on the practical side that allow substantial progress for the practical performance. Remarkably, we are able to solve the largest instances we found in published benchmark sets (with about 500000000 feasible interactions) to provable optimality. Previous approaches were not even able to compute feasible solutions.

Efficient Heuristics and Exact Methods for Pairwise Interaction Sampling

TL;DR

This work studies pairwise interaction sampling in large configurable software spaces, formulating the -wise interaction sampling problem (-Isp) on CNF formulas and focusing on . It proves BH-hardness and places -Isp in with logarithmically many Sat calls, while also presenting practical methods that scale to hundreds of millions of feasible interactions. The core contributions include an efficient initial heuristic, a suite of lower-bound tools (including a cut & price approach), and Sammy, a parallel Large Neighborhood Search framework that combines a core SAT model with multiple incremental strategies to compute provably optimal samples for large benchmarks, outperforming prior methods on several large instances. Extensive experiments demonstrate significant improvements in both solution quality and runtime, including provable optimality on the four largest PSPL Scalability Challenge instances and notable gains over SampLNS on a broad benchmark, highlighting the practical impact for software testing in highly configurable systems. The work also provides a detailed preprocessing and implementation toolkit (universe reduction, universe pruning, and advanced LNS components) to enable scalable exact and near-exact solving of -Isp in realistic settings.

Abstract

We consider a class of optimization problems that are fundamental to testing in modern configurable software systems, e.g., in automotive industries. In pairwise interaction sampling, we are given a (potentially very large) configuration space, in which each dimension corresponds to a possible Boolean feature of a software system; valid configurations are the satisfying assignments of a given propositional formula . The objective is to find a minimum-sized family of configurations, such that each pair of features is jointly tested at least once. Due to its relevance in Software Engineering, this problem has been studied extensively for over 20 years. In addition to new theoretical insights (we prove BH-hardness), we provide a broad spectrum of key contributions on the practical side that allow substantial progress for the practical performance. Remarkably, we are able to solve the largest instances we found in published benchmark sets (with about 500000000 feasible interactions) to provable optimality. Previous approaches were not even able to compute feasible solutions.

Paper Structure

This paper contains 56 sections, 12 theorems, 4 equations, 6 figures, 1 table, 5 algorithms.

Table of Contents

  1. Introduction.
  2. Related Work.
  3. Preliminaries.
  4. Complexity.
  5. Avoiding Concrete Features.
  6. Hardness for Larger $t$.
  7. Initial Heuristic.
  8. Overview.
  9. Implementation Details.
  10. Preprocessing.
  11. Lower Bounds.
  12. Initial Lower Bounds.
  13. Cut & Price Bounds.
  14. Greedy Rounding.
  15. Constraints.
  16. ...and 41 more sections

Key Result

Theorem 4.1

Given a polynomial-time Sat oracle $\mathcal{A}{}$, for any constant $t$, $t\textsc{-Isp}$ with $|\mathcal{C}{}|$ concrete features can be solved in polynomial time using $\mathcal{O}(\log |\mathcal{C}{}|)$ queries to $\mathcal{A}{}$.

Figures (6)

  • Figure 1.1: An overview of the flow of our algorithm and the corresponding sections in the paper. The three rightmost boxes are executed in parallel, with multiple copies of the LNS using different strategies running simultaneously.
  • Figure 8.1: The fraction of each parameter remaining after simplification and universe reduction on the 55 instances from the benchmark set. The time to first solution bar only includes instances with non-negligible time (at least 0.5s) to find the first solution. The number of feasible interactions bars show the remaining feasible interactions after just simplification (S) or simplification and universe reduction (UR/S).
  • Figure 8.2: Performance plots showing the solution quality of all algorithms (relative to the best lower bound found by any algorithm), the runtime of the initial heuristics and the time taken by the LNS approaches to find solutions that they can prove to be within a certain gap to a minimum sample. Sammy (first) refers to the first sample found, and Sammy (initial) refers to the entire initial phase.
  • Figure E .1: Histogram showing the absolute gap values between the number of allowed configurations in the repair subproblem and the size of the mutually exclusive set used as symmetry breaker. A value of $-1$ means that the existing solution is optimal.
  • Figure E .2: The performance (repair subproblems solved over time) of the individual approach/solver combinations. The top row shows all subproblems, the bottom row shows only the subproblems that yielded improved solutions (left) and those for which the existing solution was already optimal (left).
  • ...and 1 more figures

Theorems & Definitions (21)

  • Theorem 4.1
  • Theorem 4.2
  • Definition 4.3
  • Theorem 4.4
  • Theorem 4.5
  • Theorem A .1
  • Proof 1
  • Theorem A .1
  • Proof 2
  • Theorem A .1
  • ...and 11 more