compatible
plain-language theorem explainer
A definition stating that a partial assignment σ over n variables is compatible with a total assignment a exactly when σ agrees with a on every decided variable. Researchers formalizing backpropagation soundness for SAT instances in complexity reductions would cite this predicate when proving preservation under propagation steps. It is introduced directly as a universal quantification over variables with a disjunction on the Option type.
Claim. Let $σ$ be a partial assignment and $a$ a total assignment over $n$ variables. Then $σ$ is compatible with $a$ if and only if for every variable $v$, either $σ(v) = some(a(v))$ or $σ(v) = none$.
background
PartialAssignment is the type of maps from variables to Option Bool, with none marking unknown values and some b marking determined bits. Assignment (from both RSatEncoding and the local CNF module) is the type of total maps from variables to Bool. The module develops backpropagation over CNF formulas augmented with XOR systems, using these types to track determined literals during search.
proof idea
This is a definition, not a derived theorem. It directly encodes the agreement condition as the predicate ∀ v, σ v = some (a v) ∨ σ v = none. No lemmas or tactics are applied; the body is the primitive predicate consumed by later soundness results.
why it matters
The predicate is invoked in downstream lemmas including bp_step_sound (preservation of compatibility under a propagation step) and clauseUnit_correct (correctness of unit-clause inference under a satisfying assignment). It supplies the basic interface for partial information in the SAT backpropagation development, which in turn supports the PvsNPFromBIT certification and related complexity arguments within Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.