Exhaustive Enumeration of Selection Observations in Pure Dataflow Graphs: A Survey and Unified Framework

1. Introduction

Consider a finite, typed, acyclic, deterministic pure dataflow graph containing nested conditionals, multiplexers, priority selectors, or other finite choice operators. Its primitives are total on their typed domains. A caller supplies an input from a declared domain and requests one or more graph results. The problem of this survey is:

A selection observation records the contextual outcome of each selection site reached from the requested roots through declared operand dependencies and selected case edges. It is sparse because a site in an unselected case cone is absent, not merely assigned an unconstrained value. Its inverse image in the caller domain is an observation fiber. An exact enumerator returns one record

per nonempty fiber. The guard denotes precisely that fiber; the residual computes the requested values throughout it; and the witness demonstrates feasibility.

The paper introduces selection observation, selective term graph, enabled closure, observed-outcome guard, observation record, and full-fiber blocking as local names or local refinements for this synthesis; they are not claimed as established terms of art, and the complete four-field contract is not presented as an already established named task. The paper is therefore also a theory/position synthesis of a proposed semantic contract, not evidence that this exact observer already has a demonstrated consumer. Observer, kernel, fiber, guard, residual, projection, and symbolic execution retain their established meanings. The six groups below are overlapping solution routes, not a field-wide taxonomy.

This task is easy to misidentify. A monolithic symbolic value describes output semantics but does not enumerate structural observations. A path records a control-flow history rather than the enabled portion of an arbitrary shared graph. A projected model fixes selected logical coordinates but needs explicit reachability instrumentation to represent structural absence. A partial cube may cover several complete observations. A geometric region can give an exact guard and affine residual while quotienting equal behavior or assuming that every site is observed. These objects can look alike while answering different questions.

The survey therefore separates three choices that are often conflated:

• the observer, which determines when two inputs belong to the same record;
• the enumeration mechanism, which discovers all nonempty fibers; and
• the representation, which stores guards, residuals, witnesses, and shared structure.

This separation makes six overlapping routes comparable: guarded symbolic execution, projected enumeration, compiled decision structures, demand-guided search, geometric or parametric specialization, and compositional summaries. Each route has strong precedents, but its name alone does not determine the observer or supply the complete record contract. Section 5 introduces the representative literature only where each route is analyzed.

The paper answers four questions:

• RQ1: What consistent terminology precisely defines selection-observation enumeration and distinguishes it from neighboring tasks?
• RQ2: Which established approach traditions or routes can enumerate, compile, or specialize the required fibers, and what instrumentation do they require?
• RQ3: Which correctness, representation, and complexity guarantees does each route provide under its stated assumptions?
• RQ4: Where do the approaches coincide, where do they compute a refinement or quotient of the target observer, and where do they address only an adjacent reduction problem?

The contribution is consequently a problem-centered survey and unified framework:

• A finite selective-term-graph model defines requested-root enabled closure, contextual site identity, sparse observations, exact fibers, and the output record contract.
• An observer-refinement order distinguishes structural non-observation, existential projection, logical don’t-care, and equal-behavior quotienting without treating them as interchangeable forms of sparsity.
• Six recurring research traditions and implementation routes are compared under one set of semantic, algorithmic, representational, and complexity dimensions. They overlap rather than forming a flat taxonomy.
• Formal correspondences show that observed-outcome guards and global reachability-and-outcome projection describe the same partition, while guarded summaries agree with flattened graph substitution under explicit sharing and interface conditions.

The framework is a synthesis, not a priority claim for its ingredients. Its purpose is to state one problem precisely enough that results from different communities can be transferred only when their observers and assumptions actually agree.

Section 2 develops the problem through one graph. Section 3 then defines its core semantics independently of any solver, and Section 4 states the survey’s evidence boundary. Section 5 presents the six solution routes, Section 6 gives two general enumeration presentations, and Section 7 states the compositional extension. Section 8 separates general costs from stronger specialized frontiers; Section 9 then compares observers, guarantees, and closest established results. Section 10 states the remaining boundaries and open problems, and Section 11 closes with the main conclusions.

2. Selection observations by example

Let p and r be Boolean inputs and x and y be integer inputs. Consider the shared, pure graph

q_inner = select(r, x + 1, x + 1)
q_outer = select(p, q_inner, y)
return q_outer

Here the first case is selected when the Boolean selector is true, so we label the outcomes left (true) and right (false). Both arms of q_inner are intentionally equal. We request only q_outer.

A monolithic value encoding is immediate:

It simplifies extensionally to $ite\left(𝑝,𝑥+1,𝑦\right)$. Neither expression states the structural partition we intend to enumerate. Write ${𝑞}_{𝑜}$ and ${𝑞}_{𝑖}$ for the outer and inner sites. Table 1 lists the three observations.

The example separates four notions.

First, q_inner is structurally unobserved when $\neg 𝑝$. Assigning it a wildcard in a Boolean implicant would be weaker: a wildcard may also cover executions in which the site is observed but its outcome is irrelevant to some other formula. The totalized observation uses a dedicated unobserved sentinel; the sparse API omits the coordinate.

Second, the two $𝑝$-true records have equal residual expressions. They remain different because the observer records which outcome of q_inner was reached. A quotient by output value, residual function, or maximal affine behavior would merge them. That quotient is legitimate for a different objective but is not this observer.

This distinction has a concrete specification role even without assigning operational significance to evaluation order. As a stated hypothetical — no worked instance is developed in this survey — an event-aware validation task may ask whether every source selection outcome remains represented after graph rewriting, lowering, or component substitution (a task that itself requires a declared event correspondence, since such transformations can change the observer; see Section 10). The two inner outcomes then belong to different records despite equal values. A value-only equivalence checker deliberately chooses a coarser observer and merges them. The framework does not declare one policy universally preferable; it makes the policy an explicit part of the problem statement.

Third, the observed-outcome guards contain predicates only for sites actually observed in the corresponding record. The first guard does not say anything about r. Its exactness is structural: once q_outer chooses y, graph reachability cannot enter the cone containing q_inner. The later exact observed-outcome guard theorem generalizes this lockstep argument to arbitrary finite shared graphs and multi-case selections.

Fourth, one model per record is not the desired residual. For example, p = true, r = false, and x = 0 witnesses the second record, but the residual valid on the whole fiber is $𝑥+1$, not the sampled value $1$. Exact enumeration must combine model discovery with symbolic specialization.

This nested example is intentionally different from a dense ReLU network or a flat collection of strict sign tests. When the caller domain excludes all test boundaries, each observation is a total activation vector and established full-dimensional cell algorithms already enumerate the corresponding guards and affine maps. The unselected nested site is the minimal feature that exposes the graph-relative observation policy.

2.1. Framework at a glance

The concrete observer is easy to compute. Start at the requested root set. At an ordinary operation, walk to every operand. At a selection, always walk to its selector and only to the case roots enabled by that outcome. Record each selection occurrence reached by this backward walk and its outcome. Two inputs belong to the same observation fiber exactly when these records match.

The formal section gives names to the pieces: $𝐺$ is the graph, $𝑅$ the requested root set, $𝐴$ the caller-domain predicate, ${𝐷}_{𝐺\left(𝑥,𝑅\right)}$ the nodes reached by the walk, and ${𝑇}_{𝐺\left(𝑥,𝑅\right)}$ its selection record. For one feasible record $𝜏$, its fiber ${𝐹}_{𝜏}$ is the input group with record $𝜏$, while ${\mathrm{\Gamma }}_{𝜏}$ is an exact formula for that group. The rest of the paper asks how existing methods discover these groups and represent their formulas, residual output expressions, and sample inputs.

An implementation-oriented reading path is this example, the opening and comparison table of Section 5, the two constructions in Section 6, and Section 11. The intervening definitions and proofs make the contracts and transfer conditions precise.

3. Selection observations: formal model and semantics

This section defines the problem independently of any solver or data structure. The framework separates an observer, its inverse-image fibers, an enumeration mechanism, and an output representation. Its graph model is intentionally narrower than a general programming language: it isolates the finite, acyclic, deterministic, total pure-graph case for which exhaustive observation enumeration is a well-defined finite-output task.

