PartialAssignment
plain-language theorem explainer
PartialAssignment n maps each of n variables to none (undetermined) or some Bool (fixed value). Researchers analyzing unit propagation and backtracking in SAT solvers cite this as the core type for incomplete assignments. It is introduced by a direct type abbreviation with no proof content.
Claim. A partial assignment over $n$ variables is a map from the set of variable indices to the option type of booleans, where each index may be marked unknown or assigned a definite truth value.
background
The module defines backpropagation over CNF formulas that may include XOR clauses. CNF is the structure holding a list of clauses, while Var n is the type Fin n of variable indices. PartialAssignment n therefore extends the basic variable indexing by allowing each index to carry either no information or a concrete boolean. This choice supports incremental refinement during propagation steps without committing to a full assignment upfront.
proof idea
The declaration is a one-line abbreviation that directly equates PartialAssignment n with the function type Var n → Option Bool. No lemmas or tactics are invoked; the definition simply re-uses the imported Var abbreviation from the CNF module.
why it matters
It supplies the assignment component inside BPState and is referenced by clauseUnit, compatible, and sixteen other declarations that implement unit-clause detection and consistency checks. The structure therefore forms the data backbone for the entire backpropagation development, enabling later theorems such as clauseUnit_correct that relate partial and total assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.