Proposal — Symbolic Execution Strategy NOT IMPLEMENTED

A retrieval strategy that uses symbolic reasoning to verify or reject candidates based on logical consistency with the query's constraints.

The Idea

BM25 matches words. HDC/VSA matches structure. Neither checks logical consistency. If the user asks "What works for CPU-only deployment?" and a KB unit says "Requires GPU with 16GB VRAM", BM25 might score it high (matches "deployment") but it contradicts the constraint.

A symbolic execution strategy would detect this contradiction and prune the candidate, even if its BM25 score is high.

How It Would Work

1. Extract constraints from intent: Context, Criterion, Evidence fields
2. Extract claims from each BM25 candidate
3. Check consistency: does the claim contradict any constraint?
4. Prune contradictory candidates (when hardSymbolicPruning = true)

Candidate Approaches

Approach	Complexity	Precision	Description
A: Pattern-based	Low	Medium	Detect simple contradictions: "CPU-only" vs "requires GPU", "no network" vs "cloud-based". Keyword negation patterns.
B: Constraint graph	Medium	High	Build a constraint graph from intent fields. Propagate constraints. Check if candidate claims are reachable/consistent.
C: Z3 integration	High	Very high	Translate constraints and claims to SMT formulas. Use Z3 plugin to check satisfiability. Most powerful but slowest.

Recommended starting point: Option A — simple, fast, covers the most common contradictions.

Profile Integration

Would be used in a new symbolic-grounded profile:

{
  "symbolic-grounded": {
    "primaryStrategies": ["bm25-lexical"],
    "secondaryStrategies": ["symbolic-fixedpoint"],
    "hardSymbolicPruning": true,
    "maxResults": 5,
    "minScore": 0.2,
    "confidenceGapThreshold": 0.40
  }
}

BM25 runs first, then the symbolic strategy prunes inconsistent results. With hardSymbolicPruning = true, pruned candidates are removed even if their BM25 score is high.

Why Not Yet

• Requires well-structured constraints in Intent CNL — current normalization doesn't reliably produce Criterion and Evidence fields for all inputs
• Evaluation framework needs constraint-specific test suites (e.g., "given CPU-only, should NOT retrieve GPU-dependent units")
• Pattern-based approach (Option A) is straightforward to implement but needs a curated contradiction dictionary

Implementation Path

1. Extend Intent CNL normalization to reliably extract structured constraints
2. Implement pattern-based contradiction detector (src/mrp-vm-sdk/retrieval/strategies/symbolic-fixedpoint.mjs)
3. Add symbolic-grounded profile to config/retrieval-strategies.json
4. Create evaluation suite with constraint-contradiction scenarios
5. Optionally: integrate with Z3 plugin for formal verification (Option C)