3.1. Notation map

Table 2 collects the symbols used throughout the core definitions. A subscript $𝐺$ names the graph whose structure is being consulted; a fixed caller predicate $𝐴$ and requested-root set $𝑅$ determine the enumeration instance.

3.2. Selective term graphs

An input valuation belongs to the typed product ${\mathrm{𝒳︀}}_{𝐺}={\prod }_{𝑖\in 𝐼}{\mathrm{𝒟︀}}_{𝑖}$. An ordinary node $𝑣\in 𝑁$ with operands ${𝑢}_1,\dots ,{𝑢}_{𝑘}$ denotes a deterministic total function

Ordinary nodes follow an all-operands observation policy: observing their result observes every operand. This is a declared structural dependency policy, not an operational evaluation order and not an assertion that ${𝑓}_{𝑣}$ depends extensionally on every argument.

For readers used to runtime dataflow diagrams, the edge direction here may look backward: an edge points from a consumer to one of its operands. This lets reachability start at the requested results and walk directly toward everything they declare as a dependency.

The outcome is semantic, not necessarily the raw selector value. It must carry enough information to determine both the demanded case set and the applicable combiner. An indexed selection may have one outcome per case and one default; a priority selection may identify the first enabled case; and a mask-valued selection may use the complete enabled-case mask as one outcome and demand several roots. If an interface intends to distinguish two raw values, they must be distinct outcomes even when they choose the same cases.

Because the graph is acyclic and every primitive is total, each input $𝑥$ induces a unique total graph value ${val}_{𝑥\left(𝑣\right)}$ at every node. At a selection site, ${𝜔}_{𝑥\left(𝑞\right)}={𝜅}_{𝑞\left({val}_{𝑥\left({𝑠}_{𝑞}\right)}\right)}$, and the value is obtained by applying ${ℎ}_{𝑞,{𝜔}_{𝑥\left(𝑞\right)}}$ to the selected case-root values. Values in unselected case cones remain mathematically defined; the observation judgment below determines which of them are structurally exposed.

3.3. Contextual identity and caller domain

A site inside one graph is identified by its node. Graph substitution prefixes internal sites by the component occurrence, so two calls to the same callee have different identities. Statically bounded iteration also includes the iteration index. This policy preserves sharing within an occurrence while excluding unbounded recursion and loops, which could create an infinite event domain.

The observation is relative to a requested root set $𝑅\subseteq 𝑂$ and a caller-domain predicate $𝐴:{\mathrm{𝒳︀}}_{𝐺}\to 𝔹$. All feasibility and completeness claims range over ${\mathrm{𝒳︀}}_{𝐴}=\left\{𝑥\in {\mathrm{𝒳︀}}_{𝐺}|𝐴\left(𝑥\right)\right\}$. An open multi-output component therefore takes $𝑅$ as an interface parameter; observing all outputs unconditionally would expose sites that a caller does not request.

3.4. Enabled closure and selection observation

The word observed is local terminology for this membership judgment. It does not claim that the source evaluator is lazy. Classical neededness and demand semantics use related backward relevance but impose different semantic conditions; Section 5 compares them.

For a fixed graph, the partial-map and totalized-vector presentations are isomorphic. The first is the intended sparse record; the second permits direct projection onto the finite product ${\prod }_{𝑞\in 𝑄}\left({\mathrm{\Omega }}_{𝑞}\cup \left\{{unobs}_{𝑞}\right\}\right)$.

3.5. Observers, refinements, and representations

In plain language, an observer is the function used to sort inputs into buckets. A fiber is one bucket. Refinement means that knowing the finer bucket is enough to recover the coarser one. A residual is a formula or shared expression that computes the requested result for every input in one bucket.

For fixed $𝐺$ and $𝑅$, ${𝑇}_{𝐺\left(-,𝑅\right)}$ is the selection observer. Its sparse and totalized presentations have the same kernel and are therefore two representations of one observer. By contrast, projecting away site coordinates or coalescing records with equal residual functions generally produces a coarser observer. A control-flow path or execution trace may be finer, and it may also preserve distinctions incomparable with requested-root selection events.

This vocabulary separates semantic objects from encodings. A flat list of guards, a decision tree, a decision diagram, and a projected-model stream may represent the same observer image. A partial cube can instead represent a set of image elements. Calling all of these outputs “partial decisions” obscures whether the underlying partition has changed.

3.6. Least valuation under the declared dependency policy

Extend each value domain with a fresh undefined value ${\perp }_{𝑣}$ and order it flatly, ${\perp }_{𝑣}\le 𝑑$ for every ordinary value $𝑑$, with distinct ordinary values incomparable. Order valuations pointwise. An $𝑥$-consistent partial valuation assigns each node either ${\perp }_{𝑣}$ or its total graph value. It is dependency-closed when a defined ordinary node has all operands defined and a defined selection has its selector and every case root required by its concrete outcome defined. This is an obligation, not a prohibition: another requested root or shared consumer may independently require an unselected case root. The valuation is $𝑅$-complete when every requested root is defined.

This proposition is a graph-reachability result for the stated all-operands policy at ordinary nodes. Equality with a language’s semantic least demand requires a separate translation showing that each source operator has precisely these predecessor obligations.

3.7. Fibers and exact observed-outcome guards

Fix $𝐺$, $𝐴$, and $𝑅$. The feasible observation image and the fiber of one $𝜏$ in that image are

Because ${𝑇}_{𝐺\left(-,𝑅\right)}$ is a total function on ${\mathrm{𝒳︀}}_{𝐴}$, its nonempty fibers are pairwise disjoint and cover the caller domain. This elementary inverse-image partition is the semantic enumeration contract.

These are semantic functions. A concrete implementation may encode a guard as an SMT formula and a residual as a term DAG, provided evaluation has the stated meaning; the contract does not require tabulating either function.

For each site outcome, define

For feasible $𝜏$, its observed-outcome guard is

It mentions outcomes of observed sites but contains no outcome or absence atom for an unobserved site. The name is semantic rather than syntactic: an outcome predicate may contain negation or an inequality, and expanding it may traverse nested selection expressions. The demanded generator in Section 6 avoids constructing unobserved case cones.

The result relies on each outcome determining its case-demand set. It proves exactness, not literal minimality: an observed-site predicate may still be entailed by $𝐴$ and the remaining predicates.

Thus two observed-outcome guards are disjoint because they contain incompatible outcome predicates at a shared observed site. This structural separator is stronger than the generic fact that distinct function fibers are disjoint and is the key reason full-fiber blocking does not need explicit unobserved-site literals.

4. Survey scope and evidence basis

This is a problem-centered scoping survey supported by a reproducible systematic search record and evidence map; it is neither a closed systematic map nor a statistical systematic literature review. Discovery and reporting draw on systematic-mapping guidance (Petersen et al., 2015), separate backward and forward snowballing (Wohlin, 2014), and auditable reporting of secondary studies (Kitchenham et al., 2023); no completed reporting checklist is claimed. It supports the comparison of solution mechanisms for the problem in Section 3, not a census of every use of symbolic execution, dataflow, or enumeration.

4.1. Comparison and inclusion

The four research questions in the introduction determine the extraction schema. For each work, the map compares its model and observer, enumerated object, discovery algorithm, output representation, guarantees, complexity charge, and semantic or solver assumptions.

Works in the main comparison have one of four relationships to the target problem. A direct presentation enumerates the same observer after explicit notation or reachability instrumentation. A restricted specialization solves the same contract under stronger assumptions, such as all sites being observed and all classifiers being affine. An adjacent comparator preserves or omits information for a different observer and is included only when it clarifies a semantic or complexity boundary. An open correspondence is close enough that a reduction may exist, but this survey has not proved observer and record equality. The classification prevents a neighboring reduction problem from being presented as an alternative implementation of an input-fiber enumerator.

4.2. Discovery, screening, and technical evidence

