UniqueSolution
UniqueSolution defines the predicate asserting that a CNF formula over n variables has exactly one satisfying assignment. Researchers analyzing unique-SAT instances or reductions in complexity would reference this predicate. It is realized as a direct one-line encoding of the unique existence quantifier applied to the CNF evaluation map.
claimFor a CNF formula $φ$ with $n$ variables, UniqueSolution($φ$) holds precisely when there exists a unique assignment $a$ from the $n$ variables to Boolean values such that the conjunction of all clauses evaluates to true under $a$.
background
CNF formulas are structures consisting of a list of clauses over $n$ variables, where variable indices are Fin $n$ for a fixed problem size. An assignment maps each variable to a Boolean value. The evaluation function checks whether every clause is satisfied, returning true when the clause list is empty.
proof idea
The definition is a direct abbreviation that applies the unique existence quantifier to the predicate that evalCNF returns true.
why it matters in Recognition Science
This predicate supplies the formal notion of unique satisfiability inside the SAT encoding layer. No downstream theorems currently depend on it, so it functions as a standalone building block for potential complexity reductions or solver analyses within the module.
scope and limits
- Does not compute or enumerate the unique assignment.
- Does not extend to formulas with infinitely many variables.
- Does not link to J-cost, phi-ladder, or core Recognition Science forcing chain.
- Does not establish existence or uniqueness for concrete CNF instances.
formal statement (Lean)
45def UniqueSolution {n} (φ : CNF n) : Prop :=
proof body
Definition body.
46 ∃! (a : Assignment n), evalCNF a φ = true
47
48end SAT
49end Complexity
50end IndisputableMonolith