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

编程问答 2022-05-14

问题描述

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

  1. 我想构建一个关键约束并在 clingo 中编写如下内容
:-stu(X,Y1,Y2),stu(X,Z1,Z2),not(Y1=Z1,Y2=Z2).

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

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

但我仍然想知道是否可以将单独的约束放在一个关键约束中，使程序更简洁？

  1. 另一个问题是关于如何在 clingo 中构建“存在某些东西”的事实，我想要实现的是使用 clingo 来判断给定的两组规则是否可满足，这是一个例子。

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

enter image description here

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

enter image description here

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

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

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

enter image description here

第二组规则用 Clingo 编写为：

stu(1,v,27).

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

解决方法

如果您想使用元组比较发布完整性约束

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

可能就是你想写的。

类似的规则

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

相当于

:-stu(X,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) 谓词时，您实际上总是必须给出名称 AND 和年龄（“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,stu(ID,Name2,(Name1,Age1)!=(Name2,Age2).
clingologic