DLV 2.0

DLV 2.0 is the new version of the ASP solver DLV, combining the grounder I-DLV and the solver WASP.

The 64-bit linux binary of DLV 2.0 can be downloaded here. The version with Python support can be downloaded here (you need to install Python 3.5 to execute this version).

DLV2-SERVER can be downloaded here. A complete user manual is available here.

All material for paper submitted at LPNMR 2017 can be downloaded here.

Example 1 of the LPNMR 2017 paper is the following ASP program:

#propagator(@file="prop.py",@elements={X,value : value(X); X,in : in(X)}).

edb(1..2).
{value(X) : edb(X)} = 1.
{in(X) : edb(X)}.

% :- value(X), #count{Y : in(Y)} = X.

The directive #propagator calls the python file prop.py reported below.

import wasp

# dictionary 'elements' is created by DLV2

valueAtoms = [key for key in elements.keys() if elements[key][1] == "value"]
inAtoms = [key for key in elements.keys() if elements[key][1] == "in"]

answer = []
valueAtom = None

def checkAnswerSet(*answer_set):
    global answer
    global valueAtom
    
    count = sum([1 for i in inAtoms if answer_set[i] > 0])
    value = None
    for i in valueAtoms: 
        if answer_set[i] > 0:
            value = elements[i][0]
            valueAtom = i
            break

    if count != value: return 1     # it's an answer set!
    
    # not an answer set!
    answer = answer_set
    return 0

def getReasonsForCheckFailure():
    global answer
    global valueAtom

    reason = [-valueAtom]
    reason.extend([(-i if answer[i] > 0 else i) for i in inAtoms])
    return wasp.createReasonsForCheckFailure([reason])