预期可满足的 Clingo 程序

Clingo program expected to be satisfiable

我正在 Clingo 5.0.0 中测试一些涉及算术的程序,我不明白为什么下面的程序无法满足:

#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).

我希望答案包含:a(object1) a(object2) b(object3) go(object1,object2,object3)。

关于 Clingo 的算术,我可能想念一些东西。

恐怕大家对ASP的误解还挺多的。

  1. 您不能为谓词赋值 (value(a,b,c)=1.5)。谓词形成原子,可以是真或假(包含或不包含在答案集中)。
  2. 我假设你的最后一条规则应该导出原子 go(X,Y,Z)。规则确实以相反的方式工作,导出的内容在左侧。
  3. 没有可能的浮点运算,你必须将你的值扩大到整数。

你的问题可能看起来像这样,但这只是在黑暗中摸索:

#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.

最后一条规定: 导出 go(object1,object2,object3) 如果 value(object1,object2,object3,2) 为真且 2 > 1a(object1) 为真且 a(object2) 为真且 b(object3) 为真且 object1 != object2 .