CSP: Universal Constraint Satisfaction via the P/NP/P Sandwich

1. Framework

A CSP instance is a tuple (X, Φ, ONES, ZEROS) where:

The conflict predicate C(i,v,j,w)→{0,1} is called once to build the ONES/ZEROS indices, then discarded. All solving uses indexed lookups — no black-box queries.

1.1 Why indexed collections, not a predicate

Constraints are data, not queries. The ONES index can be walked, filtered, and updated. Propagation becomes set arithmetic on the index. Learning is native — new forbidden pairs are added directly to ONES. The vulnerability ratio |ONES[(i,v)]| / (|ZEROS[(i,v)]| + 1) gives a per-value fragility score for variable/value ordering.

2. The P/NP/P Sandwich

The solver decomposes into three zones, following the architecture established in the Sudoku and SAT papers:

P-Left techniques run in a fixpoint loop — when any technique makes progress, the loop restarts from Tier 0. This maximizes deductive reach before entering the NP-Strip.

3. LIFO Propagation (Tier 0)

When a domain becomes singleton {v}, all forbidden partners from ONES[(i,v)] are removed from neighbor domains. Removals that create new singletons are processed depth-first (LIFO stack), catching contradictions early and maximizing cascade depth.

propagate():
    while stack not empty:
        (i, v) = stack.pop()           # LIFO
        if v ∉ Φi or |Φi| ≠ 1: continue
        for (j, w) in ONES[(i, v)]:
            if w ∈ Φj:
                Φj.remove(w)
                trail.append((j, w))
                if Φj = ∅: return CONTRADICTION
                if |Φj| = 1: stack.push((j, sole(Φj)))
    return OK

4. Failed Value Probing (Tier 3)

For each variable i with |Φ_i| > 1, for each value v ∈ Φ_i: temporarily assign x_i=v, propagate. If contradiction: v is dead — permanently remove from Φ_i. Uses snapshot/restore for clean undo.

This is BCP-1 generalized from SAT to arbitrary CSP domains.

5. Markov Chain Branch Evaluation (Tier 5)

Before committing to a decision in cdcl, a short Markov chain run from the partial assignment reveals the effective difficulty of completing it:

evaluate_branch(i, v):
    assignment = partial ∪ {xi = v} ∪ random_fill(undecided)
    for step in 1..K:
        j = random(conflicted_variables(assignment))
        assignment[j] = argminw ∈ Φj conflicts(j, w)
    return total_conflicts(assignment)  # residual = branch quality

Residual = 0: branch leads to a solution. Low residual: easy subproblem. High residual: likely dead end. This is a Monte Carlo estimate of the remaining search depth, information that propagation alone cannot provide.

6. Markov Chain Walk (Tier 6)

Adapted directly from the Logistics framework (Dana, 2023). The walk operates on the reduced domains from P-Left:

1. Greedy init: assign each variable to min-conflict value
2. Repeat:
   a. Pick random conflicted variable (from incremental counter)
   b. Sample K candidates from Φi, pick min-conflicts
   c. Accept: improvement (always), lateral (always), worse (SA probability)
   d. Adaptive restart when stale

Conflict tracking is incremental using the ONES index: O(degree) per update instead of O(n²). The walk's convergence bound from the Logistics paper: O(n^a+1 M² ln M).

7. Connection to the Dana Theorem

The Dana Theorem for CSP (2024, extended 2026) states: any indicator function over a finite dataset can be encoded as a CSP in polynomial time. Snake implements this construction; this solver operates on the resulting instances.

The ONES/ZEROS collections are the CSP analogue of AUMA's weighted clause set W. The conflict predicate is the analogue of clause evaluation. The Markov chain walk is the same framework that originated in the Logistics bin packing paper.

8. Experimental Results

8.1 Technique attribution

The sandwich correctly routes problems to the right tier:

• Easy Sudoku → P-Left Tier 0 (propagation alone solves it)
• Hard Sudoku → P-Left eliminates 8 values via probing, cdcl finishes in 4ms
• Petersen 2-color → P-Left Tier 3 proves UNSAT (probing finds all values dead)
• 100-Queens → NP-Strip walk (search space too large for cdcl, walk converges in 162 restarts)

9. CSP-Classification Equivalence

Any CSP is a boolean classification problem on the Cartesian product of its domains. Any boolean classification problem is a CSP. They are the same object.

9.1 CSP → Classification

Let a CSP have variables X₁, ..., X_m with finite domains D₁, ..., D_m and constraints C. Define:

Every ω ∈ Ω is a complete assignment. The constraint predicate defines an indicator:

The CSP IS a boolean classification on Ω. Licit = positive class. Illicit = negative class. Solving = finding a positive.

9.2 Classification → CSP (Dana Theorem)

Any indicator function over a finite dataset can be encoded as a CSP in polynomial time (Dana Theorem for CSP, 2024/2026). The boolean tests on features become constraints. Snake implements this construction: oppose() finds separating tests, the bucket chain builds constraints, the 30 literal types provide the test library.

9.3 The equivalence

The difference is operational:

• Classification asks: given an element, is it positive or negative? (evaluation — polynomial)
• CSP asks: find me a positive element. (search — NP-hard)

Same function, different question. Every tool from one domain applies to the other:

10. Lineage

AUMA (2023)         — {f: {0,1}n → R} ⊂ W, everything is weighted MAXSAT
Dana Theorem (2024) — indicator → CNF in poly time
Snake               — SAT classifier, 30 literal types, oppose profiles
PolySAT             — 16 polynomial techniques on SAT
Sudoku sandwich     — P/NP/P decomposition for Sudoku
Logistics           — Markov chain CSP, superposition + random walk
CSP                 — universal solver, indexed ONES/ZEROS, P/NP/P sandwich

11. API Reference