Home

I-DLV

I-DLV is a full-fledged Answer Set Programming and Datalog reasoner. It supports the ASP-Core-2 standard language; nevertheless, the system supports additional linguistic extensions such as list terms and external atoms. I-DLV is also a full-fledged deductive database system, supporting query answering powered by the Magic Sets technique. I-DLV has also been integrated as the grounding module of the completely renewed second version of the logic-based Artificial Intelligence system DLV.

How to cite I-DLV

Francesco Calimeri, Davide Fuscà, Simona Perri, Jessica Zangari: I-DLV: The New Intelligent Grounder of dlv. AI*IA 2016: 192-207

Francesco Calimeri, Davide Fuscà, Simona Perri, Jessica Zangari: I-DLV: The new intelligent grounder of DLV. Intelligenza Artificiale 11(1): 5-20 (2017)

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 suppresses the startup banner and blank lines.

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

• --output-format sets the output format:

  • 0=smodels numeric format (Default);
  • 1=plain textual format;
  • 2=query textual format, (if the input program contains a query, only its answer(s) are printed);
  • 3=aspif numeric format.

• --t prints in textual mode (same behaviour of --output-format=1).

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

• --print-rewriting prints the rewritten program.

• --query prints the results of the input query (same behaviour of --output-format=2).

Grounding Options

• --check-edb-duplication if present, duplicates in EDB are removed.

• --choice-rewriting sets the rewriting strategy to adopt for choice rules:

  • 0=by means of disjunction;
  • 1=by rewriting choice rules into smaller choice rules (Default);
  • 2=by rewriting choice rules in a compact way.

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

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

• --look-ahead enables the look ahead mechanism.

• --ordering sets 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 disables the projection rewriting.

  • 0 = disables every projection rewriting;
  • 1 = disables the rewriting of isolated variables;
  • 2 = disables the rewriting of functional terms.

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

• --FC enables cautious reasoning.

• --FB enables brave reasoning.

• --no-magic-sets disables the magic sets rewriting.

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

  • 0 = Always (Each decomposable rule is decomposed according to the best estimated decomposition);
  • 1 = Never (Do not decompose any rule);
  • 2 = Heuristic mode (Default, Each decomposable rule is decomposed according to the best estimated decomposition only if its decomposition is estimated as convenient).

• --decomp-algorithm sets the decomposition algorith:

  • 0 = Minimum Degree (Default);
  • 1 = Maximum Cardinality Search;
  • 2 = Minimum Fill;
  • 3 = Natural Ordering.

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

• --decomp-size-body-limit sets the maximum allowed number of literals in rules body for which the fitness mechanism has be enabled (Default 10).

• --decomp-limit sets the decomposition not improvement limits (Allowed values: [0,20] and <= of decomposition iterations, Default 3).

• --decomp-iterations sets the decomposition tentative iterations (Allowed values: [0,20], Default 5).

• --decomp-no-fitness disables the fitness mechanism of decomposition rewriting.

Statistics Options

• --time the system prints the grounding time of each rule.

• --gstats the system displays grounding statistics.

General Options

• --help the system prints this guide and exit.

• --stdin the system reads 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 ("."). Currently, I-DLV supports annotations for customizing two of the major aspects of the grounding process, body ordering and indexing as well as further optimizations intervening in its grounding process.

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}).

The projection rewriting can be customized for any rule, by preceding it with the line:

  %@rule_projection(n).

where n can either 0, 1 or 2, as for the command-line projection option described above.

The rewriting of arithmetic terms, disabled by default, can be enabled for any rule, by specifying before it the following annotation:

  %@rule_rewrite_arith().

Similarly, the aligning substitutions technique disabled by default, can be enabled for a specific rule by preceding it with:

  %@rule_align_substitutions().

while, for enabling the look-ahead technique, the annotation to use is the following:

  %@rule_look_ahead().

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

• Francesco Calimeri
• Davide Fuscà
• Simona Perri
• Jessica Zangari