首页 文章

解决合金中最大化问题(或其他优化问题)

提问于
浏览
3

如果不是1 . 5年前,我已经购买并阅读了软件抽象书(实际上很棒的书)几个月 . 我已经阅读过合金等在线教程和幻灯片 . 当然,我也做过自己的练习和一些模型 . 我甚至在一些confs中为Alloy讲道 . 恭喜合金顺便说一下!

现在,我想知道是否可以建模并解决合金中整数问题的最大化问题 . 我不知道怎么做,但我认为要求真正的专家可以给我一个更确定的答案 .

例如,假设您有一个类似于此的模型:

open util/ordering[State] as states

sig State {
  i, j, k: Int
}{
  i >= 0
  j >= 0
  k >= 0
}

pred subi (s, s': State) {
  s'.i = minus[s.i, 2]
  s'.j = s.j
  s'.k = s.k
}

pred subj (s, s': State) {
  s'.i = s.i
  s'.j = minus[s.j, 1]
  s'.k = s.k
}

pred subk (s, s': State) {
  s'.i = s.i
  s'.j = s.j
  s'.k = minus[s.k, 3]
}

pred init (s: State) {
  // one example
  s.i = 10
  s.j = 8
  s.k = 17
}

fact traces {
  init[states/first]
  all s: State - states/last | let s' = states/next[s] |
    subi[s, s'] or subj[s, s'] or subk[s, s']
  let s = states/last | (s.i > 0 => (s.j = 0 and s.k = 0)) and
    (s.j > 0 => (s.i = 0 and s.k = 0)) and
    (s.k > 0 => (s.i = 0 and s.j = 0))
}

run {} for 14 State, 6 Int

我本可以使用Naturals,但让我们忘掉它 . 如果我想要在最后状态中导致最大i,j或k的轨迹怎么办?我能限制它吗?

一些直觉告诉我,我可以通过反复试验来做到这一点,即找到一个解决方案,然后手动在模型中添加一个约束,使变量严格地大于我刚发现的一个值,直到它不可满足为止 . 但它可以更优雅,更有效地完成吗?

谢谢!

弗雷德

编辑:我意识到,对于这个特殊问题,当然最容易找到 . 保持初始状态的最大值按原样,只减少其他两个,你就是好的 . 但我的观点是说明一个简单的问题需要优化,以便它可以应用于更难的问题 .

1 回答

  • 3

    你的直觉是正确的:试验和错误肯定是一种可能的方法,我在类似的情况下经常使用它(例如找到需要我想要的属性的最小公理集) .

    我认为,能否更直接,更优雅地完成取决于问题的解决方案是由原子表示还是必须是集合或其他非原子对象 . 给定一个问题,其解决方案都是T型原子,一个谓词解决方案,对于一个问题的原子解决方案是真的,一个比较关系 gt ,它保持适当类型的原子,那么你当然可以写

    pred Maximum[ a : T ] {
      Solution[a]
      and 
      all s : T | Solution[s] implies
        (gt[a,s] or a = s)
    }
    run Maximum for 5
    

    由于Alloy绝对是一阶的,你不能为涉及集合,关系,函数,通过图形的路径等的解决方案编写等效谓词 . (或者,您可以编写它们,但分析器无法分析它们 . )

    但是当然也可以引入名为MySet,MyRelation等的签名,这样一个人就可以在问题中需要每个集合,关系等一个原子 . 这有时会起作用,但它确实遇到了这样的问题有时需要所有可能的集合,关系,函数等存在的困难(如在集合理论中那样),而Alloy通常不会创建一个原子在 univ 中为每个可能的对象集键入MySet . Jackson 在他的书中的3.2.3节(见"Is there a loss of expressive power in the restriction to flat relations?"),5.2.2 "Skolemization"和5.3 "Unbounded universal quantifiers"中讨论了这种技术,迄今为止的讨论已经重复了重复 . (我在书的副本中写了一个指向这些部分的附加索引条目,在 Headers 'Second-order logic, faking it'下,所以我可以在需要时再次找到它们 . )

    然而,所有这些都说: Jackson 在他的书的第4.8节中写道:“整数实际上并不是非常有用 . 如果你认为你需要它们,那就再想一想; ......当然,如果你有一个很大的数字问题,你呢?”可能需要整数(以及更多),但是然后Alloy可能不适合 . “

相关问题