IPASIR-UP: User Propagators for CDCL
summary
Proposes a minimal standardized extension to IPASIR called IPASIR-UP interface that exposes four notifications and five callbacks to inspect and influence CDCL search; extends CaDiCaL (CaDiCaL extended) to support lazy user propagations, delayed explanations, and frozen variables for in‑processing. Tests include symmetry‑aware graph enumeration (avoids exponential clauses and produces ~12 million graphs quickly) and replacing MiniSAT inside cvc5, yielding significant speedups and more solved SMT instances. Future work focuses on representing trusted external clauses and incremental in‑processing proofs.
AI-written summary · about
chapters (10)
- 0:00Start
- 0:44Usual Use of SAT Solvers
- 2:06Usual Use of Incremental SAT Solvers
- 4:05Interactive Incremental SAT Solving
- 5:51IPASIR-UP: A New Interface for Interactive CDCL
- 8:01IPASIR-UP: IPASIR with User Propagators
- 10:09CDCL with IPASIR-UP - Example
- 23:28IPASIR-UP for SAT modulo Symmetries - Example
- 24:40IPASIR-UP for Satisfiability Modulo Theories - cvc5
- 26:34Summary
related talks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
24mBuilding Information Modeling Using Constraint Logic Programming (Extended Ab...
41mImplementing Piped Processing Language in OpenSearch Via Apache Calcite
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
19mProof Automation for Linearizability in Separation Logic
15mAutomatic Synthesis of Data-Flow Analyzers
26mCoMPAS Essentials: Key To Simplicity
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community