Clingo：如何做“如果 p 导致 UNSAT 则 q”。答案

【问题标题】：Clingo: How to do "If p causes UNSAT then q."Clingo：如何做“如果 p 导致 UNSAT 则 q”。
【发布时间】：2021-08-25 16:50:48
【问题描述】：

在下面的代码中

% Facts
a.

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

在上面添加事实p. 会导致它成为UNSAT。有没有办法在 cligo 中添加规则来显示这一点？类似的东西

q :- Assuming p causes UNSAT.

添加规则等解决方案

{p; q} = 1.

行不通。如果p. 导致UNSAT，它将在答案集中给出q.，正如我想要的那样。但是，当 p. 不会导致 UNSAT 时，它将给出 p. 和 q. 作为答案集。在p. 没有导致UNSAT 的情况下，我不希望q. 出现在答案集中。

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

【问题讨论】：

【解决方案1】：

您可能可以将其视为优化问题。因此，通常会成为约束的东西会变成一个特殊的谓词，然后您会设法将其最小化。基本上你有一些形式：

 err(err1) :- some-bad-condition.
 err(err2) :- some-other-bad-condition.

 #minimize{ 1,XXX: err(XXX) }.

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

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

【讨论】：

这确实解决了我给出的示例，但我希望在我的最后一段中澄清这将如何应用于哈密顿循环示例。据我了解，使用您的方法我会得到err(err1) :- cycle_exists. 行，但定义cycle_exists 相当于我问的问题，即检查是否有一个代码块（在这种情况下是一个找到哈密顿量的代码块循环）是可满足的。
你能提供一个更具体的例子来说明你试图建模的整体问题吗？也许您可以将您的程序分解为单独的程序并单独检查它们的可满足性？ SAT/UNSAT 适用于整个程序，因此在程序中，您应该将属性（或事实）视为持有和不持有。因此，对于哈密顿循环，如果没有循环，则没有使程序无法满足的约束，而是编码如果存在循环，则这些额外属性也必须成立，如果没有循环，则这些其他属性必须成立。
以下问题是我想解决的一个例子。 给定一个图 G。找出需要从 G 中删除的最小边数，使其不再包含哈密顿循环。
我认为你必须研究析取逻辑程序。这可能是一个 NP^2 难题。有办法为这些东西建模，但我没有足够的能力来解释它。