From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Se...
summary
Presents a progression of four solver implementations — prosynth, monosynth, loopsynth, and ASPsynth — that move from CEGIS with provenance to a custom monotonic SMT theories plugin for Z3/cvc4, a SAT encoding with loop formulas, and finally an off‑the‑shelf answer set programming encoding. Shows ASPsynth combining search and Horn solving in one solver, avoiding repeated interactions and achieving about a 9× geomean speedup over the prior state of the art while supporting minimal solutions; grounding can limit scale for very large grounded programs.
AI-written summary · about
chapters (8)
- 0:00Solver-based Datalog synthesis
- 2:09Datalog synthesis problem
- 4:55ProSynth prior approach
- 6:41MonoSynth SAT with Datalog
- 9:30LoopSynth SAT with loops
- 14:06ASP-Synth answer set programming
- 17:56Conclusion and future
- 19:12Q&A
related talks
45mProblem Solved! Using Logic Programming to Find Answers
41mOptimizing Relational Programs I
01h 24mIntroduction to Constraint Logic Programming
28mSolving Vehicle Equipment Specification Problems with Answer Set Programming
25mSmart Devices and Large Scale Reasoning via ASP: Tools and Applications
19mMaking Formulog Fast: An Argument for Unconventional Datalog Evaluation
13mAccelerating Program Analyses in Datalog by Merging Library Facts
05mRelational Programming