如何实现clingo中的key constraints？

Question

正在学习prolog，尝试使用clingo对关键约束进行建模，但遇到了一些麻烦，希望有人能帮助我。这是我的问题：

我想建立一个键约束，在clingo中写类似下面的东西

:-stu(X,Y1,Y2),stu(X,Z1,Z2),not(Y1=Z1,Y2=Z2).

作为完整性约束，但出现语法错误。我尝试了另一种表达方式，它似乎有效。

Y1=Z1:-stu(X,Y1,Y2),stu(X,Z1,Z2).
Y2=Z2:-stu(X,Y1,Y2),stu(X,Z1,Z2).

但我还是想知道是否可以将分离的约束合并为一个关键约束，使程序更简洁？

另一个问题是如何在clingo中构建fact 'there exists something'，我想实现的是用clingo来判断给定的两组规则是否可满足，这里有一个例子。

第一组规则说“存在一个id为1，名字为mike的学生”：

和“两个id相同的学生应该有相同的名字和年龄”（这是一个关键约束）：

所以我在 Clingo 中编写了第一组规则：

stu(1,"mike",v).
:-stu(X,Y1,Y2),stu(X,Z1,Z2),(Y1,Y2)!=(Z1,Z2).

假设第二组规则是“存在一个id为1，年龄为27的学生”：

第二组规则用 Clingo 写成：

stu(1,v,27).

我的问题是，如果简单地将这两组规则放在一个程序中，Clingo 会判断它们不能满足 cause ("mike",v) != (v, 27)。所以我的解决方案一定有问题（可能是建立存在的方式），因为如果你有一个 id = 1，name =“mike”和 age = 27 的学生，这两组规则实际上是可以满足的。我想知道如果有办法像上面提到的那样用Clingo来判断两组规则的可满足性，谢谢！

Answer 1

如果您想post使用元组比较的完整性约束

:-stu(X,Y1,Y2),stu(X,Z1,Z2), (Y1,Z2)!=(Z1,Z2).

大概是你想写的

像

这样的规则

Y1=Z1:-stu(X,Y1,Y2),stu(X,Z1,Z2).

相当于

:-stu(X,Y1,Y2),stu(X,Z1,Z2), Y1!=Z1.

回答你的第二个问题：

将年龄和姓名分成两个谓词。您引入了一个任意的“v”作为“未给出”的占位符，这就是您遇到问题的原因。 None 你的问题存在，而且如果可以没有名字或年龄，它也是更简洁的风格。

stu_name(123,"steve").
stu_age(123,42).
% it is not possible to have the same ID but different names
:- stu_name(ID,Name1), stu_name(ID,Name2), Name1 != Name2.
% it is not possible to have the same ID but different ages
:- stu_age(ID,Age1), stu_age(ID,Age2), Age1 != Age2.

将姓名和年龄分开可以让您没有两个条目之一。当你使用三元 stu(ID,Name,Age) 谓词时，你实际上总是必须给出一个名字和年龄（“v”不是什么神奇的东西，它会被解释为名字或年龄）

为了避免多个学生有相同的id，你可以这样写：

stu(123,"Anne",30).
stu(123,"Mia",14).
% it is not possible to have the same ID but not completely equal entries
:- stu(ID,Name1,Age1), stu(ID,Name2,Age2), (Name1,Age1)!=(Name2,Age2).

如何实现clingo中的key constraints？

How can I realize key constraints in clingo？

logic

clingo