clauseUnit
clauseUnit returns the variable and forced boolean value for a clause when exactly one literal remains unknown under a partial assignment and all known literals evaluate to false. Researchers implementing unit propagation inside SAT backpropagation or constraint solvers cite it to extract forced literals during single-step updates. The definition evaluates literals via valueOfLit, filters the unknown set, and returns the polarity-adjusted pair only on the length-one plus all-false guard.
claimLet $σ : Var_n → Option(Bool)$ be a partial assignment and $C$ a clause whose literals are pairs of variable indices and signs. Then clauseUnit$(σ, C)$ yields some$(v, b)$ if and only if exactly one literal of $C$ is unknown under $σ$ and every known literal evaluates to false; here $v$ is the variable of that literal and $b$ is the boolean that satisfies it (true for a positive literal, false for a negative literal).
background
PartialAssignment n is the type Var n → Option Bool, with none marking an undetermined variable and some b a fixed value. valueOfLit lifts this map to literals by returning the stored boolean for a positive literal and its negation for a negative literal. The module defines backpropagation states over CNF formulas augmented by XOR constraints, using these partial assignments to propagate forced values one clause or constraint at a time.
proof idea
The definition maps valueOfLit across the clause to obtain vals, zips the clause with vals, and retains only the unknown pairs. It then tests whether the unknown list has length one and whether every known value is false. On success it extracts the single unknown literal, matches its constructor to decide the returned boolean, and packages the variable with that boolean; every other case yields none.
why it matters in Recognition Science
clauseUnit supplies the concrete rule for the clause-unit case inside the BPStep inductive relation. Its output is shown to agree with any satisfying assignment in the downstream theorem clauseUnit_correct, which in turn feeds the soundness lemma bp_step_sound that preserves compatibility with models. The definition therefore closes the unit-propagation step required for the backpropagation soundness argument in the SAT module.
scope and limits
- Does not return a value when zero or more than one literal is unknown.
- Does not inspect XOR constraints or the full CNF.
- Returns none for already-satisfied or already-falsified clauses.
- Assumes the input clause obeys the size bound of the Clause structure.
Lean usage
match clauseUnit σ C with | some (v, b) => setVar σ v b | none => σformal statement (Lean)
66def clauseUnit {n} (σ : PartialAssignment n) (C : Clause n) : Option (Var n × Bool) :=
proof body
Definition body.
67 let vals := C.map (valueOfLit σ)
68 let unknowns := C.zip vals |>.filter (fun ⟨_, o⟩ => o.isNone)
69 if h1 : unknowns.length = 1 then
70 if (vals.filter Option.isSome).all (fun o => o.getD false = false) then
71 let l := unknowns.get ⟨0, by omega⟩
72 match l.fst with
73 | .pos v => some (v, true)
74 | .neg v => some (v, false)
75 else none
76 else none
77
78/-- A (single) backpropagation step relation with guarded rules. -/