3

使用合金 4.2，以下合金模型...

sig E {}
sig G {}
sig D extends G {
  x: E
}
sig F1 extends G {
  x: G
}
sig F2 extends G {
  x: G
}
sig F3 extends G {
  x: G
}
sig F4 extends G {
  x: G
}
run {} for 3

... 执行以下输出：

Executing "Run run$1 for 3"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   486 vars. 66 primary vars. 748 clauses. 158ms.
   Instance found. Predicate is consistent. 36ms.

如果您只是将签名重命名D为H（真正的单字符更改），则基础 SAT 问题的变量和子句的数量会发生变化：

Executing "Run run$1 for 3"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   494 vars. 66 primary vars. 762 clauses. 23ms.
   Instance found. Predicate is consistent. 28ms.

为什么？这种行为什么时候出现？有没有办法命名签名以确保获得尽可能少的变量和子句？

更多细节：

我确信这与签名名称的字母顺序有关。如果您选择任何低于 的名称E，您将获得 486 个变量，如果选择任何高于您的名称，H您将获得 494 个变量。

在我寻找一个最小示例的过程中（从我相当大的模型开始），我目睹了一些情况，其中选择三个不同的名称会产生三个不同数量的变量。我在这个过程中丢失了这些例子，但我记得涉及到字母顺序。

对于小尺寸，这可能看起来没什么，但如果你run {} for 12不是3，变量的数量变为 17415 和 19439，因此差异超过 10%。我也见证了我的实际模型的巨大差异（有更多的签名，但不是更大的范围）。

谢谢，

4

0 回答 0