Discovery deliberately used a broader vocabulary than the final paper. It covered symbolic execution and guarded values; projected and partial model enumeration; decision structures; functional-logic and demand-guided search; dataflow and hardware semantics; geometric, neural, and parametric regions; and observer-relative state or search reduction. Exact queries, result depths, dates, and citation chases are retained in the audited log. Transient result sets are discarded after reconciliation, so the log row is the audit unit; primary bibliographies supplement incomplete citation indexes.

Through 9 August 2026, 340 database queries and 245 backward or forward citation chases yielded 36,828 retrieved and title-triaged record occurrences. Repeated hits and rows rejected before cataloging remain in that occurrence count; it is neither a unique-paper count nor an estimate of a literature population. After deduplication and audit, the current catalog contains 924 works: 120 deep-read, 247 screened, 422 retained candidate, and 135 excluded records. Candidate status is an unresolved abstract-screening backlog rather than evidence inclusion or a promise to deep-read the work. The manuscript cites 79 deep-read technical sources and seven screened works; no candidate-status work supports a manuscript claim.

Technical claims rely on primary works with pinpoint definition, algorithm, theorem, complexity, assumption, or example anchors. Abstract- or metadata-level records support only search scope or qualified chronology. The evidence ledger binds manuscript claims to those source anchors and carries their scope and caveats.

4.3. Bounded search snapshot and on-demand updates

The initial campaign was previously described as having bounded mapping closure. Publication review withdrew that claim: although every row had a catalog status, 422 rows were still candidate, which is not an adjudicated inclusion/exclusion disposition under the clarified protocol. The present artifact is therefore a bounded search snapshot relative to the recorded sources, rankings, query depths, and date. Its reviewed evidence supports the comparisons made here, but the unresolved backlog prevents an inference that all plausible close work in the captured set has been assessed.

Updates run on demand when a new mechanism or plausible direct competitor appears and to reduce the candidate backlog. The registered searches were last run through 9 August 2026, when 22 registered queries were rerun at caps of the top 100 relevance- or recency-ranked results. No candidate-status work supports a claim, and no absence claim is drawn from the unresolved rows. The protocol, queries, catalog, log, source notes, syntheses, and evidence and claim ledgers are linked from the survey’s landing page.

4.4. Validity threats and AI assistance

The breadth-first discovery campaign may miss work whose terminology does not intersect the registered queries or citation neighborhoods. Database rankings are opaque, metadata services omit or merge records, and exact counts describe captured occurrences rather than a population. The framework itself can bias classification: a theorem proved for a different observer must not be silently transferred after adding instrumentation or changing the output quotient.

Search, extraction, and duplicate-screening used repeated AI-assisted passes under the same project framing. They are repeated checks, not independent human reviews; no inter-rater agreement statistic was computed. The title-page note gives the full authorship, assistance, evidence-use, and public-record disclosure.

5. Solution routes

The target is one exact selection-observation record per nonempty caller-input fiber. Prior approaches become comparable only after fixing that contract. Some can enumerate the fibers directly after instrumentation, some compile the same finite observer into a shared representation, and some solve restricted special cases with stronger guarantees. Table 3 summarizes six recurring, non-exclusive research traditions and implementation routes. They mix mechanisms, representations, and restrictions rather than forming a flat taxonomy.

5.1. Guarded symbolic execution

Classical symbolic execution associates path conditions with symbolic states or substitutions (King, 1976), while DART established the later concrete-plus-symbolic, solver-directed test-generation lineage (Godefroid et al., 2005). Denotational treatments make this correspondence exact under their stated language and merge conditions (Voogd et al., 2025), while multi-path execution merges paths into guarded symbolic values (Sen et al., 2015). Variational execution similarly carries conditional values under configuration contexts and shares computation across many configurations, but its native result is a shared multi-configuration execution rather than one exact inverse-fiber record (Wong et al., 2018). Solver-aided libraries and reusable merging semantics preserve the same basic separation between guards and residual values (Lu & Bodík, 2023; Porncharoenwase et al., 2022).

These systems supply two parts of the target record almost directly: a feasibility guard and a residual. They do not by themselves choose the selection observer. Conventional paths may distinguish branches outside the requested enabled closure, merge histories that retain different requested events, or split one observation because of unrelated control flow. To solve the target problem, evaluation must be demanded from the requested roots, record contextual selection outcomes, preserve graph sharing, and block the entire resulting fiber rather than one execution model.

The closest published algorithms make this gap narrow. PESO enumerates reordered relevant-slice conditions for requested output criteria, carries symbolic outputs and solver-generated tests, and proves conditional exploration completeness under a sound and complete solver (Qi et al., 2013). SPD constructs a shared graph of dependence-relevant path families and guarded symbolic values for queried uses (Santelices & Harrold, 2010). All-values and dependence-guided execution provide further output/value-directed precedents (Denaro, 2012; Wang et al., 2017). What remains open is not whether output-directed guarded exploration exists, but whether PESO’s RSC quotient or SPD’s path-family graph, after site instrumentation, gives exactly one target selection fiber rather than a refinement or fragmented cover.

SEDGE is the closest explicitly dataflow-named concolic testing comparator: it uses SMT to synthesize high-level Pig inputs intended to exercise operator cases. Its coverage target and accumulated example dataset are not a duplicate-free exact partition with residuals (Li et al., 2013).

The local generator formalized in Section 6 is therefore not a new symbolic execution paradigm. It is the target observer instantiated in a standard guard-and-residual evaluator. Its useful property is the exact observed-outcome guard: structurally unobserved sites require no absence literal because enabled reachability is already fixed by the observed outcomes.

5.2. Projected model enumeration

Phan’s AllSMT enumerates satisfying assignments to designated important Boolean coordinates while returning sampled values for relevant theory variables (Phan & Malacaria, 2015). A finite theory-valued coordinate needs an engine whose projection contract explicitly enumerates its values. Recent projected SAT and SMT methods can emit disjoint partial models and avoid a growing family of ordinary blocking clauses (Spallitta et al., 2024; 2025). Knowledge compilation similarly supports disjoint partial-model enumeration after d-DNNF compilation (Lagniez & Lonca, 2024).

This is the most direct generic reduction. Give every contextual selection site a finite coordinate whose values are its outcomes plus an explicit unobserved sentinel. Reachability equations connect that sentinel to requested-root reachability. Projecting the graph formula onto those coordinates then enumerates exactly the totalized selection observer. The construction is conceptually complete but charges the whole-graph value, classifier, case-membership, and reachability encodings.

The output contract still matters. Enumerating every complete projected tuple produces one element per selection observation. A short partial cube can cover many tuples and is therefore a compact cover of the observer image rather than the requested record stream. Disjoint short-model methods make such covers precise, but a consumer that requires one residual and witness per complete observation must refine or annotate the cubes accordingly.

5.3. Compiled decision structures

A decision tree asks only its representation tests along a root-to-leaf route. This is not the same as a graph selection site being unobserved: a compiler may choose entirely different input predicates. Reduced BDDs share Boolean subfunctions canonically under a fixed variable order (Bryant, 1986), and ADDs extend terminals beyond Boolean values (Bahar et al., 1997). Finite observer partitions can also be generated directly as exact input-equivalence classes or satisfiable atoms of a declared observation alphabet (Huang et al., 2024; Krafczyk & Peleska, 2017).

For finite encoded inputs, compiling the function $𝑥\mapsto {𝑇}_{𝐺\left(𝑥,𝑅\right)}^{\text{tot}}$ yields an exact representation of the target partition. Leaves or terminals may additionally carry residual identifiers and witnesses. A tree exposes the sparse sequence of tests made along one route; a diagram exposes shared predicates and subfunctions across many routes. Either can be exponentially smaller or larger than a flat guard list, so a comparison must state whether the output is a stream of records or one shared compiled object.

Compilation also exposes a semantic choice. Reducing nodes that have equal successors preserves the compiled observer, but compiling only the requested output value may erase equal-valued selection events. Neural decision-tree extraction and affine decision structures make this contrast concrete. Nguyen et al. construct EC-DTs and report exact empirical fidelity with contradiction pruning (Nguyen et al., 2020); Affinitree proves semantic preservation and simplifies infeasible or entailed tests (Schlüter & Steffen, 2024). They solve the selection-observation task only when their terminals or internal labels retain the declared selection events.

