Exhaustive Enumeration of Selection Observations in Pure Dataflow Graphs: A Survey and Unified Framework
Summary
A problem-centered scoping survey and theory/position synthesis for a proposed semantic contract: enumerate every requested-root-relative selection observation of a finite pure dataflow graph, with one exact input guard, residual value, and witness per nonempty fiber. It identifies the closest prior work, separates observer, enumeration mechanism, and output representation, presents local and global SMT baselines and restricted output-sensitive special cases, and makes the remaining correspondence, implementation, and evaluation questions explicit.
Links
Reading list
The works that anchor the comparison, curated from the deep-read set and organized by the survey’s six routes, with the foundations that fix the formal object and the adjacent comparators that bound it. Entries link the original paper (DOI where one exists) and our notes on it (library pages where ingested, our evidence notes in the record otherwise).
Problem and foundations
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Efficient Demand-Driven Evaluation. Part 1 | Local, structure-directed reverse demand for stream dataflow graphs, proved correct and parsimonious compositionally | TOPLAS · 1985 | notes |
| Stability, Sequentiality and Demand Driven Evaluation in Dataflow | Defines the least demanded computation for fixed inputs and requested output positions — the fixed-input core of enabled closure, under stability assumptions | Formal Aspects of Computing · 1994 | notes |
| A Complexity Theory for Hard Enumeration Problems | Fixes what delay, incremental, and output-polynomial mean — the standard that reclassifies “one solver call per solution” as an oracle-call count | Discrete Appl Math · 2019 | notes |
| Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics | Mechanized backward propagation of an output request to a minimal sufficient partial input — demand as definedness, not an internal selection trace | ICFP · 2024 | notes |
| A General Framework for Enumerating Equivalence Classes of Solutions | Enumerates every locally colored solution-tree class exactly once with polynomial delay from an acyclic decomposable AND/OR graph — the strongest general quotient-enumeration precedent, under a different representation and output contract | ESA · 2021 | notes |
Closest dataflow-specific predecessors
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Improved Symbolic Simulation by Dynamic Functional Space Partitioning | Mux-selected control/data cells pair mutually exclusive guards with residual data expressions — the closest restricted pure-dataflow representation | DATE · 2004 | notes |
| Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models | Groups initial states by bounded discrete traces that include conditional-block outcomes and carries symbolic transformers, but underapproximates a sampled class | CAV · 2009 | notes |
| Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs | Modular RTL path-fragment exploration with SMT feasibility and replayable witnesses; construction savings do not remove the exponential combination boundary | FMCAD · 2023 | notes |
Guarded symbolic execution
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Path Exploration Based on Symbolic Output | The closest formal predecessor: relevant-slice conditions, symbolic requested outputs, witnesses, and conditional exploration completeness | TOSEM · 2013 | notes |
| Exploiting Program Dependencies for Scalable Multiple-Path Symbolic Execution | The closest shared path-family/residual predecessor: query-relevant guarded symbolic values in a shared graph, without a numbered end-to-end exact-fiber theorem | ISSTA · 2010 | notes |
| All-Values Symbolic Execution | Reindexes exploration by the distinct symbolic values reaching a statement rather than by path; author-run experiments report large savings, but equal-valued alternatives lose their selection identity | AST · 2012 | notes |
| MultiSE: Multi-Path Symbolic Execution Using Value Summaries | Value summaries already represent many executions as disjoint, collectively exhaustive guard/expression pairs | ESEC/FSE · 2015 | sen2015 |
| A Formal Foundation for Symbolic Evaluation with Merging | Mechanized evaluator whose guarded choices exactly represent the reachable concrete outcomes | POPL · 2022 | notes |
| Grisette: Symbolic Compilation as a Functional Programming Library | Normalized union merging supplies the representation half of a guarded-residual enumerator, without defining enabled-edge activity or fiber leaves | POPL · 2023 | notes |
| Compositional Symbolic Execution Semantics | Exact mechanized denotation of symbolic execution as substitution/path-condition pairs with generic composition equations | Theor Comput Sci · 2025 | notes |
Projected model enumeration
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| All-Solution Satisfiability Modulo Theories | AllSMT over designated Boolean coordinates with sampled theory values — the solver-level reduction any enumeration claim is measured against | ARES · 2015 | phan2015 |
| Disjoint Partial Enumeration without Blocking Clauses | Mutually exclusive partial models via chronological backtracking and implicant shrinking; unassigned variables are logical don’t-cares, not structurally unobserved sites | AAAI · 2024 | notes |
| Leveraging Decision-DNNF Compilation for Enumerating Disjoint Partial Models | Disjoint covering partial models with polynomial post-compilation delay; a faithful reduction still needs an explicit activity variable | KR · 2024 | notes |
| Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses | The strongest direct solver baseline: projected AllSAT/AllSMT that subsumes the target task after polynomial activity/outcome instrumentation | Artif Intell · 2025 | spallitta2024 |
Compiled decision structures
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Graph-Based Algorithms for Boolean Function Manipulation | Reduced ordered BDDs: the canonical baseline for compiling an observation function by root-to-terminal traversal and extensional reduction | IEEE Trans Comput · 1986 | notes |
| Algebraic Decision Diagrams and Their Applications | Terminals beyond Booleans — exact for selection fibers only when the terminal carrier is the complete observation rather than the program output | Formal Methods Syst Des · 1997 | notes |
| Effective Infinite-State Model Checking by Input Equivalence Class Partitioning | Builds the coarsest input-equivalence-class partition of an infinite domain by enumerating satisfiable transition-condition combinations | ICTSS · 2017 | notes |
| Affinitree: Formal Analysis and Explanation of Deep Neural Networks | Compiles piecewise-linear networks into exact affine guard/residual decision structures, LP-pruning infeasible and entailed tests with a preservation proof | TAP · 2024 | notes |
| Exhaustive Property Oriented Model-Based Testing with Symbolic Finite State Machines | Exact finite equivalence partition of infinite input/output domains via SMT-enumerated atoms over a declared observation alphabet | Sci Comput Program · 2024 | notes |
Demand-guided evaluation and search
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Set Functions for Functional Logic Programming | Introduces fingerprints of executed nondeterministic steps — the beginning of a lineage that later gains stable choice-ID propagation and explicit task-local partial maps | PPDP · 2009 | notes |
| Memoized Pull-Tabbing for Functional Logic Programming | Demand-populates a task-local choice-ID/outcome map and reuses it across traversal; the closest partial-map representation, under a different nondeterministic observer | WFLP · 2021 | notes |
| SPLat: Lightweight Dynamic Analysis for Reducing Combinatorics in Testing Configurable Systems | Discovers configuration variables on first read, prunes infeasible partial assignments with SAT, and executes witnesses for claimed distinct traces, but emits no exact symbolic fiber guard or residual | ESEC/FSE · 2013 | notes |
| SmallCheck and Lazy SmallCheck: Automatic Exhaustive Testing for Small Values | Refines only the input a Boolean observation demands and prunes all completions once the answer is known — refutation, not fiber enumeration | Haskell · 2008 | notes |
| On the Correctness of Pull-Tabbing | Shared choice identifiers in term-graph rewriting already yield sound, evaluation-order-independent exhaustive enumeration of consistent results | Theory Pract Log Program · 2011 | notes |
| Implementing Functional Logic Programs by Translation into Purely Functional Programs | Choice-ID translation with a proved value-set equality; its finite partial map from choice identifiers to outcomes is the closest precedent for a sparse selection record | PhD thesis, Kiel · 2011 | notes |
| Implementing a Functional Logic Programming Language via the Fair Scheme | The Fair Scheme’s fullest formalization: sound, complete, optimal narrowing over demand-populated fingerprints | PhD dissertation, Portland State · 2023 | notes |
Geometric and parametric enumeration
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Reverse Search for Enumeration | General memory-efficient output-polynomial enumeration, already instantiated for exact duplicate-free arrangement cells | Discrete Appl Math · 1996 | avis1996 |
| Reverse Search for Parametric Linear Programming | Duplicate-free, output-sensitive traversal of every full-dimensional critical region, each basis giving a polyhedral guard plus an affine optimizer | CDC · 2006 | notes |
| Optimal Complexity Reduction of Polyhedral Piecewise Affine Systems | Merges cells carrying equal behavior into a smaller exact representation — the precise counterpoint to an observer that keeps distinct outcomes with equal residuals | Automatica · 2008 | notes |
| An Output-Sensitive Algorithm for Multi-Parametric LCPs with Sufficient Matrices | Generic traversal covering parametric LP and convex parametric QP, with explicit per-output LP-oracle work — the strongest closed output-sensitive bound in that lineage | Polyhedral Computation · 2009 | notes |
| Reachable Polyhedral Marching | Enumerates every feasible ReLU activation pattern with its exact input polyhedron and affine output map by adjacency-based work-list traversal | ICRA · 2021 | notes |
| A New Algorithm for Enumeration of Cells of Hyperplane Arrangements | Proof-bearing incremental sign-prefix enumeration — exact, duplicate-free, output-polynomial, but always assigning a side to every hyperplane | SIAM J Discrete Math · 2018 | notes |
Compositional guarded summaries
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Compositional Dynamic Test Generation | SMART’s reusable per-function pre/postcondition summaries — avoiding interprocedural path products is established prior art | POPL · 2007 | notes |
| Demand-Driven Compositional Symbolic Execution | Exact partial summaries expanded toward one target location — demand-driven composition without enumerating all observations | TACAS · 2008 | notes |
| Efficient Mode Enumeration of Compositional Hybrid Systems | Substitutes upstream affine residuals into downstream guards with infeasibility pruning — guarded residual composition in the affine case, with no requested-root demand | Int J Control · 2010 | notes |
| Selective Applicative Functors | Laws, a free construction, and reusable interpreters for a static computation graph whose effects are selected dynamically | ICFP · 2019 | notes |
Adjacent comparators
| Paper | What | Venue · Year | Notes |
|---|---|---|---|
| Marking Estimation of Petri Nets Based on Partial Observation | Exact inverse-consistency set for an observed label word via a fixed-structure linear system — hidden states, not caller-input fibers with residuals | ACC · 2003 | notes |
| Goal-Driven Unfolding of Petri Nets | Skips transitions outside every minimal goal-reaching configuration while preserving all minimal configurations | CONCUR · 2017 | notes |
| Optimal Dynamic Partial Order Reduction with Observers | Explores exactly one representative per observation-equivalence class of schedules — observer-relative omission over interleavings, not inputs | TACAS · 2018 | notes |