clauseUnit_correct
plain-language theorem explainer
The clauseUnit_correct theorem shows that if a partial assignment is compatible with a full satisfying assignment for a clause and clauseUnit identifies a unit literal, then the returned boolean matches the assignment's value for that variable. Complexity researchers applying backpropagation to SAT instances within Recognition Science models would cite this to validate propagation soundness. The proof uses case splitting on the filtered unknowns list, singleton extraction, and contradiction via known false literals to isolate the satisfying one
Claim. Let $σ : Var n → Option Bool$ be a partial assignment, $a : Fin n → Bool$ a full assignment, $C$ a clause, $v$ a variable and $b$ a boolean. If $σ$ is compatible with $a$, $a$ satisfies $C$, and clauseUnit($σ$, $C$) returns some($v$, $b$), then $b = a(v)$.
background
PartialAssignment is the type Var n → Option Bool, with none marking unknown values and some b marking determined ones. Clause is the structure from RSatEncoding whose literals field holds at most three signed variable indices. The module setting is backpropagation over CNF formulas augmented with XOR constraints, tracking determined values during solving steps.
proof idea
The tactic proof unfolds clauseUnit, splits on the length-1 filter and the all-known-false check, obtains the singleton via singleton_eq_get_zero', proves known literals evaluate false under a using known_lit_false'', extracts the satisfying literal from evalClause, shows it must be the unknown entry, and matches the returned pair by case analysis on positive versus negative literal.
why it matters
The result is invoked by bp_step_sound to establish that each propagation step preserves compatibility with any satisfying assignment, and pairs with xorMissing_correct for the XOR case. It supplies the unit-clause correctness obligation inside the SAT backprop module, closing a formerly axiomatic step in the solver soundness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.