clauseUnit
plain-language theorem explainer
clauseUnit returns the forced variable and polarity for a clause when exactly one literal remains unknown under a partial assignment and all known literals evaluate to false. Researchers modeling unit propagation inside SAT backpropagation or CNF constraint propagation would cite this definition. The body maps literals to their values, filters the single unknown, and checks the all-false condition before extracting the candidate.
Claim. For partial assignment $σ : Var_n → Option(Bool)$ and clause $C$ (list of at most three literals), the function returns some$(v,b)$ exactly when precisely one literal of $C$ has unknown value under $σ$ and every known literal evaluates to false; $b$ is the polarity that satisfies the clause. Otherwise it returns none.
background
PartialAssignment n is the type Var n → Option Bool, with none marking an undetermined variable and some b a fixed truth value. valueOfLit maps a positive or negative literal to its Option Bool under such an assignment. Clause n packages a list of at most three literals together with a size bound. The module develops partial assignments for backpropagation over CNF formulas augmented by XOR constraints; the local setting treats none as unknown and some b as determined.
proof idea
The definition maps every literal of C through valueOfLit to obtain vals, zips with the literals and retains only the none entries to form unknowns. It then tests whether unknowns has length exactly one and whether every some entry in vals is false; if both hold it extracts the unique unknown literal and returns its variable together with the required polarity (true for positive, false for negative).
why it matters
clauseUnit supplies the clause-side unit rule that is invoked inside the inductive definition of BPStep and inside the soundness statement bp_step_sound. It is the key hypothesis of the proved theorem clauseUnit_correct, which shows that any satisfying assignment must agree with the returned value. The definition therefore closes one direction of the backpropagation soundness argument used to propagate forced literals in SAT encodings of physical constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.