Uniform 3-SAT — Universal NP Reduction

Pipeline

Any k-CNF

→

Tseitin 3-SAT

→

BCP derivation

→

Uniform 3-SAT

Structural clauses preserve equisatisfiability. Derived clauses are BCP-proven logical consequences — the isomorphic restatement. Solution decode maps back through the variable map: same solution set, different topology.

Try it

Solution Set Isomorphism

Original -

Reduced (decoded) -

Uniform 3-SAT output

API

POST /reduce
{ "dimacs": "p cnf 5 3\n1 2 3 4 5 0\n...", "seed": 0 }

→ { "dimacs", "stats", "mapping" }

# Local verification (pip install uniform-3sat)
from uniform_3sat import reduce, verify
from uniform_3sat.problems import sudoku

result = reduce(sudoku("53..7....6..195..."))
report = verify(sudoku("53..7....6..195..."), solver="kissat")
print(report.sound)  # True

Documentation

Paper Architecture Economics