clauseUnit_correct
clauseUnit_correct establishes that if a partial assignment leaves exactly one literal unknown in clause C, all known literals evaluate false under a compatible full assignment a, and a satisfies C, then clauseUnit returns the pair (v, b) with b matching a(v). Researchers building backpropagation SAT solvers or verifying complexity reductions in Recognition Science cite it for propagation soundness. The proof filters the unknown list to a singleton, shows the satisfying literal must be that unknown entry, and performs polarity case analysis to
claimLet $n$ be a natural number, let $σ$ be a partial assignment over $n$ variables, let $a$ be a full assignment compatible with $σ$, let $C$ be a clause satisfied by $a$, and suppose clauseUnit$(σ, C)$ returns some pair $(v, b)$. Then $b = a(v)$.
background
PartialAssignment $n$ is the type Var $n$ → Option Bool, where none marks an undetermined variable and some $b$ records a fixed Boolean value. Clause $n$ is a structure holding a list of at most three literals, each a pair (variable index, polarity). The clauseUnit function maps a partial assignment and clause to an optional (variable, Boolean) pair precisely when exactly one literal remains unknown and every known literal is false under the assignment.
proof idea
The tactic proof unfolds clauseUnit, splits on the length of the filtered unknown list equaling one, obtains the singleton element via singleton_eq_get_zero', proves all known literals are false using known_lit_false'', extracts the satisfying literal from the assumption evalClause $a$ $C$ = true, shows that literal must be the unknown entry, and finishes by case analysis on the literal's polarity (pos or neg) to equate $b$ with $a(v)$ or its negation.
why it matters in Recognition Science
The result supplies the key correctness step for unit propagation inside the backpropagation module and is invoked by bp_step_sound to preserve compatibility after each step. It replaces a former axiom, completing the deterministic justification that clauseUnit recovers the correct value from any satisfying assignment. The lemma sits in the Complexity.SAT layer that supports the broader Recognition Science reduction of satisfiability questions to the phi-ladder and eight-tick structure.
scope and limits
- Does not prove that every satisfiable CNF contains a unit clause under the partial assignment.
- Does not apply when two or more literals remain unknown.
- Does not treat XOR constraints (see xorMissing_correct).
- Does not establish termination or completeness of the full backpropagation procedure.
Lean usage
have hb : b = a v := clauseUnit_correct σ a C v b hcompat hsat hmissformal statement (Lean)
311theorem clauseUnit_correct {n} (σ : PartialAssignment n) (a : Assignment n) (C : Clause n)
312 (v : Var n) (b : Bool)
313 (hcompat : compatible σ a)
314 (hsat : evalClause a C = true)
315 (hmiss : clauseUnit σ C = some (v, b)) :
316 b = a v := by
proof body
Tactic-mode proof.
317 unfold clauseUnit at hmiss
318 simp only at hmiss
319
320 split at hmiss
321 case isFalse h => simp at hmiss
322 case isTrue h_len1 =>
323 split at hmiss
324 case isFalse h => simp at hmiss
325 case isTrue h_all_false =>
326 -- Set up unknowns
327 set unknowns := (C.zip (C.map (valueOfLit σ))).filter (fun ⟨_, o⟩ => o.isNone) with hunk_def
328 have h_len1' : unknowns.length = 1 := h_len1
329
330 -- Get the singleton element
331 obtain ⟨unk, h_singleton, hunk_get⟩ := singleton_eq_get_zero' unknowns h_len1'
332
333 -- Known literals are false
334 have h_known_false : ∀ l ∈ C, (valueOfLit σ l).isSome → evalLit a l = false := by
335 intro l hl_in hsome
336 have hval_in : valueOfLit σ l ∈ (C.map (valueOfLit σ)).filter Option.isSome := by
337 simp only [List.mem_filter, List.mem_map]
338 exact ⟨⟨l, hl_in, rfl⟩, hsome⟩
339 rw [List.all_eq_true] at h_all_false
340 simp only [decide_eq_true_eq] at h_all_false
341 exact known_lit_false'' σ a l hcompat hsome (h_all_false _ hval_in)
342
343 -- Some literal is true
344 rw [evalClause, List.any_eq_true] at hsat
345 obtain ⟨l_sat, hl_in, hl_true⟩ := hsat
346
347 -- l_sat must be unknown
348 have hl_unknown : (valueOfLit σ l_sat).isNone := by
349 rw [← not_isSome_iff_isNone']
350 intro hsome
351 have hfalse := h_known_false l_sat hl_in hsome
352 rw [hl_true] at hfalse
353 cases hfalse
354
355 -- l_sat is in unknowns
356 have hl_in_unk : (l_sat, valueOfLit σ l_sat) ∈ unknowns := by
357 rw [hunk_def, List.mem_filter]
358 constructor
359 · have hlen : C.length = (C.map (valueOfLit σ)).length := by simp
360 obtain ⟨i, hi, hget⟩ := List.mem_iff_getElem.mp hl_in
361 have hi2 : i < (C.map (valueOfLit σ)).length := by simp; omega
362 have hmem := mem_zip_of_getElem' C (C.map (valueOfLit σ)) i hi hi2
363 simp only [List.getElem_map, hget] at hmem
364 exact hmem
365 · exact hl_unknown
366
367 -- Since unknowns = [unk], l_sat = unk.fst
368 rw [h_singleton, List.mem_singleton] at hl_in_unk
369 have hl_eq : l_sat = unk.fst := congrArg Prod.fst hl_in_unk
370
371 -- Rewrite hmiss using hunk_get
372 have hmiss' : (match unk.fst with
373 | .pos v => some (v, true)
374 | .neg v => some (v, false)) = some (v, b) := by
375 convert hmiss using 2
376 rw [← hunk_get]
377
378 -- Case analysis on unk.fst
379 cases hl : unk.fst with
380 | pos w =>
381 simp only [hl] at hmiss'
382 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss'
383 obtain ⟨hv_eq, hb_eq⟩ := hmiss'
384 subst hv_eq hb_eq
385 rw [hl_eq, hl] at hl_true
386 simp only [evalLit] at hl_true
387 exact hl_true.symm
388
389 | neg w =>
390 simp only [hl] at hmiss'
391 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss'
392 obtain ⟨hv_eq, hb_eq⟩ := hmiss'
393 subst hv_eq hb_eq
394 rw [hl_eq, hl] at hl_true
395 simp only [evalLit, Bool.not_eq_true'] at hl_true
396 exact hl_true.symm
397-- ... 3 more lines elided ...