5.4. Demand-guided evaluation and search

Functional-logic set functions and pull-tabbing establish the representation lineage most directly: set functions record the nondeterministic steps actually executed, the 2010 pull-tab transformation propagates immutable choice identifiers so runtime copies make consistent decisions, and memoized pull-tabbing finally exposes an explicit task-local partial choice map (Alqaddoumi et al., 2010; Antoy & Hanus, 2009; Hanus & Teegen, 2021). Other pull-tabbing, translations, and memoization use demand-populated decision maps or prove value-set preservation under their own search assumptions (Antoy, 2011; Braßel, 2011; Braßel & Huch, 2007; Hanus & Teegen, 2021; Jost, 2023). Lazy SmallCheck refines just the partial input demanded by a Boolean observation and remains exhaustive over its bounded domain (Runciman et al., 2008). SPLat similarly discovers configuration variables on first read, uses SAT to prune feature-model-infeasible partial assignments, and executes concrete witnesses for distinct claimed test traces (Kim et al., 2013). Classical dataflow analyses compute least or reverse demand for a fixed requested result (Avron & Sasson, 1994; Pingali & Arvind, 1985), and modern bidirectional demand semantics can characterize minimal sufficient partial inputs (Xia et al., 2024).

These results establish that stable sparse choice maps, dynamically discovered configuration decisions, and requested-result demand are not new. Their natural output, however, is commonly a value stream, a partial input, a choice fingerprint, a concrete test trace, or a fixed-input demand set. The target enumerator additionally requires the complete inverse-image guard and a residual valid over that entire guard. A demand system becomes a direct solution only after its demand judgment is proved equal to the enabled closure and its fair search is grouped by complete observation fibers.

The comparison also prevents a terminology error. The base graph is not called lazy: ordinary nodes expose all operands under a declared observation policy, while selection sites demand only the cases chosen by their outcomes. “Demand” here is graph-relative support for a requested observer, not an operational evaluation strategy.

5.5. Geometric and parametric specializations

When every selection is observed, each classifier is the strict sign of a distinct nonconstant affine form, and the caller domain is the ambient space with all classifier boundaries removed, a complete observation is a sign vector and each nonempty fiber is a full-dimensional hyperplane-arrangement cell. Reverse-search and incremental algorithms enumerate those cells exactly with output-sensitive guarantees (Avis & Fukuda, 1996; Ferrez et al., 2005; Rada & Černý, 2018). Exact ReLU analyses likewise enumerate activation patterns or polyhedral regions and often attach affine output maps (Serra et al., 2018; Vincent & Schwager, 2021); star-set reachability and explicit piecewise-affine conversion emit exact guards with affine images, and cell-complex, edge-subdivision, and parallel layerwise variants recover richer exact structure (Berzins, 2023; Drammis et al., 2024; Masden, 2025; Robinson et al., 2020; Tran et al., 2019).

Multiparametric programming provides a closely related guard-and-residual contract. Critical-region algorithms emit polyhedral parameter guards together with affine optimizers and have explicit LP-oracle-relative bounds, building on the positive-semidefinite pLCP precursor (Columbano et al., 2009; Jones & Maciejowski, 2006; Jones & Morari, 2006). Piecewise-affine systems compose upstream affine maps into downstream guards and can minimize regions with equal behavior relative to a supplied arrangement and representation class (Geyer et al., 2008; 2010).

The full-dimensional hyperplane and dense activation-pattern methods are direct specializations under the stated observer and domain restrictions. Assigning boundary points to a side produces closed or lower-dimensional strata and requires separate face or ownership machinery; the cited open-cell guarantees do not transfer automatically. Parametric critical regions instead observe an optimizer basis or active set. They are direct only after an explicit model shows that this identity is exactly the graph’s selection observer; otherwise they are strong guard-and-residual comparators. The full-dimensional cell algorithms analyzed here no longer instantiate the target when nested selections make sites unobserved, the caller predicate cuts across cells, or equal affine maps are merged despite different observed outcomes.

5.6. Compositional guarded summaries

Compositional symbolic execution summarizes component behavior with guarded relations, preconditions, postconditions, or path fragments (Anand et al., 2008; Godefroid, 2007; Voogd et al., 2025). Guarded piecewise-affine composition substitutes an upstream residual into downstream guards and residuals while discarding infeasible conjunctions (Geyer et al., 2010). Selective computations supply an abstract interface for statically visible, dynamically chosen effects (Mokhov et al., 2019).

The unified framework adds two parameters needed by the target observer: requested output roots determine boundary demand, and contextual prefixes distinguish multiple component occurrences while retaining sharing within an occurrence. Under full-domain component summaries, guard substitution and namespaced observation union agree with flattened graph evaluation. This is an exact compositional presentation of the same partition.

Exactness does not imply compactness. A component with many outputs can require one summary family per demand mask, caller predicates can split component fibers differently at different occurrences, and residual substitution can duplicate large terms unless sharing is retained. Compositional summaries are therefore a representation and reuse strategy, not a general improvement in enumeration complexity.

These routes overlap rather than form a ranking. Section 9 compares their observers, guarantees, applicability, and closest established boundaries.

6. Full-fiber blocking and projected enumeration

The survey identified two general routes to enumerating the observer image. A local presentation discovers one complete fiber from a model, constructs its residual, and blocks the fiber. A global presentation constructs a whole-graph encoding and projects a conventional model enumerator onto totalized observation coordinates. This section states both in the unified terminology and proves that they enumerate the same observer. The constructions are comparison baselines, not claims of new generic enumeration paradigms. Projection directly supplies the observation index and, with model production, a witness and an exact fiber predicate obtained by fixing the projected tuple. It does not by itself construct a residual; satisfying the full record contract requires exact symbolic specialization of the requested values under the fiber guard, such as the demanded symbolic evaluator used by the local presentation. This paper calls that construction residualization; it is not a primitive operation supplied by an SMT solver.

6.1. Symbolic and solver assumptions

Every primitive, classifier outcome, case-membership relation, selected combiner, caller-domain predicate $𝐴$, and typed input-domain constraint must have an exact symbolic representation. A model-producing oracle for a formula returns sat(m), unsat, or unknown. Only unsat certifies exhaustion; unknown produces an explicit incomplete result. We do not assume that the oracle runs in polynomial time or that a decision-only oracle returns a witness for free.

Let ${Dom}_{𝐺\left(𝑥\right)}$ be the symbolic encoding of the typed input product and write

Every solver query below uses ${𝐴}_{\text{enc}}$. This is explicit because a bit-vector or integer lowering can otherwise admit codes that do not denote a typed graph input.

For an input model $𝑚\in {\mathrm{𝒳︀}}_{𝐴}$, a demanded evaluator carries three objects:

• a conjunction $𝑔$ of observed outcome predicates;
• a partial observation map $𝑇$; and
• a candidate-local memo $𝜇$ from graph-node identities to pairs of concrete and symbolic values.

The memo is essential for shared DAGs. Memoizing syntax-tree positions could duplicate one source site or allow inconsistent outcomes.

6.2. Concolic exact-fiber generation

The construction uses the standard DART-style pattern of one concrete model guiding a simultaneous symbolic evaluation (Godefroid et al., 2005); its additional obligation is to generalize that model to the entire exact observation fiber.

Evaluation of a demanded node $𝑣$ returns a concrete value ${𝑐}_{𝑣}$ at $𝑚$ and a symbolic residual ${𝑒}_{𝑣}$:

1. An input returns its component of $𝑚$ and its symbolic variable.
2. An ordinary node demands all operands and applies the exact concrete and symbolic primitive.
3. A selection $𝑞$ first evaluates its selector, including any selections in that cone. It computes $𝜔={𝜅}_{𝑞\left({𝑐}_{{𝑠}_{𝑞}}\right)}$, records $𝑇\left(𝑞\right)=𝜔$ once, conjoins ${𝜒}_{𝑞,𝜔}\left({𝑒}_{{𝑠}_{𝑞}}\right)$, evaluates exactly the case roots in ${𝐶}_{𝑞\left(𝜔\right)}$, and applies the corresponding symbolic combiner.
4. A memo hit reuses the pair and records no duplicate event.

