0

我必须将一个多重集划分为两个总和相等的集合。例如，给定多重集：

1 3 5 1 3 -1 2 0

我会输出两组：

1) 1 3 3
2) 5 -1 2 1 0

两者之和为 7。

我需要使用 Z3（smt2 输入格式）和“线性算术逻辑”来执行此操作，其定义为：

formula : formula /\ formula | (formula) | atom
   atom : sum op sum
     op : = | <= | <
    sum : term | sum + term
   term : identifier | constant | constant identifier

老实说，我不知道从哪里开始，任何建议都将不胜感激。

问候。

4

2 回答 2

1

这是一个想法：

1- 为每个元素创建一个 0-1 整数变量c_i。如果元素在第一组中，则该想法c_i为零，如果在第二组中，则为 1。你可以通过说0 <= c_i和来做到这一点c_i <= 1。

2-第一组元素的总和可以写成1*(1 - c_1) + 3*(1 - c_2) + ... +

3-第二组中元素的总和可以写为1*c1 + 3*c2 + ...

于 2012-01-29T04:24:15.210 回答
1

虽然 SMT-Lib2 很有表现力，但它并不是最容易编程的语言。除非您有硬性要求必须直接在 SMTLib2 中编写代码，否则我建议您研究与 SMT 求解器具有更高级别绑定的其他语言。例如，Haskell 和 Scala 都有库，允许您在更高级别编写 SMT 求解器脚本。以下是使用 Haskell 解决问题的方法，例如：https ://gist.github.com/1701881 。

这个想法是，这些库允许您在更高级别进行编码，然后在幕后为您执行必要的 SMT 求解器翻译和查询。（如果您真的需要掌握问题的 SMTLib 编码，您也可以使用这些库，因为它们通常带有必要的 API，可以在查询求解器之前转储它们生成的 SMTLib。）

虽然这些库可能无法提供 Z3 允许您通过 SMTLib 访问的所有内容，但它们更容易用于解决大多数感兴趣的实际问题。

于 2012-01-30T01:56:39.233 回答