Documentation

The communication between wasp and the external propagators follows a synchronous message passing protocol. The protocol is implemented by means of method calls. Basically, the propagator must be compliant with a specific interface described below. Whenever a specific point of the computation is reached the corresponding method of the propagator is called, e.g. when a literal is true the method onLiteralTrue is called. Some of the methods of the interface are allowed to return values that are interpreted by WASP.

Method: setScriptDirectory(id, dirname) - Return: -

id: an integer representing the id of the directory. At the moment this is a (useless) integer equal to 0 since only directory can be specified.
dirname: the current directory of the script.

This method is invoked before starting and specifies the current directory of the python script.

Note: Optional.

Method: addedVarName(id, name) - Return: -

id: an integer representation of a variable.
name: the name associated to the id.

This method is invoked while reading the name associated to an atom.

Note: Optional. Try DLV2 for a convenient way to avoid this method.

Method: getLiterals(*lits) - Return: L

lits: a list of literals derived as true during the parsing. The first element of the list is the number of variables used in wasp. Literal 1 is always false.
L: a list of integers.

This method returns a list of literals L attached to the propagator, i.e. when a literal in L is derived as true a notification is sent to the propagator using either method onLiteralTrue or method onLiteralsTrue.

Note: Required only if one between onLiteralTrue and onLiteralsTrue is used. Otherwise, it is optional.

Method: onVariableElimination(var) - Return: -

var: a positive integer representing the id of a variable.

This method is invoked when the variable is removed by clause rewriting.

Note: Optional.

Method: simplifyAtLevelZero() - Return: L

L: a list of literals.

This method is invoked before starting the search and returns a list of literals L to be inferred as deterministic consequence. In order to trigger an incoherence add "1" to L.

Note: Optional.

Method: onStartingSolver() Return: -

This method is invoked when the computation starts. After this point all the simplifications are done.

Note: Optional.

Method: onLiteralTrue(lit, dl) - Return: L

lit: a literal whose truth value is true.
dl: a positive integer representing the decision level of the solver.
L: a list of literals.

This method is invoked whenever a literal becomes true by propagation or by choice. Returns a list of literals L to infer as true. Afterward, the method getReason (or getReasonForLiteral) is invoked.

Note: Required if checkAnswerSet is not used. Otherwise, it is optional. Exactly one between onLiteralTrue and onLiteralsTrue is required.

Method: onLiteralsTrue(*lits) - Return: L

lits: a list of literals that are true. The first element of the list is the current decision level of the solver.
L: a list of literals.

This method is invoked after unit propagation and notifies all literals that become true by propagation and by choice. Returns a list of literals L to infer as true. Afterward, the method getReason (or getReasonForLiteral) is invoked.

Note: Required if checkAnswerSet is not used. Otherwise, it is optional. Exactly one between onLiteralTrue and onLiteralsTrue is required.

Method: endPropagation(dl) - Return: L

dl: a positive integer representing the current decision level of the solver.
L: a list of literals.

This method is invoked after all propagations are done. It can be used to postpone the propagation of some of the literals. Returns a list of literals L to infer as true. Afterward, the method getReason (getReasonForLiteral) is invoked.

Note: It can be used only if onLiteralTrue is used.

Method: getReason() - Return: S

S: a set of literals.

This method returns a clause modeling the reason for the assignments made by onLiteralTrue (onLiteralsTrue). That is, let P = {p1;...;pm} be the literals returned by onLiteralTrue (onLiteralsTrue), and the reason is of the form l1 ^ ... ^ ln -> p (for each p in P). Then, S={-l1;...;-ln}.

Note: Required only if one between onLiteralTrue and onLiteralsTrue is used. Otherwise, it is useless. Exactly one between getReason and getReasonForLiteral is required.

Method: getReasonForLiteral(lit) - Return: S

lit: one of the literals inferred as true by onLiteralTrue (onLiteralsTrue).
S: a set of literals.

This method returns a clause modeling the reason for the assignment of one literal. That is, if the reason is of the form l1 ^ ... ^ ln -> lit. Then, S={-l1;...;-ln}.

Note: Required only if one between onLiteralTrue and onLiteralsTrue is used. Otherwise, it is useless. Exactly one between getReason and getReasonForLiteral is required.

Method: onLiteralsUndefined(*lits) - Return: -

lits: a list representing the undefined literals. The first element of lits is the current decision level of the solver.

This method is invoked when some of the literals notified as true are again undefined (e.g. after an unroll or a restart).

Note: Required only if one between onLiteralTrue and onLiteralsTrue is used. Otherwise, it is optional.

