Discrete-Continuous Duality
From SAT to Real Functions — Charles Dana, 2023
Each clause C maps to a real function via the encoding:
f_C(x) = -1 + Σ x_l[l>0](1 - x|l|)[l<0]
A SAT instance is satisfiable iff ∀f ∈ D, f(x) ≥ 0. The score heuristic:
S_k(f) = f(0) + Σ max(c_i, 0) - Σj=1..k |c*_j|
When S_k(f) < 0, a k-clause is implied. Addition of clause functions IS resolution in continuous space.
Try it
Paste a DIMACS CNF instance (or use the example):
API
POST /solve — JSON body: {"cnf": "...", "budget": 5, "max_k": 7}GET /paper — the original manuscript (PDF)GET /health — status check
How it works
- Clauses become real-valued linear functions with integer coefficients
- Addition of two clause functions = resolution in continuous space
- The score S_k detects when a combination implies a short clause
- The solver tries k=0 (UNSAT), k=1 (unit), k=2 (binary), ... up to max_k
- Learned clauses feed back into BCP, which may trigger further simplification