Cone: SAT Analysis via Linear Algebra

Charles Dana — Berkeley 2023, rebuilt April 2026 — Paper · API docs

Clause → affine function. Cone combination → resolution. LP → variable forcing.

The idea: Map each clause to f_k(x) = -1 + Σ literal_values. The linear cone {Σ λ_k f_k | λ_k ≥ 0} is non-negative on satisfying assignments. Three tools built on this:

Cascade — LP identifies the weakest variable, forces it, BCP propagates. Repeat.
Resolution — (x₁∨x₂) + (¬x₁∨x₂) → (x₂). Cancel variables via weight matching.
Mining — 135K random cone samples in 2s. Each sample extracts an implied clause.

Try it

Paste a CNF in DIMACS format:

Presets

Results

Cone Cascade (LP → force → BCP)

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(5)	8	24	4	8	0.46s
Random n=50	50	250	9	49	57s

Resolution via Cone

Instance	Status	Rounds	Learned
(x₁∨x₂) + (¬x₁∨x₂)	learns (x₂)	1	1
All-signs 2-var	UNSAT	1	4
PHP(3,2)	UNSAT	3	63

Random Cone Mining (2s budget)

Instance	Samples	Mined	3-SAT	4-SAT	5-SAT
Random 8-var 30-clause	135K	881	7	59	208

Each random λ on the simplex gives a different cone combination encoding a different implied clause.

How it works

Clause function: (x₁ ∨ ¬x₂ ∨ x₃) → f(x) = -1 + x₁ + (1-x₂) + x₃

f(x) ≥ 0 iff clause satisfied. f(x) = -1 when no literal true.

Cone property: Σ λ_k f_k ≥ 0 on satisfying assignments (λ_k ≥ 0).

Resolution: λf + μg cancels shared variable when opposing polarities match. What remains is a constraint on the surviving variables.

Cascade: The LP min_λ max_x Σ λ_k f_k(x) decomposes per variable: O(m × n). No 2^n enumeration. Frank-Wolfe converges in O(1/t). The optimal λ reveals which variable the adversary exploits most — force it, BCP cascade.

API

# Cascade: LP-guided variable forcing + BCP
curl -X POST https://cone.aws.monce.ai/cascade \
  -H "Content-Type: application/json" \
  -d '{"dimacs": "p cnf 2 4\n1 2 0\n-1 2 0\n1 -2 0\n-1 -2 0"}'

# Resolution: cancel variables via cone algebra
curl -X POST https://cone.aws.monce.ai/resolve \
  -H "Content-Type: application/json" \
  -d '{"dimacs": "p cnf 2 2\n1 2 0\n-1 2 0"}'

# Mining: random cone sampling (2s budget)
curl -X POST https://cone.aws.monce.ai/mine \
  -H "Content-Type: application/json" \
  -d '{"dimacs": "p cnf 4 6\n1 2 0\n-1 3 0\n-2 4 0\n-3 -4 0\n1 -3 0\n-1 -4 0"}'

Cone v0.1.0 — Zero dependencies. Pure Python.
Charles Dana & Claude Opus 4.6 — cone.aws.monce.ai