Only selection outcomes are specialized to $𝑚$. Replacing an ordinary symbolic value by its sampled concrete value is unsound: it typically weakens the outcome guard while overspecializing the residual. Write

where ${𝑟}_{𝑚}$ is the residual tuple for the requested roots and the encoded complete guard is ${𝐴}_{\text{enc}}\wedge {𝑔}_{𝑚}$.

6.3. Full-fiber blocking

Initialize the uncovered formula ${𝑈}_0={𝐴}_{\text{enc}}$ and repeat:

1. Query the model oracle for ${𝑈}_{𝑗}$.
2. On unknown, return all accumulated records marked incomplete.
3. On unsat, return them marked complete.
4. On sat(m_j), compute $\left({𝑇}_{𝑗},{𝑔}_{𝑗},{𝑟}_{𝑗}\right)=Gen\left(𝐺,{𝑚}_{𝑗},𝑅\right)$ and emit $\left({𝑇}_{𝑗},{𝐴}_{\text{enc}}\wedge {𝑔}_{𝑗},{𝑟}_{𝑗},{𝑚}_{𝑗}\right)$.
5. Set ${𝑈}_{𝑗+1}={𝑈}_{𝑗}\wedge \neg {𝑔}_{𝑗}$.

Previous blockers are not folded into an emitted guard. Every query already assumes ${𝐴}_{\text{enc}}$, so the incremental blocker need only negate ${𝑔}_{𝑗}$.

This is a $𝐾+1$ model-producing invocation count under a unit-cost oracle. It is not an OutputP, IncP, DelayP, wall-clock, or decision-oracle theorem. Formula construction, serialized guard and residual size, solver work, and the final exhaustion query must all be charged separately.

6.4. Global reachability-and-outcome encoding

The alternative presentation symbolically evaluates every node, including unobserved case cones. Let ${𝑒}_{𝑣\left(𝑥\right)}$ be the exact whole-graph symbolic value of $𝑣$. For each case position define the direct predicate

Introduce one Boolean reachability indicator ${𝑎}_{𝑣}$ per node. It is true exactly when $𝑣$ is reachable from a requested root through an enabled consumer edge. The acyclic defining equations are

Multiple consumers contribute by disjunction, and the biconditional prevents spurious disconnected reachability. Acyclicity gives a unique valuation of the reachability circuit for every input.

For each selection site introduce a projected coordinate ranging directly over ${\mathrm{\Omega }}_{𝑞}\cup \left\{{unobs}_{𝑞}\right\}$:

Let ${\mathrm{\Phi }}_{𝐺,𝐴,𝑅}\left(𝑥,𝑎,𝑍\right)$ conjoin ${𝐴}_{\text{enc}}\left(𝑥\right)$, every displayed reachability biconditional, and every displayed coordinate definition. Project ${\mathrm{\Phi }}_{𝐺,𝐴,𝑅}$ onto $𝑍={\left({𝑧}_{𝑞}\right)}_{𝑞\in 𝑄}$, so its projected image is

An exact projected enumerator or finite decision-diagram compiler can then enumerate the feasible totalized observations. A Boolean-backed implementation may injectively encode the entire finite domain ${\mathrm{\Omega }}_{𝑞}\cup \left\{{unobs}_{𝑞}\right\}$ into designated projected atoms; an SMT enumerator with appropriate finite-domain projection may instead retain ${𝑧}_{𝑞}$ as a theory term.

Consequently, naive projected enumeration of complete observation tuples and full-fiber blocking have the same $𝐾+1$ model-producing invocation count. Full-fiber generation is an input-only, lazily constructed substitution of one projected-assignment blocker. An enumerator that emits a short partial cube has a different output contract: one cube may cover several complete selection observations.

6.5. Representation boundary

Local generation avoids constructing unobserved cones for one record and returns a sparse observation, guard, and residual directly. The global encoding constructs one shared whole-graph value/reachability circuit and reuses it across all records; it can exploit mature projected-enumeration algorithms that avoid a growing sequence of ordinary blocking clauses. Neither dominates in the general model. Classifier and direct case-membership circuits can themselves be exponential in a succinct selector description, and local output can repeat large residual structures unless DAG sharing is explicit.

The equivalence also fixes attribution. Projected enumeration supplies the generic enumerator (Phan & Malacaria, 2015; Spallitta et al., 2025); symbolic execution supplies residual construction; the graph-specific obligation is proving that enabled reachability selects the recorded sites and that the totalized unobserved/outcome coordinates and the observed-outcome guard induce the same observer fibers.

7. Compositional extension

The core framework treats one requested graph independently of any implementation strategy. This section extends that semantics to sequential components. It states when demand-parametric guarded summaries preserve the same observations as graph flattening, including contextual site identity and sharing. The result is an exactness theorem, not a compactness claim.

7.1. Graph substitution and sharing

Consider sequential components ${𝐺}_1:𝑋\to 𝑌$ and $𝐻:𝑌\to 𝑍$ with disjoint site namespaces and a type-preserving bijection $𝜌:{𝐼}_{𝐻}\to {𝑂}_{{𝐺}_1}$. Flattening removes the input nodes of $𝐻$, retains one context-prefixed copy $𝑐\cdot \left({𝑉}_{𝐻}\setminus {𝐼}_{𝐻}\right)$, and redirects every edge that targeted $𝑖\in {𝐼}_{𝐻}$ to $𝜌\left(𝑖\right)$. Call the resulting graph $𝐹$. Two uses of one retained node in either component remain shared; a second component occurrence receives a different contextual prefix.

Embed every downstream node into the flattened graph by

For input $𝑥$ and requested roots $𝑅\subseteq {𝑂}_{𝐻}$, define the boundary valuation ${𝑦}_{𝑖}={val}_{𝑥\left(𝜌\left(𝑖\right)\right)}$. The downstream enabled closure determines the demanded boundary inputs and hence the upstream root demand:

Operationally, picture a pipeline ${𝐺}_1\to 𝐻$. A downstream summary for $𝐻$ says which boundary inputs it needs. Those ports select the requested roots for an upstream summary of ${𝐺}_1$; the upstream residuals are then substituted into the downstream guard and residual. The contract below states exactly when that familiar substitution covers each flattened-graph input once.

A demand-parametric exact summary is defined by the structural projection

For every $\left(𝛿,𝜏\right)\in im\left({\mathrm{\Pi }}_{𝐺,𝑅}\right)$, the summary has exactly one record $\left(𝑔,𝛿,𝜏,𝑟\right)$ with

such that, for every full component input $𝑥\in {\mathrm{𝒳︀}}_{𝐺}$,

This is the exact-summary contract. It is a full-domain contract with no independent precondition: if an interface precondition mentions an otherwise undemanded input, that input must be charged as interface support. For fixed $𝑅$, the lockstep argument behind the exact observed-outcome guard shows that $𝜏$ determines $𝛿$; the demanded-port set remains explicit because it is needed by component interfaces.

For a downstream record $\left(ℎ,{𝛿}_{𝐻},{𝜏}_{𝐻},{𝑟}_{𝐻}\right)$ of $𝐻$ at demand $𝑅$, and an upstream record $\left(𝑔,{𝛿}_1,{𝜏}_1,{𝑟}_1\right)$ of ${𝐺}_1$ at demand $𝜌\left({𝛿}_{𝐻}\right)$, the summary contract gives the following exact guard and residual types:

Thus every expression below consumes precisely the demanded boundary tuple. For a full caller input $𝑥$, write $𝑥{|}_{{𝛿}_1}$ for its restriction to the demanded upstream ports. Reindex the upstream residual at the downstream inputs by

Their composed record is

Infeasible guard conjunctions are discarded.

This is equality with flattening, not a compactness theorem. A summary may contain one family for each of $2^{\left|{𝑂}_{𝐻}\right|}$ root-demand sets, and compatible record products may still be exponential. Guard substitution and exact piecewise residual composition are established techniques (Geyer et al., 2010); the graph-specific content is requested-root demand, demanded-input propagation, contextual identity, and preserved DAG sharing.

