Skip to content
kaliaragorn edited this page Jun 25, 2018 · 55 revisions

I-DLV

I-DLV is intended as the new intelligent grounder of the logic-based Artificial Intelligence system DLV: it is an Answer Set Programming (ASP) instantiator that natively supports the ASP-Core-2 standard language. I-DLV core instantiation mechanism is based on semi-naive database techniques that proved to be reliable and efficient over a huge number of scenarios, especially when domain extensions are very large. I-DLV is also a full-fledged deductive database system, supporting query answering powered by the Magic Sets technique.

Download

You can download the latest stable release of I-DLV in the release section of github.

Usage

I-DLV can interoperate with the state-of-the-art solvers wasp and clasp. Indeed, by default I-DLV output is produced in a numeric format compliant with the mentioned solvers.

In order to interoperate with a solver type:

./idlv [filename [filename [...]]] | ./solver_executable

In order to obtain the ground program in textual format type:

./idlv --t [filename [filename [...]]]

Command-line Options

Output Options

  • --silent suppress the startup banner and blank lines.

  • --no-facts suppress the printing of EDB.

  • --output-format set the output format: 0=Numeric, 1=Textual.

  • --t print in textual mode.

  • --filter filter the specified predicates with the specified arity. Example: --filter=p1/2,p2/3.

  • --print-rewriting print the rewritten program.

  • --query print the results of the input query.

Grounding Options

  • --check-edb-duplication if present, remove duplicate EDB.

  • --rewriting set the rewriting strategy to adopt for choice rules: 0: Native Rewriting (Default); 1: By means of disjunction.

  • --rewrite-arith-terms enable the rewriting of arithmetic terms into assignment built-in atoms.

  • --align-dictionaries enable the dictionaries alignment mechanism.

  • --ordering set the body ordering criterion:

    • 0 = A basic ordering strategy that applies minor changes to the original ordering just to ensure a correct evaluation;
    • 1 = DLV Combined Criterion, the ordering criterion applied in DLV (See http://dblp.org/rec/html/conf/lpnmr/LeonePS01);
    • 2 = Combined+ Criterion (Default), a criterion that enhances the Combined one by considering comparisons;
    • 3 = Functional Terms Criterion, a criterion that pushes literals with functional terms down in the body;
    • 4 = Indexing Criterion, a strategy that tries to improve the quality of available indices;
    • 5 = Backjumping Criterion, a criterion that works in synergy with backjumping procedure employed in the rule instantiation task in order to facilitate it;
    • 6 = A Combination of criteria 4 and 5.
  • --no-isolated-filter disable the filtering mechanism of isolated variables.

  • --no-projection disable the projection rewriting of irrelevant variables.

  • --indexing set the indexing terms for the specified predicates. Example: --indexing=p/3={0,1};p/2={1}.

  • --FC enable cautious reasoning.

  • --FB enable brave reasoning.

  • --no-MS disable the magic sets rewriting.

  • --decomp configure the decomposition rewriting, inspired by LPOPT:

    • 0 = Always (Each rule which is decomposable, is decomposed),
    • 1 = Never (Do not decompose any rule),
    • 2 = Heuristic mode (Default, decompose a rule if its decomposition is estimated as convenient).
  • --decomp-algorithm set the decomposition algorith:

    • 0 = Minimum Degree (Default),
    • 1 = Maximum Cardinality Search,
    • 2 = Minimum Fill,
    • 3 = Natural Ordering.
  • --decomp-seed Set the random seed for the decomposition rewriting (Default 0).

  • --decomp-threshold set the decomposition threshold (Allowed values: [0,1], Default 0.5).

Statistics Options

  • --time print the grounding time of each rule.

  • --gstats display grounding statistics.

General Options

  • --help print this guide and exit.

  • --stdin read input from standard input.

Inline Customization: Annotations

I-DLV introduces a new special feature for facilitating system customization and tuning: annotations of ASP code. I-DLV annotations allow to give explicit directions on the internal grounding process, at a more fine-grained level with respect to the command-line options: they "annotate" the ASP code in a Java-like fashion while embedded in comments, so that the resulting programs can still be given as input to other ASP systems, without any modification.

Syntactically, all annotation start with the prefix "%@" and end with a dot ("."). The current I-DLV release supports annotations for customizing two of the major aspects of the grounding process, body ordering and indexing; additional options are being developed.

A specific body ordering strategy can be explicitly requested for any rule, simply preceding it with the line:

 %@rule_ordering(@value=Ordering_Type).

where Ordering_Type is a number representing an ordering strategy. In addition, it is possible to specify a particular partial order among atoms, no matter the employed ordering strategy, by means of before and after directives. For instance, in the next example I-DLV is forced to always put literals a(X,Y ) and X = #count{Z : c(Z)}} before literal f(X,Y ) , whatever the order chosen:

 %@rule_partial_order(@before={a(X,Y),X=#count{Z:c(Z)}},@after={f(X,Y)}).

As for indexing, directives on a per-atom basis can be given; the next annotation, for instance, request that, in the subsequent rule, atom a(X,Y,Z) is indexed, if possible, with a double-index on the first and third arguments:

  %@rule_atom_indexed(@atom=a(X,Y,Z),@arguments={0,2}).

Multiple preferences can be expressed via different annotations; in case of conflicts, priority is given to the first. In addition, preferences can also be specified at a "global" scope, by replacing the rule directive with the global one. While a rule annotation must precede the intended rule, global annotations can appear at any line in the input program. Both global and rule annotations can be expressed in the same program; in case of overlap on a particular rule/setting, priority is given to the rule ones.

Core Team