Universal Scalability in Declarative Program Analysis (with Choice-Based Combination(…)
summary
Uses the choice construct in Souffle to enforce multiplicity bounds by hashing an extra index field, letting relations be pruned when a projected key exceeds a programmer-set cap. Applies with tiny, local edits to large frameworks Doop (Java bytecode) and Gigahorse (Ethereum analyses), yielding dramatic speedups—up to ~57x (average ~23x, authors report >20x on hardest inputs)—with modest completeness loss (example: reachability drops ~63%→59–60%) and added nondeterminism.
AI-written summary · about
chapters (13)
- 0:00Universal scalability intro
- 0:43What is Datalog?
- 2:09Scalability challenges
- 3:31Pruning for scalability
- 4:17Choice construct in Soufflé
- 5:19ChoiceBound core idea
- 7:45Adopting ChoiceBound
- 8:49Exploring ChoiceBound configs
- 9:30ChoiceBound evaluation
- 11:18Summary of findings
- 12:01Q&A on soundness
- 13:07Comparison with Answer Set Programming
- 14:34Closing remarks
related talks
15mThe Choice Construct in the Soufflé Language
41mOptimizing Relational Programs I
13mAccelerating Program Analyses in Datalog by Merging Library Facts
17mBring Your Own Data Structures to Datalog
26mDebugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
17mBetter Together: Unifying Datalog and Equality Saturation
19mMaking Formulog Fast: An Argument for Unconventional Datalog Evaluation
45mProblem Solved! Using Logic Programming to Find Answers