8. Complexity and specialized frontiers

The comparison framework must separate record count, representation size, oracle invocations, and actual enumeration complexity. This section first charges the graph, symbolic circuits, solver formulas, and serialized output, then identifies hardness in the general problem and stronger established frontiers for geometric and parametric specializations.

8.1. Parameters and enumeration classes

Table 4 fixes the charge model used below. Formula sizes are shared-DAG sizes unless a serialized representation is named explicitly.

In particular, ${𝑆}_{\text{enc}}$ may be larger than ${𝑆}_{𝐺}$, and ${𝑆}_{\text{out}}$ is meaningful only together with its declared flat or shared representation.

The source-node count alone is insufficient. A width-$𝑤$ mask-valued selector is one node but can have $2^{𝑤}$ mask outcomes. Lowering one multiway site to binary choices can also introduce auxiliary decisions whose projection must be merged back to one source outcome; such an elaboration must be charged separately.

OutputP requires total time polynomial in serialized input plus total output. IncP bounds the time to produce the first $𝑘$ solutions by a polynomial in the input size and $𝑘$ under the stated encoding and balance convention. DelayP bounds the time before the first output, between consecutive outputs, and after the last output by an input polynomial. A compiled decision diagram or d-DNNF is not free preprocessing unless it is declared to be the input. No such classification is proved for the general algorithm here: exact-record membership, SMT solving, coefficient growth, residual equivalence, and flat guard serialization need not be polynomial (Creignou et al., 2019).

8.2. Output count and unavoidable products

Totalization gives the general structural bound

The coordinates are not independent, so the bound may be loose. If every site is always observed, the 1 terms disappear. For $𝑛$ independent observed binary selectors, $𝐾=2^{𝑛}$, and any explicit record enumerator needs $\mathrm{\Omega }\left(𝐾\right)$ output time. Demand-relative omission cannot remove this necessary product. Conversely, a single mask-valued site can have $𝐾=2^{𝑤}$ while $𝐿=1$; trace length alone is not a complexity parameter.

The output quotient also matters. Dense activation cells can differ while implementing the same affine function, and piecewise-affine minimization can merge equal-behavior guards into coarser representations (Geyer et al., 2008). The selection observer retains observed equal-valued outcomes, so those merged output counts cannot be substituted for $𝐾$ without changing the task.

8.3. Cost of full-fiber blocking

Ignoring solver work, memoized candidate-local construction costs

shared-DAG operations and creates guard/residual DAGs of the same order. If every flat record copies ${𝐴}_{\text{enc}}$, output size includes $𝑂\left(𝐾{𝑆}_{{𝐴}_{\text{enc}}}\right)$; if records share one immutable reference to ${𝐴}_{\text{enc}}$, it includes only $𝑂\left({𝑆}_{{𝐴}_{\text{enc}}}\right)$ once. Complete record serialization additionally includes ${𝑊}_{\text{wit}}$; no representation-independent bound on witness byte length is assumed.

Before model query $𝑗$, the solver sees

An honest solver-time expression is therefore

The cumulative blocker DAG can grow to $𝑂\left(𝐾{𝑆}_{\text{enc}}\right)$, plus one shared copy of ${𝐴}_{\text{enc}}$. Incremental solving may reuse learned clauses but supplies no general monotone-runtime or polynomial-delay guarantee. The global projected encoding has one shared $𝑂\left({𝑆}_{\text{enc}}+{𝑆}_{{𝐴}_{\text{enc}}}\right)$ circuit but may spend exponential work compiling or enumerating its projected image. The two presentations have the same $𝐾+1$ model-producing invocation count under naive complete-tuple blocking, not the same runtime or memory.

Formula representation must also preserve graph sharing. In the chain

e0 = x
e1 = f(e0, e0)
e2 = f(e1, e1)
...
en = f(e[n-1], e[n-1])

the source DAG is linear while recursive tree serialization is exponential. Every size claim therefore refers to a formula DAG, let-bound SMT term, definitional encoding, or measured serialized bytes.

8.4. Decision and counting hardness

The hardness statements in this subsection are inherited boundaries obtained by standard circuit and SAT encodings, not contributions of this survey. Feasibility of one requested outcome is NP-hard even for Boolean graphs: let a selector compute an arbitrary circuit $𝐹\left(𝑥\right)$ and ask whether its true outcome is feasible. For polynomial-size Boolean circuits over explicitly encoded finite bit-vector inputs, a supplied input verifies feasibility in polynomial time, so that restricted problem is in NP. The general typed model allows primitives without a declared polynomial-time evaluation bound and therefore makes no uniform membership claim.

Counting feasible observations is #P-hard when $𝐴$ is part of the input. Under a Boolean constraint $𝐹\left(𝑥\right)$, expose every input bit as an always-observed binary outcome; observations are then injective on satisfying assignments and $𝐾=\#SAT\left(𝐹\right)$. We do not call general image counting #P-complete because many inputs may map to one observation and an upper-bound proof is separate. Checking that a supplied finite guard family covers every Boolean input is coNP-hard by propositional validity.

8.5. Hyperplane cells: a strict all-sites-observed case

Suppose every site is structurally observed. After canonicalization, let ${𝑄}_{𝑐}\subseteq 𝑄$ be a geometric core of $𝑚=\left|{𝑄}_{𝑐}\right|$ sites. For each $𝑞\in {𝑄}_{𝑐}$, the classifier is the strict sign of a nonconstant affine form ${\ell }_{𝑞}:{ℝ}^{𝐷}\to ℝ$, and distinct core forms define distinct hyperplanes. Constant and scalar-duplicate site coordinates are outside this core; a fixed reconstruction map restores their deterministic outcomes in each full observation record. Let $𝐴\left(𝑥\right)\iff {\prod }_{𝑞\in {𝑄}_{𝑐}}{\ell }_{𝑞\left(𝑥\right)}\ne 0$, and define each core classifier arbitrarily on zero outside that caller domain. Each feasible core observation is one full-dimensional open cell of the resulting $𝑚$-hyperplane arrangement, and $𝐾$ is equivalently the number of such cells and reconstructed observations. The cost symbols below are source-specific: ${𝐿}_{\text{AF}}\left(𝑚,𝑑\right)$ is the arithmetic cost of the LP used by Avis–Fukuda, while ${𝐿}_{𝐹}$ and ${𝐿}_{𝑅}$ denote the LP costs charged respectively by Ferrez et al. and Rada–Černý. Avis and Fukuda enumerate all $𝐾$ cells in

arithmetic time with $𝑂\left(𝑚𝐷\right)$ working space (Avis & Fukuda, 1996). Sleumer gives $𝑂\left(𝐾𝑚\right)$ arithmetic time for fixed $𝐷$ (Sleumer, 1998). For central arrangements, Ferrez, Fukuda, and Liebling give the pre-Rada bound

with $𝑂\left(𝑚𝐷\right)$ working space (Ferrez et al., 2005). Rada and Černý later give a different incremental sign-prefix formulation with $𝑂\left(𝐾𝑚{𝐿}_{𝑅\left(𝑚,𝐷\right)}\right)$ time (Rada & Černý, 2018).

All four algorithms are complete, duplicate-free, and output-polynomial under their stated arithmetic or LP-cost models. Rada–Černý additionally classify their bounded-encoding algorithm in OutputP; the other displayed operation bounds are not silently promoted to coefficient-bit theorems. For the full-dimensional rational zonotope dual to this central-arrangement case, Deza and Pournin give a self-contained rational-bit analysis of a traversal. If ${𝐵}_{𝑍}$ is total generator encoding length, its proof gives

for unspecified polynomials $𝑞$ and $𝑝$, while retaining all visited vertices and generator subsets (Deza & Pournin, 2022). The symmetry-aware White Whale successor can greatly reduce structured instances but gives no stronger generic theorem (Deza et al., 2026). Newer circuit-guided central-arrangement algorithms report large practical improvements without a replacement OutputP, IncP, or DelayP bound (Dussault et al., 2025).

