坚持：如何做"If p causes UNSAT then q."

Question

下面的代码

% Facts
a.
% Rules
-a :- a, not not p.

将事实p.添加到上面将使其成为UNSAT。在语言中有没有办法添加一个规则来显示这一点?就像

q :- Assuming p causes UNSAT.

如添加规则 的解决方案

{p; q} = 1.

不会工作。如果p.导致UNSAT，它会在答案集中给出q.，这是我想要的。但是，当p.不引起UNSAT时，会给出p.和q.作为答案集。在p.没有引起UNSAT的情况下，我不希望q.出现在答案集中。

我希望能够检查某些事实是否导致某个复杂条件不成立。例如，假设问题的一部分要求您检查图是否包含哈密顿循环。如果图满足条件，查找哈密顿环的程序将返回UNSAT，但我不希望程序结束，因为还有其他计算要做。

Answer 1

您可以将其视为优化问题。所以一些通常是约束的东西变成了一个特殊的谓词，然后你寻求最小化。基本上你有这样的形式:

err(err1) :- some-bad-condition.
err(err2) :- some-other-bad-condition.
#minimize{ 1,XXX: err(XXX) }.

这里XXX是每个错误条件的唯一标识符。优化语句找到一个最小化errs数量的模型。

唯一需要注意的是，这会增加问题的复杂性;你现在解决的是优化问题，而不是决策问题。在调试asp程序时，这是一个有用的技巧，但对于大型/困难的问题，它可能太慢了。