Method: checkAnswerSet(*lits) - Return: i

lits: a list of literals representing the answer set.
i: an integer.

This method is invoked after an answer set is found. The role of the method is to check whether the answer set is consistent with the propagator. Returns 0 if the answer set is inconsistent, !=0 otherwise.

Note: Required only if onLiteralTrue and onLiteralsTrue are not used. Otherwise, it is optional.

Method: checkPartialInterpretation(*lits) - Return: i

lits: a list of literals representing the partial interpretation.
i: an integer.

This method is invoked after each propagation. The role of the method is to check whether the interpretation is consistent with the propagator. Returns 0 if the interpretation is inconsistent, !=0 otherwise.

Note: Optional.

Method: getReasonsForCheckFailure() - Return: L

L: a list of clauses.

This method is invoked after a failure of checkAnswerSet or checkPartialInterpretation. It returns a list of clauses modeling the reasons for the failure. Each clause is a set of literals S={l1;...;ln} interpreted as l1 v ... v ln. The clauses must be separated by 0. Note that the first and the last element of the list are expected to be equal to 0. If you import the library wasp.py you can simply use wasp.createReasonsForCheckFailure(clauses). See running examples for more details.

Note: Required only if checkAnswerSet or checkPartialInterpretation are used.

Method: onNewLowerBound(lb) - Return: -

lb: a positive integer representing the lower bound.

This method is invoked only on optimization problems whenever a new lower bound of the optimum solution is found.

Note: Optional.

Method: onNewUpperBound(ub) - Return: -

ub: a positive integer representing the upper bound.

This method is invoked only on optimization problems whenever a new upper bound of the optimum solution is found.

Note: Optional.

Method: addWeakConstraints(*lits) - Return: L

lits: a list of literals representing the answer set.
L: a list of soft clauses.

This method is used to lazily add weak constraints (you have to enable the option --lazy-weakconstraints). The method is invoked after an answer set is found and it returns a list of soft clauses modeling the weak constraints to add. Each soft clause is a set of literals S={l1;...;ln} interpreted as l1 v ... v ln. The soft clauses must be separated by 0. Note that the first and the last element of the list are expected to be equal to 0. If you import the library wasp.py you can simply use wasp.createWeakConstraints(softClauses). See running examples for more details.

Note: Optional.

Method: addWeightsForWeakConstraints() - Return: L

L: a list of weights associated to each soft clause.

This method is invoked after addWeakConstraints and returns a list of positive weights associated to each soft clause. Note that the i-th soft clause is associated with the i-th weight. Moreover, the weights must be long, so if you are using python2 you have to explicit add long(e) for each element e in L. If you import the library wasp.py you can simply use wasp.createWeights(weights). See running examples for more details.

Note: Required if addWeakConstraints is used. Otherwise, it is optional.

Description of the module wasp (file wasp.py)

The module wasp can be used to simplify the interaction with the solver.

Method: createReasonsForCheckFailure(clauses) - Return: L

clauses: a list of clauses, where a clause is a list of integers.

This method takes as input a list of clauses and produces a list that can be interpreted by wasp as reasons for the check failure.

Method: createWeakConstraints(weak) - Return: L

weak: a list of soft clauses, where a soft clause is a list of integers.

This method takes as input a list of soft clauses and produces a list that can be interpreted by wasp as weak constraints.

Method: createWeights(weights) - Return: L

weights: a list of integers (long) representing the weights of the weak constraints.

This method converts each integer in the list weights in a long. This is useless if python3 is used.

Method: fromNogood(conj) - Return: L

conj: a list of integers representing a conjunction.

Converts the conjunction into a disjunction.

Method: fromLitImplConj(lit, conj) - Return: L

lit: an integer representing a literal.
conj: a list of integers representing a conjunction.

Takes as input the implication lit → l₁ ∧ ... ∧ l_n (for l₁, ... ,l_n in conj) and creates a list of clauses

c₁ ∧ ... ∧ c_n, where c_i = -lit ∨ l_i (for i = 1, ... ,n).

Method: fromLitImplDisj(lit, disj) - Return: L

lit: an integer representing a literal.
disj: a list of integers representing a disjunction.

Takes as input the implication lit → l₁ ∨ ... ∨ l_n (for l₁, ... ,l_n in disj) and creates the clause -lit ∨ l₁ ∨ ... ∨ l_n.

Method: fromConjImplLit(lit, conj) - Return: L

lit: an integer representing a literal.
conj: a list of integers representing a conjunction.

