DLV User Manual

Definite Rules

The simplest case is if the truth of some statement depends on the truth of some other statements. As an example, reconsider our EDB stored in the file engine. Let us now define an IDB, which we will store in the file alarm. It should specify that if the furnace is hot (hot_furnace holds) and the pressure valve is closed (valve_closed holds), then alarm_on should hold.

	  alarm_on :- hot_furnace, valve_closed.

This construct is called a rule. The :- can be read as “if”, and the comma can be considered as an “and”. The part to the right of :- is referred to as body, the left hand side is termed head. If we call DLV on these two files, we see that alarm_on is indeed derived:

	  $ DLV -silent engine alarm
	  {alarm_on}

Of course, we usually want to make more general statements, involving some kind of variables. For instance, we might want to define the notion of a path (i.e., there is a sequence of arcs from one node to a second node) on any graph which is defined by means of the arc predicate. The following IDB does exactly that:

	  path(X,Y) :- arc(X,Y).
	  path(X,Y) :- path(X,Z), arc(Z,Y).

Note that X, Y, and Z are variables. The name of a variable is a sequence of letters, underscores and digits, starting with an uppercase letter. The name of a predicate can be any sequence of letters, underscores and digits, starting with a lowercase letter. So the program above says that there is a path from some X to some Y, if there is an arc from X to Y. The second rule is more difficult: It says that a path exists from X to Y, if there is a path from X to some Z (note that Z did not occur before in this rule) and there is an arc from this Z to Y. The second rule is worth looking at. The predicate path occurs both in the head and in the body of the rule, so it seems that something is defined by itself which seems odd. However, this is a common feature in logic programming and is called recursion. You can think of it as assuming that path is already completely defined, and specifying what conditions have to be met by the defined relation. Note that variables, which occur in the head, must also occur in the body. This is one of the safety requirements for rules (see  Chapter 3). If we take this program (assume it is stored in a file called path and apply it to the graph defined above, we see:

	  $ DLV -silent -nofacts simple_graph path
	  {path(1,2), path(1,3), path(1,4), path(2,3), path(2,4)}

Indeed, this result corresponds to the paths in the graph. Sometimes a variable is used to mask an argument which is not used in the rest of the rule. For example, if you want to define a node in some graph (specified in the same format as above), you could write:

	  node(X) :- arc(X,Y).
	  node(Y) :- arc(X,Y).

In the first rule Y is used to mask the second argument, in the second rule X masks the first argument of arc. DLV provides a feature which saves us from the need to invent variable names for these masking variables and which clarifies to readers of programs that a variable is just used for masking. This feature is called anonymous variable and denoted as _ (an underscore). In spite of its name, an anonymous variable is not a variable as in the original description. Its meaning can be described as follows: In a preprocessing step, each occurrence of an anonymous variable is replaced by a unique variable (which does not occur anywhere else in the same rule resp. constraint). The previous example (defining a node) can thus be rewritten as follows:

	    node(X) :- arc(X,_).
	    node(Y) :- arc(_,Y).

Disjunctive Rules

The rules above described definite knowledge, but Disjunctive Datalog (the language we use here) also provides several ways to define indefinite knowledge. A simple case is the one, where we know for sure that at least one of two conditions is true, but we are unable to determine which. For example, if we notice that it is not dark in a room, we know that either the sun shines or that some artificial light is on, or even both:

	  sunny v light_on.

The v (alternate notions are | and ;) indicates that this construct specifies disjunctive knowledge. Although the above may look similar to a simple fact, it is no definite knowledge and thus part of the IDB. Now let’s see how DLV acts on this input:

	  $ DLV -silent light
	  {sunny}
	  {light_on}

For the first time, the output consists of more than one model. Now it is also clear what a model represents: It represents different worlds for which the program gives reason. But something seems to miss: What about the model, in which both sunny and light_on are true? Practically all semantics (definitions of the meaning of a program) have a minimality criterion. That means that if there are two potential models and one of them is a superset of the other, it should not be considered because it contains some redundant information. Since {sunny, light_on} is a superset of both {sunny} and {light_on}, it is not considered a proper model. Note that because of this minimality criterion one disjunctive rule can give reason to exactly one of its atoms in the head. If several head atoms are true in one rule, there must be some other rules which require the truth of these additional true atoms. Another example: Say you want to find some node coloring of a graph, which is represented by arcs. That is, we have several colors to choose from, say red, green, and blue and every node should be assigned one color, but we do not know which one. To this end, we reuse the node definition of  Example 2-11. The more interesting part is the last rule. Similar to the previous example, we specify that for any node X, either color(X,red), color(X,green) or color(X,blue) must hold. Here the minimality criterion ensures that exactly one color is assigned to a node.

	  node(X) :- arc(X,_).
	  node(Y) :- arc(_,Y).

	  color(X,red) v color(X,green) v color(X,blue) :- node(X).

Let us view the output by DLV for this example (file coloring) on our example graph in simple_graph:

	  $ DLV -silent -nofacts coloring simple_graph
	  {node(1), node(2), node(3), node(4), color(1,red), color(2,red), color(3,red), color(4,red)}
	  {node(1), node(2), node(3), node(4), color(1,red), color(2,red), color(3,red), color(4,green)}

	  [... and so on ...]

	  {node(1), node(2), node(3), node(4), color(1,blue), color(2,blue), color(3,blue), color(4,green)}
	  {node(1), node(2), node(3), node(4), color(1,blue), color(2,blue), color(3,blue), color(4,blue)}

Negative Rules

We have not yet introduced another important feature of Disjunctive Datalog: negation. Several proposals of what negation should mean in this context have been made. DLV implements one of those, which has been widely accepted as a reasonable proposal: the Stable Model Semantics. Negation is treated as “negation as failure”. In other words: If an atom is not true in some model, then its negation should be considered to be true in that model. We will not go into detail here, the examples should give you an idea how this works. With this mechanism we can, for example, define the complementary graph of a given graph. This is the graph which has the same nodes, but of all possible arcs, it has exactly those arcs which do not exist in the original graph.

	  node(X) :- arc(X,_).
	  node(Y) :- arc(_,Y).

	  comparc(X,Y) :- node(X), node(Y), not arc(X,Y).

Here comparc describes the set of arcs in the complementary graph. Such an arc must go from one node to another node (possibly the same one), and this arc must not be contained in the original arc set. Note that node(X) and node(Y) need to be included in the body in order to satisfy the following safety requirement for rules: Variables, which occur in a negated literal, must also occur in a positive literal in the body. See Chapter 3.

	  $ DLV -silent -nofacts simple_graph compl_graph

	  {node(1), node(2), node(3), node(4), comparc(1,1), comparc(1,3), comparc(1,4), comparc(2,1), comparc(2,2), comparc(3,1), comparc(3,2), comparc(3,3), comparc(3,4), comparc(4,1), comparc(4,2), comparc(4,3), comparc(4,4)}

This was straightforward, but what if negation is used together with recursion? Let us look at a simple example:

	  bad :- not bad.

Now let us assume a model in which bad is true (in this case {bad}: It is not a valid model, since the only way in which bad could become true is by not bad being true, which clearly is not the case. On the other hand, a model not containing bad (here {}), is not valid either, because in this case not bad is true, hence bad must be in the model, but it is not. Consequently, no model exists.

	  $ DLV -silent bad

So in this case, there is no output at all, because as we have seen, the “empty model” {} is not valid.

True Negation

DLV implements yet another notion of negation: true negation. Negation as failure, which has been introduced above, does not support explicit assertion of falsity. Rather, if there is no evidence that an atom is true, it is considered to be false. There are several situations in which negation as failure is not appropriate because it is necessary that something is explicitly known to be false. For this reason, true negation is sometimes referred to as explicit negation. True negation is denoted by preceding an atom with “-” or “~”.

            cross_railroad :- not train_approaches.

            $ DLV -silent rail_naf
            {cross_railroad}

            cross_railroad :- -train_approaches.

            $ DLV -silent rail_true
            {}

            a.
            -a.

A very well-known problem is to find a coloring of a graph, such that no two adjacent nodes (i.e. two nodes which are connected by an arc) have the same color. To formulate this problem in Disjunctive Datalog, let us reconsider the coloring example from above:

	  node(X) :- arc(X,_).
	  node(Y) :- arc(_,Y).

	  color(X,red) v color(X,green) v color(X,blue) :- node(X).

The models of this program (together with a database describing the graph) correspond to all possible colorings. We only need to add a constraint which discards colorings where two adjacent nodes have the same color:

	  :- arc(X,Y), color(X,C), color(Y,C).

Assuming the combined code resides in 3col, the output then is:

	  $ DLV -silent -nofacts simple_graph 3col
	  {node(1), node(2), node(3), node(4), color(1,red), color(2,green), color(3,red), color(4,red)}

	  [... and so on ...]
	  
	  {node(1), node(2), node(3), node(4), color(1,blue), color(2,green), color(3,blue), color(4,red)}
	  {node(1), node(2), node(3), node(4), color(1,blue), color(2,green), color(3,blue), color(4,blue)}

Note that this program yields 24 models, while the previous coloring example led to 81 models.

            a v b.
            :- not a.

            a v b.
            :- -a.

Weak Constraints

This feature allows us to formulate several optimization problems in an easy and natural way. While standard constraints (integrity constraints, strong constraints) always have to be satisfied, weak constraints express desiderata, i.e., they should be satisfied if it is possible, but their violation does not “kill” the models. The answer sets of a program P with a set W of weak constraints are those answer sets of P which minimize the number of violated weak constraints. They are called Best Models of (P,W). Note that a program may have several best models (violating the same number of weak constraints). Weak constraints can be weighted according to their importance (the higher the weight, the more important the constraint). In the presence of weights, best models minimize the sum of the weights of the violated weak constraints. Weak constraints can also be prioritized. Under prioritization, the semantics minimizes the violation of the constraints of the highest priority level first; then the lower priority levels are considered one after the other in descending order. Syntactically, weak constraints are specified as follows.

            :~ Conj. [Weight:Level]

where Conj is a conjunction of (possibly negated) literals, and both Weight and Level are positive integers. Weights and priority levels are allowed to be variables, provided that these variables also appear in a positive literal in Conj. The user can omit the weight or the priority or both, but all weak constraints must have the same syntactic form (i.e., the user is free to specify only weights or only priorities, or both, but all constraints of the program must have the same syntactic form).

            a v b.
            c :- b. 
            :~ a.
            :~ b.
            :~ c.

	    $ DLV -silent example1

            Best Model: {a}
            Cost ([Weight:Level]): <[1:1]>

            root(a).
            node(a). node(b). node(c). node(d). node(e).
            edge(a,b,4). edge(a,c,3). edge(c,b,2). edge(c,d,3). edge(b,e,4). edge(d,e,5).

            in_tree(X,Y,C) v out_tree(X,Y) :- edge(X,Y,C), reached(X).
            :- root(X), in_tree(_,X,C).
            :- in_tree(X,Y,C), in_tree(Z,Y,C), X != Z.

            reached(X):- root(X).
            reached(Y):- reached(X), in_tree(X,Y,C).
            :- node(X), not reached(X).

            :~ in_tree(X,Y,C). [C:1]

	    $ DLV -silent -nofacts min_sp_tree

            Best model: {reached(a), out_tree(a,b), in_tree(a,c,3), reached(b), reached(c), 
            in_tree(b,e,4), in_tree(c,b,2), in_tree(c,d,3), reached(e), reached(d), 
            out_tree(d,e)}
            Cost ([Weight:Level]): <[12:1]>

Finally, we show an example where both weights and priorities are specified.

	    employee(a). employee(b). employee(c). employee(d). employee(e).
            know(a,b). know(b,c). know(c,d). know(d,e).

            same_skill(a,b).
            married(c,d).

            member(X,p1) v member(X,p2) :- employee(X).
            :~ member(X,P), member(Y,P), X != Y, not know(X,Y). [1:1]
            :~ member(X,P), member(Y,P), X != Y, married(X,Y). [1:2]
            :~ member(X,P), member(Y,P), X != Y, same_skill(X,Y). [1:2]

	    $ DLV plan -silent -filter=member

            Best model: {member(a,p2), member(b,p1), member(c,p1), member(d,p2), member(e,p2)}
            Cost ([Weight:Level]): <[6:1],[0:2]>
            Best model: {member(a,p1), member(b,p2), member(c,p2), member(d,p1), member(e,p1)}
            Cost ([Weight:Level]): <[6:1],[0:2]>

If you specify the -costbound=weight[,weight] option on the command line, all of the models with a cost less-or-equal than costbound will be computed. Note that not all of the computed models will be best models. You can associate a positive integer with each priority level of costbound. If, instead of an integer, _ is specified the corresponding weight is unbound. For instance, running DLV with the option

            $ DLV take2.dl -costbound=5,10,_

sets up an upper bound for the cost of the computed models, where the first two priority levels must have a value less-or-equal than 5 and 10, respectively, while the last one is unbound. Note that the rightmost weight is associated with the highest level. If you specify fewer priority levels than occur in the input, only weights corresponding to the lower priorities will set up the upper bound of the cost, the remaining levels will be unbound. On the other hand, superfluous higher levels will be ignored. For instance, running the following command line for Example 2-16 we will obtain the following results

           $ DLV min_sp_tree -silent -filter=member -costbound=13
           {in_tree(a,c), in_tree(c,b), in_tree(c,d), in_tree(d,e)}
           Cost ([Weight:Level]): <[13:1]>
           {in_tree(a,c), in_tree(b,e), in_tree(c,b), in_tree(c,d)}
           Cost ([Weight:Level]): <[12:1]>

If costbound is less than the cost of the best model(s), no model is output. Note that the number of computed models can be limited also under option -costbound. For instance running

            $ DLV take2.dl -costbound=10 -n=1

asks for computing one model whose cost is at most 10.

Built-in predicates

In addition to those predicates defined by the user, some predicates are already built into DLV and available for all programs. These predicates have names different from those that can be defined by users and must not be redefined. An atom with a built-in predicate is referred to as a built-in atom. Like ordinary atoms, built-in atoms can be negated by using negation-as-failure.

	  number(X) :- #int(X). 

	  $ DLV -silent -N=5 number
	  {number(0), number(1), number(2), number(3), number(4), number(5)}

	  lessthan(A,B) :- #int(A), #succ(A,B).
	  lessthan(A,C) :- lessthan(A,B), #succ(B,C). 

	  $ DLV -silent -N=3 lessthan
	  {lessthan(0,1), lessthan(0,2), lessthan(0,3), lessthan(1,2),
	   lessthan(1,3), lessthan(2,3)}

        pred(X..Y).

        weekday(1..7).

        weekday(1).
        weekday(2).
        weekday(3).
        weekday(4).
        weekday(5).
        weekday(6).
        weekday(7).

        #maxint=19.
        bignumber(#maxint).

        #const namedConstant = constant.

          #const rate = 5.
          due(2). due(10).
          pay(X) :- due(Y), X=Y*rate.

          $ DLV -silent -N=50 numconst
          {due(2), due(10), pay(10), pay(50)}

          #const nickname = mickey.
          username(u1). username(u2).
          user(X,nickname) :- username(X).

          $ DLV -silent symconst
          {username(u1), username(u2), user(u1,mickey), user(u2,mickey)}

          #const rate = 5.
          #const new_rate = rate.
          p(rate).
          p(new_rate).

          $ DLV -silent remark1
          {p(5), p(rate)}

          #const a = b.
          #const b = a.
          a(a).
          b(b).

          $ DLV -silent remark2
          line 2: constant term 'b' already used.
          Aborting due to parser errors.

          q :- 0 <= #count{X,Y : a(X,Z,k),b(1,Z,Y)} <= 3.
          q(Z) :- 2 < #sum{V : d(V,Z)}, c(Z). p(W) :- #min{S : c(S)} = W. :- #max{V : d(V,Z)} > G, c(G).

            {Vars : Conj}

              q(Z) :- 1 < #count{X : a(X,Y,Z), not d(2,Y,goofie)}, c(Z).

              I = {d(1,1), d(1,3), d(3,3)}

              S = {<1,d(1,3)>, <3,d(3,3)>}

            #count{<1,d(1,3)>, <3,d(3,3)>}

            emp(1,goofie,1250).
            emp(2,willy,700).
            emp(3,woody,750).
            emp(4,jerry,900).
            emp(5,tom,1050).

            over1000(I,S) :- emp(I,N,S), S > 1000.
            over1000nr(X) :- #count{I : over1000(I,W)} = X.

             {<1,over1000(1,1250)>,<5,over1000(5,1050)>}

            #count{over1000(1,1250),over1000(5,1050)}

              $ DLV -silent -nofacts employees query1.dl
              {over1000(1,1250), over1000(5,1050), over1000nr(2)}

            warnMeOver1200 :- #count{I : emp(I,N,S), S > 1200} > 0.

            salaryTotal(X) :- #sum{S,I : emp(I,N,S)} = X.

              $ DLV -silent -nofacts employees query3.dl
              {salaryTotal(4650)}

            warning :- #sum{S,I : emp(I,N,S)} > 4500.

            lowest(X) :- #min{S : emp(I,N,S)} = X.

            lowest(X) :- emp(_,_,X), not existsLowerThan(X).
            existsLowerThan(W) :- emp(_,_,W), emp(_,_,W1), W1 < W.

            highest(X) :- #max{S : emp(I,N,S)} = X.

            $ DLV -nofacts employees query6.dl
              {highest(1250)}

              :- root(X), in_tree(_,X,C).

            :- root(R), not #count{X : in_tree(X,R,C)} = 0.

            :- in_tree(X,Y,C), in_tree(Z,Y,C), X != Z.

            :- edge(_,Y,_), not #count{X : in_tree(X,Y,_)} = 1.

            reached(X) :- root(X).
            reached(Y) :- reached(X), in_tree(X,Y).
            :- node(X), not reached(X).

            in_tree(X,Y,C) v out_tree(X,Y) :- edge(X,Y,C).

            :- root(R), not #count{X : in_tree(X,R,C)} = 0. 
            :- edge(_,Y,_), not #count{X : in_tree(X,Y,_)} = 1.
 
            :~ in_tree(X,Y,C). [C:1]

              npersons(24).  % number of people
              #maxint = 24.  % number of people
              person(K1):- #int(K1),  K1 > 0, K1 <= K, npersons(K).

              like(1,2).
              dislike(2,3).
              ...

              ntables(3).    % number of tables
              nchairs(8).    % number of chairs            

              %  Guess if person P sits at table T or not.
              at(P,T) v not_at(P,T) :- person(P), table(T).

              %  The number of persons at a table T must not exceed the number of chairs.
              :- table(T), nchairs(C), not #count { P: at(P,T) } <= C.

              %  A person is seated at precisely one table.
              :- person(P), not #count{T : at(P,T)} = 1.

              %  People who like each other should sit at the same table.
              :- like(P1,P2), at(P1,T), not at(P2,T).

              %  People who dislike each other must not sit at the same table.
              :- dislike(P1,P2), at(P1,T), at(P2,T).