clauseUnit
plain-language theorem explainer
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.
Claim. Let $σ : 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.