Charles Dana — Monce SAS, 2026
We present a polynomial-time reduction from arbitrary CNF to uniform 3-SAT that preserves equisatisfiability while producing a structurally regular instance. The reduction comprises two stages: (1) standard Tseitin/splitting to 3-SAT, and (2) BCP-guided derivation of implied 3-clauses that balance variable frequency. Empirically, the uniform output is solved 2–30x faster by CDCL solvers on structured instances, with the speedup growing superlinearly with instance hardness.
SAT solvers exploit structural regularity. Random instances at the phase transition are hard; highly structured instances (pigeonhole, graph coloring) are hard for different reasons — unbalanced variable frequency creates deep, asymmetric search trees.
Our observation: if we can transform a structured instance into one with uniform variable statistics while preserving solutions, we remove the structural asymmetry that causes exponential blowup in CDCL branching.
A CNF formula F is uniform 3-SAT if every clause has exactly 3 literals, and for every variable x, |pos(x) - neg(x)| ≤ δ and |occ(x) - occ(y)| ≤ δ for all variables x, y, where δ = O(√n).
Standard Tseitin transformation for long clauses (width > 3), auxiliary padding for short clauses (width 1–2). This is O(n) in clause count.
For each candidate 3-clause C over active variables: assume ¬C (negate all literals), run unit propagation on the current formula. If contradiction is derived, C is a logical consequence — add it. Time-bounded to 180ms.
Every clause in the output is a logical consequence of the input formula. The output is equisatisfiable with the input.
The reduction runs in O(n² · m) time where n = variables, m = clauses. In practice, bounded to 180ms by the BCP budget.
| Instance | Original (Kissat) | Uniform (Kissat) | Speedup |
|---|---|---|---|
| PHP(9,8) | 50.8 ms | 35.3 ms | 1.4x |
| PHP(10,9) | 182.9 ms | 72.6 ms | 2.5x |
| PHP(11,10) | 1,195.7 ms | 145.9 ms | 8.2x |
| PHP(12,11) | 31,913.3 ms | 1,049.0 ms | 30.4x |
| Rand(250, r=4.26) | 84.7 ms | 33.2 ms | 2.5x |
The speedup is superlinear in instance hardness. On PHP, the original solve time grows exponentially while the uniform version grows polynomially in the measured range.
The BCP-derived clauses are resolution lemmas that the solver would eventually discover through conflict-driven learning. By pre-computing them and embedding them in the formula, we eliminate exponential search on the critical path. The uniform topology ensures VSIDS branching doesn't get trapped in deep asymmetric subtrees.
The monce-optimization library reduces locally (zero network cost) and forwards only the uniform DIMACS to npdollars for budget-aware solving. This separation keeps the reduction fast and the solving scalable.