Propagators
summary
Defines propagators as monotone functions between join-semilattices and proves termination and deterministic results under simple sufficient conditions like finite height and the ascending chain condition, so scheduling and partitioning no longer matter. Pulls optimizations from SAT and LVars — threshold reads, two‑watched literals, inflationary writes, decomposed reads — and adds a practical trick: use group actions to relocate whole packs of propagators for O(1) updates. Implements examples (elvish LVars, guanxi nondeterministic propagators, incremental parsing, maps with O(1) relocation) and catalogs ~172 domains that fit.
AI-written summary · about
chapters (13)
- 0:00Start
- 2:57Hasse Diagrams
- 3:48Power Sets
- 5:45Monotonicity
- 5:58What is a Propagator?
- 8:00Naive Propagation
- 12:48Promises, Promises
- 18:13The Problem with L-Vars
- 20:47Breaking Apart L-Vars
- 20:59Building the Primitives
- 21:34SAT Solving
- 23:54n-Watched Literal Wake-Up
- 25:53Constraint Programming
related talks
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
19mFunctional Meaning for Parallel Streaming
28mLiveness to Safety for Distributed Systems
31mCompositional Verification of Stigmergic Collective Systems
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
21mMonotone Procedure Summarization via Vector Addition Systems and Inductive Potentials
25mProperty-agnostic base case extension for scalable verification of distributed systems
15mProducts of Recursive Programs for Hypersafety Verification