答案集编程-使事实无效

Question

我有一个关于答案集编程的问题，即当知识库中已经(也)存在默认语句时，如何使现有的事实无效。

例如，有两个人seby和andy，其中一个可以同时驾驶。可能的情况是，seby可以像第3行那样开车，但假设他的执照被吊销后，他就不能再开车了，所以我们现在有了4到7线，同时andy学会了驾驶，就像在第7行中所看到的那样。第6行显示，一次只能有一个人开车，除了显示seby和andy是不一样的。

1 person(seby).
2 person(andy).
3 drives(seby).
4 drives(seby) :- person(seby), not ab(d(drives(seby))), not -drives(seby).
5 ab(d(drives(seby))).
6 -drives(P) :- drives(P0), person(P), P0 != P.
7 drives(andy).

在上面的程序中，第3行和第7行与第6行相矛盾，Clingo求解器(我使用的)显然输出了UNSATISFIABLE。

说了这些之后，请不要说删除第3行，问题就解决了。问这个问题的目的是想知道，现在是否有可能使第3行变得无效，让第4行履行其职责。

但是，第4行也可以写成：

4 drives(P) :- person(P), not ab(d(drives(P))), not -drives(P).

提前谢谢。

Answer 1

我不完全理解这个问题。第3行和第4行是分开的规则，即使第4行的前面是false，第3行仍然是真的。换句话说，第4行看起来是多余的。

看来你想要一个选择。我假设ab(d(驱动器( seby ))表示seby已经失去了执照。所以，在第四行下面是你对只有有驾照的人的限制。第五行是选择，因此在默认情况下，andy或seby可以开车，但两者都不能。请注意，在地面程序中，第五行是如何等同于驱动器(Seby) :-不是驱动器(Andy)。和驱动器(安迪) :-不是驱动器(塞比)。您还可以使用优化语句将seby作为首选驱动程序(下面的选择规则类似于优化语句)。

person(seby).
person(andy).
ab(d(drives(seby))).
:- person(P), ab(d(drives(P))), drives(P).
1{drives(P) : person(P)}1.

Answer 2

如果某件事是真的，它必须永远是真实的。因此，这条线：

drives(seby).

永远都是真的。

然而，我们可以通过将这一事实纳入一个选择规则来解决这个问题。

0{drives(seby)}1.

这一行表示一个答案将有0到1 drives(seby).。这意味着我们可以有与drives(seby).相矛盾的规则，并且答案仍然是可满足的，但我们也可以让drives(seby).为真。

这两个方案：

0{drives(seby)}1.
drives(seby).

这个项目：

0{drives(seby)}1.
:- drives(seby).

是可以满足的。

如果可以的话，您很可能希望drives(seby).是真的，如果不能的话，您希望它是假的。要做到这一点，我们需要强制Clingo使drives(seby).成为现实，如果可能的话。我们可以通过使用优化来实现这一点。

一种简单的方法是计算存在多少drives(seby). (0或1)并使计数最大化。

我们可以用这一行来计算drives(seby).的数量：

sebyCount(N) :- N = #count {drives(seby) : drives(seby)}.

N等于域中drives(seby).的drives(seby).数。这将是0或1。

然后我们可以用这个语句来最大化N的值：

#maximize {N@1 : sebyCount(N)}.

这使sebyCount(N)域中具有优先级1的N的值最大化(数目越低，优先级越低)。