These traversal bounds count core cells. Materializing dense records that restore every noncore coordinate adds $𝑂\left(𝐾\left|𝑄\right|\right)$ output work. They do not automatically bound the survey’s complete four-field record: residualization must be restricted to an explicitly charged affine/PWA computation or added to the construction and serialization cost, and witness production must also be charged.

The reduction has sharp boundaries. A non-strict classifier assigns boundary points to one side, and an arbitrary $𝐴$ can cut or lower the dimension of a fiber. Such a fiber need not be an open full-dimensional arrangement cell. None of the geometric bounds transfers automatically to general typed bitvector primitives or an arbitrary solver theory.

8.6. Parametric partitions

Jones and Maciejowski enumerate every full-dimensional critical-region basis of a multiparametric LP by reverse search. For their constraint matrix $𝑀\in {ℝ}^{𝑚\times 𝑛}$ with $rank\left(𝑀\right)=𝑚$, parameter dimension $𝑑$, $𝑒=𝑛-𝑚$, and ${𝑁}_{𝑟}$ regions, let ${𝐿}_{𝑃\left(𝑎,𝑏\right)}$ denote the paper’s exact LP-oracle cost at the displayed dimensions. Their LP-relative bound is

with output-relative constant auxiliary space; each basis reconstructs a polyhedral guard and affine optimizer (Jones & Maciejowski, 2006). The later sufficient-matrix pLCP treatment covers pLP and convex pQP and gives a stronger explicit comparator. For the separate pLCP dimension $𝑛$, parameter dimension $𝑑$, and ${𝑁}_{𝑔}$ reported bases in general position, let ${𝐿}_{𝐶\left(𝑎,𝑏\right)}$ denote that paper’s LP-oracle cost. Columbano, Fukuda, and Jones bound the work by

Under lexicographic perturbation, for ${𝑁}_{𝑝}$ perturbed bases the corresponding bound is

The perturbed basis count can exceed the number of unperturbed critical domains; the analysis retains an output-sized visited set and supplies neither a coefficient-bit nor a DelayP theorem (Columbano et al., 2009).

Separate work resolves other degeneracy and representation questions. Lexicographic perturbation selects a unique continuous affine optimizer and nonoverlapping basis regions (Jones et al., 2007). A minimum-norm secondary optimization yields, under stated assumptions, a unique continuous selection from the original pQP solution set with an algorithm-independent polyhedral representation (Spjøtvold et al., 2007). Patrinos and Sarimveis discover every full-dimensional convex-pQP neighbor across a facet without nondegeneracy or a facet-to-facet assumption, but state no polynomial total, delay, space, or bit bound (Patrinos & Sarimveis, 2010). Bemporad’s rank-deficiency treatment likewise gives practical per-combination analyses rather than a new enumeration-class theorem (Bemporad, 2015). Finally, pLP solution and halfspace polyhedral projection are polynomially interreducible, so renaming one side as projection does not establish a different complexity frontier (Jones et al., 2008).

The parametric objects also need a local correspondence caveat. The full-dimensional critical regions reported by Jones and Maciejowski are closed and can overlap on boundaries; regions that exist only in lower dimension are not emitted. Without a boundary-ownership convention or a caller-domain restriction that removes those boundaries, this is not the disjoint all-input fiber contract of Section 3. Parametric results are therefore adjacent optimizer/basis comparators unless a target-observer correspondence is proved.

8.7. General equivalence-class enumeration

Wang et al. give a different strong frontier: from an explicitly supplied acyclic decomposable AND/OR solution graph with locally colored OR nodes, their Next algorithm enumerates every contracted colored solution-tree class exactly once with delay $𝑂\left(𝑛𝑠\right)$, where $𝑛$ is graph size and $𝑠$ is the solution size (Wang et al., 2021). This establishes exact quotient enumeration with polynomial delay as prior art. It does not classify the present problem: no general reduction from the selection observer to that decomposable representation is known, and its outputs are class trees rather than exact caller-input guards, residuals, and witnesses.

The resulting complexity claim is intentionally negative but precise: the general theory proves finite exact enumeration and an exact $𝐾+1$ oracle-call accounting, while established special cases already have stronger output-sensitive algorithms. It proves no general asymptotic advantage from demand-relative sparsity alone.

9. Comparative synthesis

The six routes overlap in mechanism and representation, so listing them does not yet show whether they solve the same problem. This section compares their observers and record guarantees, identifies the closest established results that bound the survey’s claims, and answers the four research questions.

9.1. Observer, contract, and representation

The observer-kernel test gives the shortest comparison. Projected enumeration and candidate-local symbolic evaluation are direct general presentations after the instrumentation proved in Section 6. Decision structures are direct when they compile the totalized observer; dense-sign geometry is direct only on its all-sites-observed affine restriction; and demand-guided, parametric, or compositional methods require the correspondence conditions stated in Section 5 and Section 7.

This is more precise than asking whether a method emits a “partial assignment.” Structural absence is an observer value; existential projection hides formula coordinates; a logical don’t-care represents either value; and equal-residual coalescing takes a quotient. Similar syntax can therefore denote different fibers.

The record contract adds four independent obligations: duplicate-free coverage, guard/fiber equivalence, residual correctness, and a witness. Output representation remains orthogonal: a flat record stream, tree, decision DAG, or polyhedral complex may encode the same observer while charging very different construction and serialization costs. The two tables below separate published native guarantees from the framework correspondence needed to obtain the target contract.

9.2. Complexity takeaway

The general problem can have exponentially many observations and contains hard feasibility and counting special cases. Its $𝐾+1$ model-query accounting is not an output-sensitive theorem; stronger guarantees belong to restricted or precompiled inputs and must charge residuals, witnesses, and representation size as Section 8 specifies.

9.3. Closest established results

The nearest results are output-directed and dataflow-specific, while the strongest novelty boundary comes from exact equivalence-class enumeration on a different representation. Table 5 consolidates those published native objects and guarantees.

The general routes require a separate table because several rows are framework reductions or restricted correspondences rather than native end-to-end algorithms for the target.

The tables make two novelty boundaries explicit. Output-directed guarded exploration and sparse executed-choice maps are established, and Wang et al. already prove exact polynomial-delay quotient enumeration for a restricted decomposable representation. Their class-tree output does not, however, supply arbitrary caller-input guards, residuals, or witnesses.

Three exact correspondences remain open: whether instrumented PESO plus RSC quotienting yields exactly one selection fiber; whether SPD’s dependence families denote the enabled-closure observer rather than a refinement; and whether Feng’s actual split/merge algorithm, augmented with immutable contextual event labels, preserves every target observation. The survey does not use their absence of an explicit theorem as evidence that no reduction exists.

The strongest adjacent boundaries remain useful but should not be mistaken for the closest algorithms. Requested-output quotients can merge distinct internal histories, as in common-first-action controller regions (König & Mönnigmann, 2020; Mitze et al., 2021) and exact neural-policy decision trees (Chang et al., 2026). Giua et al. give exact inverse consistency for Petri-net markings under an observed label word (Giua et al., 2003). SymPaths records scheduler choices and proves its symbolic semantics sound and complete against concrete executions (Boer et al., 2020). Lindblad’s property-blocked constructor search is a close demand-refinement shape, but its stated soundness and completeness conditions are explicitly unproved (Lindblad, 2008); Korat and the BLISS–LISSA–PLI heap line establish stronger bounded access-guided and feasibility-preservation results for different artifacts (Boyapati et al., 2002; Copia et al., 2022; Copia et al., 2023; Rosner et al., 2015). Finally, Fisler and Vardi show that exact BDD bisimulation minimization can cost more than direct symbolic checking (Fisler & Vardi, 2002). No performance claim follows from the observer-fiber construction alone.

9.4. Adjacent reduction problems

