The Choice Construct in the Soufflé Language
summary
Implements a relation-based choice extension to the Soufflé Datalog engine that enforces functional dependencies on relations, emitting an existence-check (using Soufflé’s B-tree existence check) in RAM before insertions and compiling to C++. Applies to worklist tasks like rooted spanning tree over specCPU-derived CFGs, reducing a 157-line native encoding to 3–5 LOC and yielding up to 10k× faster runs and constant memory use; relation- and rule-based choices are equally expressive and show no significant performance gap.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:17Soufflé
- 2:35Motivating Example: Rooted Spanning Tree
- 3:12Stratified Datalog Solution
- 3:58Datalog with Choice Construct
- 5:41Relation based Choice Syntax
- 6:54Rule-based Choice
- 8:20Expressive Power
- 9:10Implementing Relation-based Choice in Souttle
- 9:55RAM Representation
- 11:24Experiments
- 12:15Root Spanning Tree with Real World CFGS
- 13:19Classic Non-deterministic Algorithms in Datalog
- 13:45Experience Report
related talks
15mUniversal Scalability in Declarative Program Analysis (with Choice-Based Combination(…)
19mMaking Formulog Fast: An Argument for Unconventional Datalog Evaluation
45mProblem Solved! Using Logic Programming to Find Answers
17mBring Your Own Data Structures to Datalog
41mOptimizing Relational Programs I
26mDebugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
17mInteractive Debugging of Datalog Programs
17mBetter Together: Unifying Datalog and Equality Saturation