Takes as input the implication l₁ ∧ ... ∧ l_n → lit (for l₁, ... ,l_n in conj) and creates the clause

-l₁ ∨ ... ∨ -l_n ∨ lit (for l₁, ... ,l_n in conj).

Method: fromDisjImplLit(lit, disj) - Return: L

lit: an integer representing a literal.
disj: a list of integers representing a disjunction.

Takes as input the implication l₁ ∨ ... ∨ l_n → lit (for l₁, ... ,l_n in disj) and creates a list of clauses

c₁ ∧ ... ∧ c_n, where c_i = lit ∨ -l_i (for i = 1, ... ,n).

Method: incoherent() - Return: i

i: an integer.

Return 0 to indicate that the answer set candidate is not valid.

Method: coherent() - Return: i

i: an integer.

Return 1 to indicate that the answer set candidate is valid.

Method: getTerms(predicateName,atomName) - Return: L

predicateName: a string representing the name of the predicate.
atomName: a string representing the full name of the atom.

Return a list of string representing the terms. For example, given atomName="pred(1,2,hello)" and predicateName="pred", it returns ["1","2","hello"].

Running examples

Consider the following simple encoding

{a;b;c;d}.

We want to keep answer sets where exactly two atoms among a, b, c, and d must be true. In the following we present two different python implementations.

Solution 1

interpretation = []; atoms=[]
TRUE = 1; FALSE = -1; UNDEFINED = 0
countTrue = 0; countFalse = 0

def addedVarName(var, name):
    global atoms
    atoms.append(var)

def getLiterals(*lits):
    global interpretation
    #The first position of lits contains the number of atoms used in wasp
    interpretation = [UNDEFINED for i in range(0, lits[0]+1)]
    #Attached to all changes of the truth values
    l = [-i for i in atoms]
    l.extend(atoms)
    return l

def getVariablesToFreeze():
    #Freeze all atoms
    return atoms
    
def onLiteralTrue(lit, dl):
    global interpretation, countTrue, countFalse
    #Count true and false atoms and propagate if needed.
    interpretation[abs(lit)] = lit / abs(lit); #1 TRUE, -1 FALSE    
    if lit >= 0:
        countTrue += 1
    else:
        countFalse += 1
    output = []
    if countTrue == 2:
        output = [-i for i in atoms if interpretation[i]==UNDEFINED]
    elif countFalse == 2:
        output = [i for i in atoms if interpretation[i]==UNDEFINED]
    return output

def getReason():
    #Let T={a,b} be the true atoms, then the reason for the assignment is a ^ b (clause -a v -b).
    reason=[]    
    if countTrue == 2:
        reason=[-i for i in atoms if interpretation[i]==TRUE]
    else:
        reason=[i for i in atoms if interpretation[i]==FALSE]
    return reason

def onLiteralsUndefined(*lits):
    global interpretation, countTrue, countFalse
    #If a literal is again undefined the interpretation is restored.
    for i, l in enumerate(lits):
        if i == 0:    continue
        if l >= 0:    countTrue -= 1
        else:    countFalse -= 1
        interpretation[abs(l)] = UNDEFINED
    return

Solution 2

import wasp

answer = []; atoms = []

def addedVarName(var, name):
    global atoms
    atoms.append(var)

def checkAnswerSet(*answer_set):
    global answer
    #Check whether the answer set has exactly two atoms true
    count = sum([1 for i in atoms if answer_set[i] > 0])
    if count != 2:
        answer = answer_set
        return wasp.incoherent()
    return wasp.coherent()

def getReasonsForCheckFailure():
    #In case of failure compute the clause
    global answer
    reasons=[[-answer[i] for i in atoms]]
    return wasp.createReasonsForCheckFailure(reasons)

Consider again the following simple encoding

{a;b;c;d}.

We want to lazily instantiate the following weak constraints


:~ not a. [1@1,a]
:~ not b. [1@1,b]
:~ not c. [1@1,c]
:~ not d. [1@1,d]

One possible solution is the following

import wasp

answer = []; atoms = []

def addedVarName(var, name):
    global atoms
    atoms.append(var)

def addWeakConstraints(*answer_set):
    global answer
    answer = answer_set
    soft = [[i] for i in atoms if answer_set[i] < 0]
    return wasp.createWeakConstraints(soft)

def addWeightsForWeakConstraints():
    global answer
    weights=[1 for i in atoms if answer[i] < 0]
    return wasp.createWeights(weights)

Wasp

Documentation

Description of the module wasp (file wasp.py)

Running examples