A 怎么能暗示 B 和 B 暗示 A 而 A 和 B 不等价？

Question

下面是一个合金模型，它将一组数字约束为正数和偶数。我展示了两种方法（两个谓词）来实现约束。我相信这两种方式是等价的（两个谓词产生的集合是相同的）。

为了测试这两个谓词是否等价，我创建了一个断言，它说：

defining_property => generate_set_members

检查断言没有产生反例。

然后我创建了一个断言：

generate_set_members => defining_property

检查该断言也没有产生反例。

最后，我使用iff 创建了一个断言：

defining_property iff generate_set_members

检查产生了一个反例。反例是一组包含正偶数和负偶数的数字。

嗯？

A => B 和 B => A 怎么可能是真的而A iff B 是假的？

one sig PositiveEven {
     elements: set Int 
}

/*
    To be in the set, a member must have these two properties:
    - it must be be positive 
    - it must be even
*/
pred defining_property {
    PositiveEven.elements = {i: Int | i >= 0 and (rem[i,2] = 0)}
}

/*
    0 is in the set
    If i is in the set, then i+2 is in the set
    Nothing else is in the set
*/
pred generate_set_members {
    0 in PositiveEven.elements
    all i: PositiveEven.elements - 0 | i.minus[2] in PositiveEven.elements
    // Create a complete set of positive even elements
    all i: Int | i.minus[2] in PositiveEven.elements => i in PositiveEven.elements
}

assert equivalent_constraints {
    //defining_property iff generate_set_members
    //defining_property => generate_set_members
    generate_set_members => defining_property
}

assert only_positive_even_numbers {
  //generate_set_members => 
  defining_property => 
    all i: Int | i in PositiveEven.elements <=> i >= 0 and i.rem[2] = 0
}

run defining_property
run generate_set_members
check equivalent_constraints
check only_positive_even_numbers

Answer 1

我在 4.2_2015-02-22 中复制了此内容，但在 4.2 中没有。据我所知，这是 4.2_2015 如何将 Kodkod 表示转换为 SAT 问题的一个错误。您可以通过将 SAT 求解器更改为“将 CNF 输出到文件”并在 4.2 和 4.2_2015 上运行相同的规范，然后在两个 .cnf 文件上运行 SAT4J 来重现这一点。 4.2 将有 72 个子句并且是可满足的（发现错误），而 4.2_2015 cnf 将有 66 个子句并且是不可满足的。 4.2 是稳定版本，而 4.2_2015 是实验性版本，因此现在切换回应该可以解决此问题。