DLV-Complex: a (short) Tutorial

 

This tutorial is aimed at helping you in properly running DLV-Complex programs. The capabilities offered by the system are shown by means of a few simple examples. Hereafter, the binary of the system is supposed to be named ‘dlv-complex’, while names of the file storing the proposed examples are specified for each example as a commented line (after a ‘%’ symbol). Thus, let’s start.

 

 

Consider the following program: 

 

 

 

Running DLV-Complex on this example, we obtain the following output:

 

 

 

The unique answer set is given. In this case, the only option specified on the command line is ‘-silent’. This is a DLV option (not peculiar for DLV-Complex) which suppresses various informational output and blank lines.

The finite-domain check is performed with success; thus, the program is guaranteed to terminate.

 

Consider now the following recursive program:

 

 

 

Running DLV-Complex on this example, we obtain:

 

 

 

The program does not pass the finite-domain check, because of the second argument of the predicate ‘p’. The system outputs the set of rules that are not recognized as finite-domain. Note that rules are printed as internally stored in the system, i.e., after the proper rewriting for managing function symbols and with unique identifiers in place of the original variables.

Even if the program is not recognized as finite-domain, it is easy to see that such a program is finitely-ground, as the increasing nesting level of the second argument of ‘p’ is ‘blocked’ by the first argument. We can then ask the system to skip the finite-domain check through the ‘-nofdcheck’ command line option, obtaining:

 

 

 

Let’s drop now the first argument of ‘p’, and consider the following modified version of the previous program:

 

 

 

The program still results as not finite-domain. But, in this case, if we ask the system to skip the finite-domain check (thus forcing the computation), it does not halt at all. Indeed, it indefinitely generates new ground atoms of the form ‘p(s(b))’, ‘p(s(s(b)))’, ‘p(s(s(s(b))))’… and so on. You’d better kill the process :)

 

Nevertheless, we still can perform some safe computation, even in this case. Indeed, we can force the system to limit the generation of ground atoms with a (fixed) maximum nesting level for their terms, by using the –MAXNL options. For instance, by specifying ‘–MAXNL=4’ on the command line, we obtain:

 

 

 

Let’s start now taking advantage from the availability of complex terms such lists and sets. The following program is intended in order to compute all possible ordered lists of numbers between 1 and 4. Note as lists are terms between square brakets (“[]”).

 

 

 

Unfortunately, the program results as no finite-domain.

 

 

 

Nevertheless, we know that the computation would terminate, because the possible elements of the lists are limited to the numbers 1..4, and each newly generated list (see the last recursive rule) must come from an already generated list by means of the addition of an element which is lower to the one which is currently the head of the list. Thus, we can safely skip the finite-domain check.

 

 

 

The error here comes from the need of set the maximum value for integer values within the program (the system requires this every time we exploit a built-in that involves integer values). We can do the job by setting “maxint” (in this case, by specifying “-N=10” on the command line), exactly as we would do while using DLV (see the DLV manual for further details), finally getting the result.

 

 

 

What to do now, if we want to exploit the provided library for list and set manipulation? We must first ensure to have the library itself (tipically, a file named ListAndSet.so or ListAndSet.dll, depending on your operating system): you can freely download it from the DLV-Complex website. By default, it is supposed to stay in the “./LIB” folder, where “.” is the folder containing the DLV-Complex executable. Of course, you can locate it anywhere else, provided that you tell the system where to find it.

Let’s have a look at the following example. It is intended to compute all lists of 3 elements or less chosen among {a,b,c,d} with no repetitions.

 

 

 

First of all, note the “#include<ListAndSet>” line in the preamble. This tells the system to include the library, so that we can exploit the built-ins there included. In this example, “#length(L)” (being “#length” an interpreted function) is returns (as a term) the length of list “L”; “#member(X,Y)” (being “#member” a built-in predicate) is true if “X” is a member of list “Y”. Please refer to the reference guide for a full list and details about what is available in “ListAndSet” library.

Running DLV-Complex on this example produces the following (expected) output.

 

 

 

The following program selects from a given EDB of words (represented as lists of chars) only those resulting as palindromic.

 

 

 

The result of the computation is the following:

 

 

 

Note that, this time, we did not need to skip the finite-domain check, as the program is finite-domain. Also, there’s no need to set “maxint”.

 

As a last example, let us imagine that the administrator of a social network wants to increase the connections between users. In order to do that, (s)he decides to propose a connection to pairs of users that result, from their personal profile, to share more than two interests. If the data about users are given by means of EDB atoms of the form user(id, {interest₁, . . . , interest_n}), the following program computes the set of common interests between all pairs of users (by means of predicate “sharedInterests”), and selects all pairs of users sharing more than two interests (by means of predicate “proposeConnection”.

 

 

 

Note as set are terms between braces (“{}”). In this example, “#intersection(S1,S2)” (being “#intersection an interpreted function) returns (as a term) the intersection of sets “S1” and “S2”; “#card(S)”, on the other hand, returns (as a term) the cardinality of set “S”.

Let us imagine that the “ListAndSet” library stays in folder “/usr/local/mylib”; we tell the system to look up there by means of option “-libpath”.