known_lit_false''
The lemma shows that a literal known to be false under a compatible partial assignment σ remains false when evaluated under the full assignment a. Researchers formalizing unit propagation in SAT solvers cite this helper when proving backpropagation correctness. The tactic proof cases on literal polarity, invokes compatibility to equate the known value with evalLit a l, then matches on the Option to conclude from the false hypothesis.
claimLet $n$ be a natural number, let $σ$ be a partial assignment on $n$ variables, and let $a$ be a total assignment on the same variables. Suppose $σ$ and $a$ are compatible, the value of literal $l$ under $σ$ is defined, and that value equals false. Then the evaluation of $l$ under $a$ equals false.
background
PartialAssignment n is the type Var n → Option Bool, where none marks an unknown bit and some b a determined Boolean value. The predicate compatible σ a asserts that for every variable v, either σ v = some (a v) or σ v = none, so the partial assignment agrees with the total assignment wherever it is defined. valueOfLit σ l returns the Option Bool obtained by applying the literal's polarity to the partial map at its variable. The module models backward propagation over CNF formulas with XOR constraints, using these partial maps to track determined literals during search.
proof idea
The proof first constructs an equality valueOfLit σ l = some (evalLit a l) by cases on the literal constructor (pos or neg). For each case it performs rcases on the compatibility hypothesis for the underlying variable, then simplifies with the known-value assumption to obtain the equality. It next cases on the actual valueOfLit result: the none branch contradicts hsome, while the some branch rewrites hfalse and the equality to finish with rw on the false value.
why it matters in Recognition Science
This helper feeds directly into the parent theorem clauseUnit_correct, which states that clauseUnit returns the correct variable-value pair for any satisfying assignment. It closes a formerly axiomatic step in the backpropagation correctness argument for the SAT encoding. The result sits inside the Complexity.SAT.Backprop module and supports the larger RSatEncoding machinery used to embed constraint problems into the Recognition Science framework.
scope and limits
- Does not treat literals whose value remains unknown under σ.
- Does not assume a satisfies the containing clause.
- Does not extend to clauses with multiple unknown literals.
- Does not invoke the XOR-specific valueOfXOR function.
formal statement (Lean)
277private lemma known_lit_false'' {n} (σ : PartialAssignment n) (a : Assignment n) (l : Lit n)
278 (hcompat : compatible σ a) (hsome : (valueOfLit σ l).isSome)
279 (hfalse : (valueOfLit σ l).getD false = false) :
280 evalLit a l = false := by
proof body
Tactic-mode proof.
281 have heq : valueOfLit σ l = some (evalLit a l) := by
282 cases l with
283 | pos v =>
284 simp only [valueOfLit, evalLit] at *
285 rcases hcompat v with h | h
286 · exact h
287 · simp [h] at hsome
288 | neg v =>
289 simp only [valueOfLit, evalLit, Option.map] at *
290 rcases hcompat v with h | h
291 · simp [h]
292 · simp [h] at hsome
293 cases hv : valueOfLit σ l with
294 | none => simp [hv] at hsome
295 | some b =>
296 simp only [hv, Option.getD_some] at hfalse heq
297 simp only [Option.some.injEq] at heq
298 rw [← heq, hfalse]
299
300/-- **PROVED**: clauseUnit produces the correct value for a satisfying assignment.
301 If exactly one literal is unknown in clause C, all known literals are false,
302 and a satisfies C, then the value returned by clauseUnit equals a v.
303
304 **Mathematical justification**: A clause is satisfied iff at least one literal is true.
305 If all known literals are false under a (by compatibility), and a satisfies C,
306 then the unknown literal must be the satisfying one.
307 - For .pos v: the literal is true iff a v = true
308 - For .neg v: the literal is true iff a v = false
309
310 **Status**: PROVED (formerly axiom) -/