如何在clingo中实现关键约束？

Question

我现在正在学习prolog，并尝试使用clingo来建模关键约束，但遇到了一些麻烦，希望有人能帮我。以下是我的问题：

1. 我想构建一个键约束，并在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).

但是，我仍然在想，是否可以将分离的约束放在一起，形成一个关键约束，从而使程序更加简洁？

1. 的另一个问题是如何在clingo中建立“存在某物”的事实，我想要实现的是使用clingo来判断给定的两组规则是否可以满足，下面是一个例子。

第一套规则说：“有一个学生的id是1，名字是mike"：

​

​

“两个身份证相同的学生应该有相同的名字和年龄”(这是一个关键的限制因素)：

​

​

因此，我在Clingo中将第一组规则写成：

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

假设给出了第二套规则，即“存在一个身份证为1，年龄为27岁的学生”：

​

​

第二套规则用Clingo写成：

stu(1,v,27).

我的问题是，如果简单地将这两组规则放在一个程序中，Clingo将判断它们不能满足原因("mike"，v) != (v，27)。因此，我的解决方案一定有问题(可能是建立存在的方法)，因为如果有一个id = 1、name = "mike“和年龄= 27的学生，这两套规则实际上是可以满足的。我想知道是否有一种方法可以用Clingo来判断上面提到的两套规则的可满足性，谢谢！

Answer 1

如果要使用元组比较发布完整性约束，请使用

:-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“作为”未给定“的占位符，这就是您出现问题的原因。你的任何问题都不存在，而且如果可能的话，它的风格也要干净得多，没有名字或年龄。

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