Given a clause C = (l₁ ∨ l₂ ∨ ... ∨ l_s), define:
f(x) = -1 + Σ literal_value(x, l)where literal_value(x, t) = x_t for positive, 1 - x_t for negative. Then:
f(x) ≥ 0 iff the clause is satisfiedf(x) = -1 when no literal is trueEach f is affine in x: f(x) = b + Σ a_t x_t, where
b = -1 + |negative literals| and a_t = +1 (positive) or -1 (negative).
The cone {Σ λ_k f_k | λ_k ≥ 0} is non-negative on every satisfying assignment,
because each f_k ≥ 0 there. This is the soundness property.
Contrapositive: if Σ λ_k f_k(x) < 0 for all x, no satisfying assignment exists.
The optimization min_λ max_x Σ λ_k f_k(x) decomposes per variable:
max_x Σ_k λ_k f_k(x) = Σ_k λ_k b_k + Σ_t max(0, Σ_k λ_k a_{k,t})This is O(m × n) per Frank-Wolfe iteration — no 2^n enumeration.
The core observation: for two clauses sharing a variable in opposing polarity, their cone combination cancels that variable's coefficient.
f = -1 + x₁ + x₂ clause (x₁ ∨ x₂)
g = -x₁ + x₂ clause (¬x₁ ∨ x₂)
f + g = -1 + 2x₂ learned clause (x₂)The x₁ coefficient cancels: 1 + (-1) = 0. What remains is a constraint
on x₂ alone. This is resolution via the cone's algebra — matching weights on
opposing polarities zeros out the resolved variable.
General principle: Σ λ_k a_{k,t} = 0 for variable t means t is resolved out.
The surviving affine function encodes a clause on the remaining variables.
The LP doesn't just certify UNSAT — it reveals which variable the adversary exploits.
The variable with the largest positive coefficient Σ λ_k a_{k,t} is the adversary's
best escape route.
Force it the other way. Then BCP propagates. The reduced formula has fewer variables. Repeat.
| Instance | n | m | Rounds | Forced | Time |
|---|---|---|---|---|---|
| x ∧ ¬x | 1 | 2 | 0 | 1 | 0.00s |
| All-signs 2-var | 2 | 4 | 1 | 2 | 0.02s |
| PHP(3,2) | 6 | 9 | 1 | 6 | 0.07s |
| PHP(4,3) | 12 | 22 | 2 | 11 | 0.36s |
| PHP(5,4) | 20 | 45 | 3 | 18 | 1.28s |
| Tseitin(4) | 5 | 12 | 2 | 5 | 0.12s |
| Tseitin(5) | 8 | 24 | 4 | 8 | 0.46s |
| Random 3-SAT n=20 | 20 | 100 | 3 | 14 | 3.3s |
| Random 3-SAT n=50 | 50 | 250 | 9 | 49 | 57s |
The cascade is not DPLL (it doesn't backtrack) and not resolution (it doesn't derive new clauses in the traditional sense). It uses the cone's global affine structure to identify the one decision that maximally constrains the solution space, then lets BCP handle the consequences.
Every point λ on the probability simplex gives a cone combination
h = Σ λ_k f_k that encodes an implied clause. Random sampling
explores the space of implied clauses at ~70K samples/second.
From a 30-clause 8-variable formula: 881 unique implied clauses in 2 seconds, including 7 ternary clauses not in the original formula.
The combination h(x) = const + Σ coeff_t x_t refutes assignments
where h(x) < 0. The strongest refutation occurs at
x_min = {x_t = 1 iff coeff_t < 0}:
h_min = const + Σ_{coeff_t < 0} coeff_tA good heuristic maximizes |const| relative to the number of
positive "escape routes" — variables the adversary can turn on to
push h above zero. Each iteration of the LP eliminates escape routes
by canceling variable coefficients, tightening the learned constraint.