UniqueSolution
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.