Several broad literatures informed the observer vocabulary without providing alternative implementations of the target contract. Partial-order reduction omits redundant interleavings while preserving reachable states or temporal properties (Alur et al., 2001; Holzmann et al., 1992). Petri-net unfoldings represent concurrent configurations, and goal-directed prefixes can preserve all minimal configurations reaching a requested marking while omitting irrelevant transitions (Bonet et al., 2014; Chatain & Paulevé, 2017). Observer- and property-guided state reduction preserves a declared event language, state quotient, or coverage objective (Aronis et al., 2018; Bugrara & Engler, 2013). These works confirm the general lesson that omission is observer-relative, but their outputs are runs, markings, states, or search objectives rather than caller-input fibers with residual functions.

Whole-network dataflow semantics similarly supplies important boundaries for determinism, stability, and compositionality, but usually observes streams, traces, or network behavior rather than finite requested-root selection maps. The main comparison therefore uses fixed-input least-demand results where they directly explain enabled closure and leaves the broader semantic lineage in the repository synthesis.

9.5. Answers to the research questions

RQ1. The common object is a finite observer on caller inputs. Its nonempty inverse images are fibers, and an exact record attaches a guard, residual, and witness to each fiber. This distinguishes semantic partitioning from the algorithm and data structure used to expose it.

RQ2. The included approaches organize into six recurring, overlapping routes. Local guarded evaluation and global projected enumeration are equivalent general presentations; decision structures compile the observer; demand-guided methods supply sparse discovery mechanisms; dense-sign geometric methods solve a restricted affine specialization; and guarded summaries provide composition.

RQ3. General exactness follows only after all four record obligations are proved. General output-sensitive complexity does not follow from sparse demand or one model per fiber. Stronger bounds belong to restricted geometric, parametric, or compiled inputs and must charge their representations. The route-by-route obligations and assumptions are summarized in Table 5 and Table 6.

RQ4. Approaches induce the same fibers when their observer kernels agree after explicit instrumentation. Their labeled images and record schemas then correspond only after an explicit image bijection. Coordinate projection, equal-behavior merging, path refinement, and property-guided search otherwise produce coarser, finer, or incomparable partitions. This observer test is the framework’s primary rule for transferring results across terminology; the two guarantee tables record the known equality, open, and incomparable cases.

10. Boundaries and open problems

10.1. Applicability of selection observations

Selection observations may support event-aware specifications such as checking that graph rewriting, lowering, or component substitution preserves a declared map of source selection events. This is a motivating hypothetical in the present paper, not a demonstrated application: no worked validation case or evaluation is reported. They are not preferable for every client. A value-only client should merge behaviorally equal records, as explicit-control methods do when they group regions that share the requested first action (König & Mönnigmann, 2020) or compile an exact extensional policy tree (Chang et al., 2026); an optimization client may retain active constraints rather than source events; and a diagnostic client may record causal events beyond selections. The framework makes these choices explicit rather than ranking them by a universal notion of precision.

10.2. Semantic scope

The theory assumes a finite, typed, acyclic, deterministic, pure graph. Ordinary primitives, classifiers, and selected combiners are total. Partial operations require a proved caller precondition or an explicit error outcome; silently ignoring division by zero, invalid indexing, assertion failure, or language-specific overflow would invalidate coverage. Cycles, recursion, and unbounded dynamic occurrences can make the event domain infinite and require a bounded, time-indexed, regular, or coinductive observer instead.

The all-operands rule is an observation policy, not an extensional dependence theorem. Every operand of an ordinary node is observed even if algebraic simplification makes it irrelevant. Translating a lazy language or stream-dataflow semantics therefore requires a separate correspondence proof. Likewise, an outcome must determine its demanded cases and combiner; two raw selector values with different structural consequences cannot be silently grouped as one outcome.

Site identity is structural and occurrence-sensitive. Sharing within one graph or component occurrence records a site once, whereas distinct contextual occurrences receive distinct names. A compiler that duplicates, fuses, or lowers selections can change the observer while preserving values. Source and lowered observations need an explicit event map. The exact observed-outcome guard is not necessarily a literal-minimal formula: logical minimization is a later representation transformation and may erase the event whose outcome the record is intended to expose.

10.3. Solver, output, and composition boundaries

Exhaustion depends on exact symbolic encodings and decisive oracle answers. An unknown, timeout, unsupported primitive, incomplete theory combination, or inexact floating-point abstraction yields an explicitly incomplete result. A model is a witness for one fiber, not a residual valid throughout it.

The exact $𝐾+1$ model-producing invocation count is deliberately weak. It does not charge solver work, formula growth, coefficient bits, projection, serialization, or final unsatisfiability. The number of fibers can be exponential, and feasibility and counting contain familiar hard special cases. No general OutputP, IncP, DelayP, compact-summary, or practical-speedup theorem is established. The negative precedent is explicit: BDD bisimulation minimization can cost more than the symbolic invariant check it was meant to accelerate (Fisler & Vardi, 2002).

Representation can dominate the comparison. Flat guards, trees, diagrams, compiled circuits, polyhedral complexes, and residual DAGs may denote the same observer with exponentially different sizes. Exact guarded-summary composition has the same caveat: equality with flattening does not imply reuse. A component with many outputs can require exponentially many demand masks, and different caller predicates can split its fibers differently at each occurrence.

The exact-guard, projection-equivalence, demanded-port locality, and guarded-summary composition results are survey-authored derivations. They have not been peer reviewed, mechanized, or independently verified. In particular, the paper has not proved exact correspondence between its observer/record contract and PESO’s relevant-slice conditions, SPD’s path-family graph, or Feng et al.‘s actual functional-space split/merge algorithm. Those are explicit open reduction questions, not implicit novelty evidence.

The evidence map is also open. The dated search snapshot contains an unresolved candidate backlog, so it supports the comparisons made from adjudicated and deep-read works but not a claim that every captured plausible competitor has been assessed.

10.4. Open theoretical questions

The framework suggests a focused research agenda:

• Which observer languages make selection events, value behavior, active constraints, and diagnostic causality explicit, and which refinement or full-abstraction results relate them?
• Which classes of partial operations, cycles, or recurring component occurrences retain a finite or finitely representable observation image?
• When can a shared decision structure, disjoint cover, or guarded-summary DAG be constructed with output-sensitive delay or polynomial auxiliary space?
• Which structural restrictions make demanded local generation asymptotically preferable to whole-graph reachability projection, rather than merely smaller on one candidate?
• Under what interface and workload conditions do demand-parametric summaries provide reusable compression instead of an exponential family of exact fibers?

These questions keep the observer, enumerator, and representation separate. Improving one does not automatically strengthen the other two.

10.5. Reference implementation and evaluation agenda

This paper reports no implementation or benchmark result. A reference implementation should first validate small finite graphs by exhaustive concrete input enumeration, checking observation identity, guard membership, residual values, witnesses, and coverage. It should then compare local full-fiber blocking, global projected enumeration, finite-input ADD or MTBDD compilation, and specialized geometric traversal on inputs that expose nested unobserved sites, equal-valued observed alternatives, sharing, multiple roots, multiway choices, lower-dimensional fibers, and repeated components. Measurements should report serialized and shared output size, compilation cost, solver effort, peak memory, and final-exhaustion cost—not only record count.

11. Conclusion

Exhaustive enumeration of selection observations is a specific observer-partition problem. For a caller domain and requested roots in a pure shared dataflow graph, each input induces a sparse map of contextual selection outcomes. The exact output is one guard, residual, and witness for every nonempty inverse-image fiber of that map.

The unified framework separates this semantic object from the method used to enumerate it and the structure used to represent it. Guarded symbolic execution, projected model enumeration, decision structures, demand-guided search, geometric traversal, and compositional summaries consequently become comparable without being declared equivalent by terminology alone. Local observed-outcome-guard generation and global reachability-and-outcome projection are two general presentations of the same observer. Decision structures compile it, affine methods solve important restricted specializations with stronger guarantees, and component summaries preserve it only under explicit demand, identity, and interface conditions.

The survey finds no new generic enumeration paradigm or general complexity advantage. Its contribution is a precise problem statement, common vocabulary, transfer criteria, and an evidence-backed analysis of known solution routes. Future progress should therefore state which observer is preserved, which record obligations are met, which representation is charged, and which assumptions support any claimed improvement.