evalLit
plain-language theorem explainer
The evalLit definition computes the truth value of a positive or negated variable under a complete Boolean assignment to n variables. SAT complexity researchers cite it when reducing problems or proving propagation rules. It is realized by a simple pattern match on the literal's constructor.
Claim. Let $a$ be an assignment of Boolean values to $n$ variables. For a literal $l$, if $l$ is the positive literal on variable $v$ then evalLit$(a,l)=a(v)$; if $l$ is the negative literal on $v$ then evalLit$(a,l)=¬a(v)$.
background
Variable indices are Fin n for a given problem size. An Assignment n is the type of total functions Var n → Bool that supply truth values to each variable. A Lit n is an inductive type with constructors pos v and neg v for a variable v. This module builds directly on the Assignment definition from RSatEncoding, which uses the equivalent Fin n → Bool, together with the local Lit inductive.
proof idea
The definition is a direct pattern match on the Lit inductive type. The .pos case returns the assignment value; the .neg case returns its Boolean negation.
why it matters
This definition is invoked by evalClause to test clause satisfaction and appears in the proofs of clauseUnit_correct and known_lit_false'' in the Backprop module. Those results establish correctness of unit propagation for SAT solving. It supplies the basic literal evaluation step required for the CNF encoding layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.