Extended Magic for Negation: Efficient Demand-Driven Evaluation of Stratified Datalog with Precise Complexity Guarantees

TL;DR

This paper introduces a demand-driven evaluation method for stratified Datalog with negation, ensuring precise complexity guarantees and optimal performance by handling non-stratified negation resulting from transformations.

Contribution

It extends demand transformation and bottom-up evaluation techniques to support stratified negation in Datalog, maintaining complexity guarantees and efficiency.

Findings

Method provides precise complexity guarantees.

Evaluation is optimal with constant-time rule firing.

Experimental results demonstrate performance improvements.

Abstract

Given a set of Datalog rules, facts, and a query, answers to the query can be inferred bottom-up starting from the facts or top-down starting from the query. For efficiency, top-down evaluation is extended with memoization of inferred facts, and bottom-up evaluation is performed after transformations to make rules driven by the demand from the query. Prior work has shown their precise complexity analysis and relationships. However, when Datalog is extended with even stratified negation, which has a simple and universally accepted semantics, transformations to make rules demand-driven may result in non-stratified negation, which has had many complex semantics and evaluation methods. This paper presents (1) a simple extension to demand transformation, a transformation to make rules demand-driven for Datalog without negation, to support stratified negation, and (2) a simple extension to an optimal bottom-up evaluation method for Datalog with stratified negation, to handle non-stratified negation in the resulting rules. We show that the method provides precise complexity guarantees. It is also optimal in that only facts needed for top-down evaluation of the query are inferred and each firing of a rule to infer such a fact takes worst-case constant time. We extend the precise relationship between top-down evaluation and demand-driven bottom-up evaluation to Datalog with stratified negation. Finally, we show experimental results for performance, as well as applications to previously challenging examples.