Search code examples
logic-programminganswer-set-programmingclingo

Clingo program expected to be satisfiable


I am testing some programs involving arithmetics in Clingo 5.0.0 and I don't understand why the below program is unsatisfiable:

#const v = 1.

a(object1).
a(object2).
b(object3).
value(object1,object2,object3) = "1.5".
value(X,Y,Z) > v, a(X), a(Y), b(Z), X!=Y :- go(X,Y,Z).

I expected an answer containing: a(object1) a(object2) b(object3) go(object1,object2,object3).

There is probably something I miss regarding arithmetic with Clingo.


Solution

  • I fear there are quite some misunderstandings about ASP here.

    1. You can not assign values to predicates (value(a,b,c)=1.5). Predicates form atoms, that can be true or false (contained in an answer set or not).
    2. I assume that your last rule shall derive the atom go(X,Y,Z). Rules do work the other way around, what is derived is on the left hand side.
    3. There is no floating point arithmetic possible, you would have to scale your values up to integers.

    Your problem might look like this, but this is just groping in the dark:

    #const v = 1.
    
    a(object1).
    a(object2).
    b(object3).
    value(object1,object2,object3,2).
    go(X,Y,Z) :- value(X,Y,Z,Value), Value > v, a(X), a(Y), b(Z), X!=Y.
    

    The last rule states: Derive go(object1,object2,object3) if value(object1,object2,object3,2) is true and 2 > 1 and a(object1) is true and a(object2) is true and b(object3) is true and object1 != object2.