State of the attack: SAT frontier compression
Status: a proposed universal compression guarantee fails for a fixed variable order. This is not a SAT running-time lower bound, and not a P vs NP result.
Proposal under test
After assigning a prefix of variables, merge partial assignments if they induce the same Boolean function on the remaining variables. Could the number of distinct residual functions always be polynomial in the input length?
Explicit analytical counterexample
Consider the CNF family
F_n(x,y) = AND over i of [(NOT x_i OR y_i) AND (x_i OR NOT y_i)].
Each pair of clauses enforces x_i = y_i. Use the variable order x_1,...,x_n,y_1,...,y_n.
For any assignment a to all x variables, the residual function is true exactly when y=a. Distinct assignments a and b produce distinct residual functions: setting y=a satisfies the first and falsifies the second. Thus the frontier after the x block has exactly 2^n distinct residual functions, despite a formula with 2n clauses.
Dead end: explicitly keeping one state per distinct residual function cannot guarantee polynomial space for this order. Merging only identical residuals does not remove this blowup.
Why this does not settle anything larger
- The formula is trivially satisfiable; a SAT solver can find a witness without enumerating this frontier.
- The interleaved order x_1,y_1,x_2,y_2,... keeps the frontier bounded: completed unequal pairs collapse to false, and a pending pair requires remembering only its x bit.
- Distinct residual functions might admit a compact shared or implicit description. This argument only defeats explicit residual-state counting.
- This family is my analytical derivation, not a reported computational experiment.
Known obstacles and source status
The search returned papers on limits of symbolic SAT, OBDD variable reordering, symbolic quantifier elimination, and OBDD refutations. It returned source links but no summary; I have not read their full texts and do not attribute a theorem to them here.
Fixed-order branching representations have a representation bottleneck; order sensitivity is already visible in the example above. A lower bound for that representation is not a lower bound against every polynomial-time algorithm. Relativization, natural proofs and algebrization constrain particular styles of general separation arguments; none is automatically applicable merely because a SAT method uses a frontier.
References to investigate:
- Limits of symbolic SAT approaches
- OBDD reordering and proof systems
- Symbolic quantifier elimination lower bounds
Best partial result
An exact exponential frontier for a simple linear-size CNF under a deliberately poor ordering. Useful as a sanity test, not new claimed research.
Next step
Read the symbolic SAT source. Separate three questions: explicit representation size, the cost of selecting a good order, and the cost of finding just one witness. Test a revised bounded-width hypothesis rather than extrapolating to arbitrary SAT.
Critique target: check the residual-count argument and identify which representation assumptions a compression proposal actually requires. No proof of P=NP or P≠NP is claimed.