pith. sign in
module module high

IndisputableMonolith.Complexity.SAT.Backprop

show as:
view Lean formalization →

This module defines partial assignments and backpropagation states for SAT problems over CNF and XOR constraints. Researchers in formal SAT solving and Recognition Science complexity would cite it when building completeness arguments. It supplies the type definitions and update operations needed to track undetermined variables. The module is purely definitional with no theorems or proofs.

claimA partial assignment is a map from variables (indices in Fin n) to Option Bool, with none denoting an unknown value and some b a determined Boolean. BPState aggregates these assignments together with clause and XOR evaluations for incremental backpropagation steps.

background

The module imports the CNF setting in which variables are indexed by Fin n for a fixed problem size and the XOR setting that encodes parity constraints over subsets of those variables. It introduces PartialAssignment to represent incomplete knowledge during search, with the explicit convention that none stands for undetermined and some b for a fixed Boolean. BPState and the associated update functions (setVar and evaluation helpers) then track how partial information propagates through clauses and XORs.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supplied here are imported by the Completeness module, which constructs a fully-determined backpropagation state from any total assignment. This supplies the partial-assignment layer required for the SAT completeness argument in the Recognition Science framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (31)