From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
Abstract
Given a set of candidate Datalog rules, the Datalog synthesis-as-rule-selection problem chooses a subset of these rules that satisfies a specification (such as an input-output example). Building off prior work using counterexample-guided inductive synthesis, we present a progression of three solver-based approaches for solving Datalog synthesis-as-rule-selection problems. Two of our approaches offer some advantages over existing approaches, and can be used more generally to solve arbitrary SMT formulas containing Datalog predicates; the third—an encoding into standard, off-the-shelf answer set programming (ASP)—leads to significant speedups (∼ 9× geomean) over the state of the art while synthesizing higher quality programs.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 09, 2023
- Source ID
- 10.1145/3571200
Entities
People
- Aaron Bembenek
- Michael Greenberg
- Stephen Chong
Organizations
- Defense Advanced Research Projects Agency
- Harvard University
- Stevens Institute of Technology