valueOfLit
plain-language theorem explainer
valueOfLit evaluates a literal under a partial assignment by direct lookup on positive variables and negation on negative ones. SAT solver designers and complexity researchers cite it when implementing unit propagation or clause evaluation routines. The definition proceeds by exhaustive pattern matching on the two constructors of the Lit inductive type.
Claim. Let $n$ be a natural number and let $σ : Var_n → Option(Bool)$ be a partial assignment. For a literal $ℓ$, define $valueOfLit(σ, ℓ) = σ(v)$ when $ℓ = pos(v)$ and $valueOfLit(σ, ℓ) = ¬(σ(v))$ when $ℓ = neg(v)$.
background
PartialAssignment n is the abbreviation Var n → Option Bool, where none marks an undetermined variable and some b records a fixed boolean value. The Lit type is the inductive datatype with constructors pos v and neg v for each variable v. The module models backpropagation over CNF formulas that may also contain XOR constraints, using these partial maps to track known literals during search.
proof idea
The definition is a direct pattern match on the Lit inductive type. The pos case returns the value stored in σ v; the neg case applies Option.map not to the same stored value.
why it matters
valueOfLit supplies the primitive literal evaluator required by valueOfClause and clauseUnit. Those definitions in turn support the unit-propagation step whose correctness is stated in clauseUnit_correct. Within the Recognition Science setting the construction supplies a concrete mechanism for constraint propagation that can be compared with the forcing chain and composition laws developed elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.