A Linear Algebraic Approach to Datalog Evaluation
Taisuke Sato

TL;DR
This paper introduces a novel linear algebraic method for evaluating Datalog programs by translating logical clauses into matrix equations, enabling efficient computation of models with potential speedups over symbolic systems.
Contribution
It presents a new approach that converts Datalog evaluation into linear algebra problems, achieving O(N^3) complexity for certain program classes and demonstrating significant performance improvements.
Findings
Achieves O(N^3) time complexity for specific program classes.
Runs 10 to 10,000 times faster than symbolic systems on certain datasets.
Successfully computes transitive closures on real network data.
Abstract
In this paper, we propose a fundamentally new approach to Datalog evaluation. Given a linear Datalog program DB written using N constants and binary predicates, we first translate if-and-only-if completions of clauses in DB into a set Eq(DB) of matrix equations with a non-linear operation where relations in M_DB, the least Herbrand model of DB, are encoded as adjacency matrices. We then translate Eq(DB) into another, but purely linear matrix equations tilde_Eq(DB). It is proved that the least solution of tilde_Eq(DB) in the sense of matrix ordering is converted to the least solution of Eq(DB) and the latter gives M_DB as a set of adjacency matrices. Hence computing the least solution of tilde_Eq(DB) is equivalent to computing M_DB specified by DB. For a class of tail recursive programs and for some other types of programs, our approach achieves O(N^3) time complexity irrespective of the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Formal Methods in Verification
