An Advanced Disjunctive Magic-Set Method and Its Implementation Embedded in the DLV System

This page describes an advanced Magic-Set method and its implementation, which has been embedded into the DLV system by Mario Alviano, Chiara Cumbo, Wolfgang Faber, Gianluigi Greco, Nicola Leone.

Implementation

The implementation is included in the main DLV binary since release 2011-12-21.

Experiments

We have performed several experiments, comparing our implementation to evaluation without Magic-Set and to a previous Magic-Set proposal by Sergio Greco.

Some of the instances we used are available for the problems: Ancestor, SimplePath, StrategicCompanies.

Usage

We refer to our Magic-Set method by notation DMS and to our optimized Magic-Set method by notation ODMS. The system will turn on a suitable optimization by default. For using DMS (without further optimizations) use command line option -ODMS, for DMS with subsumption checking (but without further optimizations) -ODMS+, for full ODMS use -OODMS . To turn off magic sets, use -ODMS- or -OODMS-.

Since a Disjunctive Datalog program may have more than one answer set there are different reasoning modes (brave/credulous and cautious/skeptical) to decide whether a query is satisfied. In order to choose the appropriate one, you have to specify (on the command line) -FB or -FC, respectively. If you know that your program has exactly one answer set, just use -FB.

We would like to point out that the magic set optimization will be performed only if the program does not contain unstratified negation and has no integrity constraints or occurrences of strong negation. Disjunction and stratified negation is, however, supported (and the main target of our work).

We suggest to run an example to get familiar with the system.

For instance, for running the first Ancestor problem instance with Disjunctive Magic-Sets under brave reasoning use the command line:

 DLVmagic -FB S100 -ODMS

For instance, for running the same problem with Optimized Disjunctive Magic-Sets under cautious reasoning use this command line:

 DLVmagic -FC S100 -OODMS

For further informations about DLV's general options and usage, please refer to DLV online manual.