pw_coverage/coverage_formulation.rst

.. _module-pw_coverage-formulation:

========================
Mathematical Formulation
========================

-------------------------------------------------
Combinatorial Test Coverage as Weighted Set Cover
-------------------------------------------------

This document details the mathematical formulation used to optimize the test configuration set. We reduce the Combinatorial Test Design (CTD) problem to a **Weighted Set Cover** problem, solved via Integer Linear Programming (ILP) using OR-Tools CP-SAT.

------------------
Problem Definition
------------------
We adhere to the Input-Output model defined by the **Coverage Request**:

- **Input**:

  - Parameters :math:`P = \{p_1, ..., p_n\}`, each with a finite domain of Options :math:`O(p_i)`.
  - **Exclusions (Hard Constraints)**: Rules defining invalid combinations (e.g., ``IF OS=Windows THEN Compiler!=GCC``).
  - **Coverage Goals** :math:`G`: Subsets of parameters requiring Cartesian product coverage (e.g., Pairwise :math:`(p_a, p_b)`).
  - **Point Constraints**: Specific partial configurations that *must* be included (e.g., ``Force {OS: Linux, Compiler: Clang}``).
  - **Existing Coverage**: A set of configurations already present (e.g., in CI) that should count towards goals but incur zero "new" cost.
  - **Option Costs** :math:`v(o)`: Resource cost associated with each option :math:`o \in O(p)` (default 1).

- **Output**:

  - A minimal-cost set of *additional* valid configurations :math:`S` such that all requirements are covered.

------------------------
Mathematical Formulation
------------------------
We formulate this as a **Weighted Set Cover** problem with **Preprocessing**.

Candidate Validity (Exclusions)
===============================
Unlike solvers that encode hard constraints as logical implications in the ILP (which bloats the constraint matrix), we enforce exclusions during **Candidate Generation**.
Let :math:`\text{isValid}(c)` be the boolean function evaluating all Exclusion rules.
The Candidate Pool :math:`C` is constructed such that:

.. math::
   \forall c \in C, \text{isValid}(c) = \text{True}

This ensures the optimization phase never wastes time considering invalid configurations.

Candidate Cost Derivation
=========================
Each parameter option :math:`o` has an associated atomic cost :math:`v(o) \ge 0`.
The total weight :math:`w_j` for a candidate configuration :math:`c_j` is the sum of the costs of its selected options:

.. math::
   w_j = \sum_{p \in P} v(c_j[p])

where :math:`c_j[p]` denotes the option selected for parameter :math:`p` in :math:`c_j`.
This linear aggregation allows the solver to naturally prefer "cheaper" configurations (e.g., using ``SimulatedTarget`` instead of ``HardwareTarget``).

Universe of Elements (Requirements)
===================================
Let :math:`U` be the universe of all required interactions. We index these requirements as :math:`r_i` where :math:`i \in \{1, \dots, M\}` and :math:`M = |U|`.

It is composed of two parts:

- **Combinatorial Goals**: For each goal :math:`g \in G` involving parameters :math:`P_g \subseteq P`, the requirements are the valid Cartesian products:

.. math::
   U_{goals} = \bigcup_{g \in G} \{ \text{valid combinations of } P_g \}

- **Point Constraints**: Each point constraint is treated as a unique mandatory requirement :math:`r_{pc}` that can only be satisfied by a configuration matching its criteria.

.. math::
   U_{points} = \{ r_{pc_1}, \dots \}

.. math::
   U_{total} = U_{goals} \cup U_{points}

Preprocessing (Existing Coverage Pruning)
=========================================
Before optimization, we prune requirements satisfied by **Existing Coverage** (:math:`E`). This is critical for incremental testing.

.. math::
   U_{active} = U_{total} \setminus \{ r \in U_{total} \mid \exists e \in E \text{ s.t. } e \text{ satisfies } r \}

Let :math:`M_{active} = |U_{active}|`.

- If :math:`M_{active} = 0`, the solution is trivial (empty set).
- The solver only sees :math:`U_{active}`, significantly reducing problem size.

Integer Linear Program (ILP)
============================
Let :math:`C = \{c_1, \dots, c_N\}` be the pool of valid candidate configurations, where :math:`N = |C|`.
We define a binary decision variable :math:`x_j` for each candidate:

.. math::
   x_j \in \{0, 1\} \quad \forall j \in \{1, \dots, N\}

**Objective Function:**
Minimize the total cost of selected configurations.

.. math::
   \text{Minimize } Z = \sum_{j=1}^{N} w_j x_j

**Subject to Constraints:**
Every active requirement must be covered.

.. math::
   \sum_{j : r_i \in U_j} x_j \ge 1 \quad \forall i \in \{1, \dots, M_{active}\}


**Note on Point Constraints**:
The interactions for Point Constraints are handled in two synchronized steps:
1.  **Generation**: We effectively "force" at least one candidate :math:`c_{pc}` into the pool :math:`C` that satisfies the point constraint.
2.  **Optimization**: We add a hard constraint to the ILP: :math:`\sum_{j : c_j \text{ satisfies } pc} x_j \ge 1`.

Since Step 1 guarantees the set :math:`\{j : c_j \text{ satisfies } pc\}` is non-empty, the logic in Step 2 is guaranteed to be feasible. The solver *must* select at least one of these forced candidates to satisfy the equation.

----------------
Scaling Analysis
----------------

Variables (Candidates)
======================
- **Small Domains**: Full Enumeration (:math:`N = \prod |O(p_i)|`). Global optimality.
- **Large Domains**: Goal-Driven Generation (:math:`N \approx 50 \times |U_{active}| + \text{RandomPadding}`).

  - Exclusions effectively *reduce* the effective domain, but might make random sampling harder (handled by constructive generation/retries).

Constraints (Requirements)
==========================
- **Pruning**: Existing Coverage drastically reduces the number of active constraints. If 90% of pairwise interactions are covered by baseline tests, the solver only optimizes the remaining 10% "edge cases".
- **Point Constraints**: Add exactly 1 constraint per request. They are "cheap" for the solver but expensive for generation (require specific targeting).

-------------------------
Justification of Approach
-------------------------
- **Handling Exclusions via Generation**: Keeps the ILP matrix "pure" (only set cover logic). Complex arbitrary exclusions (e.g., Python verification logic) can be used without translating them to CNF/SAT clauses.
- **Existing Coverage as Pruning**: Decouples "what we have" from "what we need". The solver doesn't need to know *which* existing test covers a requirement, only that it *is* covered.
- **Point Constraints as Requirements**: Unifies manual requests with combinatorial goals. The solver sees them identically ("I must cover X"), simplifying the architecture.