问题标签 [flatzinc]

fzn2smt工具允许通过Yices求解flatzinc公式。

当我尝试运行它时，求解器会回答UNKNOWN我测试的每个公式。例如：

但是，在给定的示例中，它似乎正确地2DPacking.fzn.smt在文件的同一目录中创建了实例2DPacking.fzn：

如果我手动运行Yices公式smt，我会得到一个肯定的结果：

问：有没有其他人有经验fzn2smt并知道如何解决这个问题？

为了确定我遇到的问题不是由于安装部分，我将在这里分享：

我还按照工具说明的要求修改了环境变量：

关于选项类型，Minizinc的规范（第 6.6.3 节）说：

概述。使用 opt 类型构造函数定义的选项类型，定义可能存在或不存在的类型。它们类似于 Haskell 的 Maybe 类型，为类型隐式添加新值<>。

[...]

初始化。opt 类型变量不需要在实例时初始化。未初始化的 opt 类型变量会自动初始化为<>.

我想用两种类型解析和处理以下约束opt：

但是，我不确定我应该期望什么作为参数的值s0以及s 在解析此约束时。

我可以简单地忽略opt修饰符的存在并假设约束签名等于以下一个吗？

如果不是，我应该如何处理？

我有以下MiniZinc代码示例：

mzn2fzn使用标准库执行的命令输出以下FlatZinc代码：

在这里，请注意最初在模型中y被声明为 a ，但正确地将数组元素的边界传播到 上，因此模型声明为 a 。set of 1..100MiniZincmzn2fznxyFlatZincyset of 1..10

现在，我想自定义 的内容，element_set.mzn以便在使用时调用我自己的谓词element_set，所以我将其更改为如下：

但是，此代码不会将数组元素的边界传播x到 上y，因此生成的FlatZinc文件y仍然声明为set of 1..100：

我想知道是否有人知道传播xover域的正确编码是什么y。我设法为其他element_T约束做到了这一点，但我无法找到一个优雅的解决方案element_set，因为我找不到合适的内置函数来执行此操作。

换句话说，我想得到

代替

我该怎么做？

默认情况下，自动计算MiniZincmzn2fzn模型中浮点除法的结果，并将其作为常量浮点值存储在生成的FlatZinc模型中。

例子：

文件test.mzn

翻译成

变得等于

相反，我们想要获得的是一个FlatZinc文件，内容如下：

其中float_div()是一个新引入的非标准FlatZinc约束。

是否可以通过使用约束目录的变体来生成原始问题的std这种编码，或者这种编码是否需要对工具的源代码进行更重大的更改mzn2fzn？在后一种情况下，我们可以提供一些指导吗？

***：我们有一些公式不适合有限精度浮点表示，因为它会将SAT结果更改为UNSAT.

我只是尝试运行mzn2fzn以下MiniZinc文件：

这是生成的FlatZinc文件：

的版本mzn2fzn如下：

我有以下问题：

• 什么是FlatZinc 1.6 标准float_div似乎没有提到的约束？
• 什么是FlatZinc 1.6 标准float_times似乎没有提到的约束？

是否有任何FlatZinc求解器实际上支持它们？

注意我实际上在FlatZinc 2.2.0 的文档中找到了这些函数的踪迹，但是，我不明白为什么这些函数是由 1.6 版生成的，mzn2fzn因为它的文档似乎没有提到它们中的任何一个。

我只想知道这两个 MiniZinc 求解器是否默认使用无限精度算术。

我是一名 CS 学生，我正在将 Gurobi 用于一个项目。

我在这里是因为我遇到了与 MiniZinc 驱动程序一起使用的 Gurobi 求解器的小问题。特别是我注意到 Gurobi 针对同一个优化问题（使用 MiniZinc 建模）返回两个不同的解决方案，但所有浮点问题变量的域不同。第一个问题使用的域等于-2^31.0 .. 2^31.0，而第二个问题使用的域等于-3.402823e+38..3.402823e+38。

在第一种情况下，Gurobi 返回等于1.0的解，在第二种情况下，它返回UNSATorUNBOUNDED。

最近引起我注意的是，一些最新版本的FlatZinc支持半具体化的谓词：

半具体化的谓词本质上表示由布尔变量隐含的约束，而不是等价于一个。

来源：文档

问：

• 现在所有全局谓词都有一个_reif版本吗？
• 所有全局谓词也都有_imp版本吗？

看里面的内容share/minizinc/可以看到 insidestd只nosets.mzn使用_imp了谓词，所以我的印象是还不是强制支持_imp谓词的。问：这是正确的吗？

查看文档，我发现了这一点：

因此，求解器库应尽可能提供约束的具体版本。该库包含fzn__reif.mzn用于此目的的文件。

来源：文档

如果我正确解释它，则没有必要支持_reif谓词，因为它们已经在其中重新定义share/minizinc（尽管它可能对性能有益）。问：这是正确的吗？

FlatZinc 文档说只有非标准谓词必须在 FlatZinc 模型的顶部声明：

模型中使用的非标准 FlatZinc 谓词必须在 FlatZinc 模型的顶部声明，在任何其他词汇项之前。谓词声明的形式

来源：链接

显然，mzn2fzn 编译器在编译文件的顶部添加了半具体化的谓词声明（参见： this github issue）：

我觉得这种行为有点令人困惑，因为半具体化的谓词似乎是标准的一部分。

问：

• 这不是一个错误，因为只有非标准谓词应该在文件顶部声明？
• 有没有办法压制这样的声明？

给定以下 minizinc 程序：

和redefinitions-2.0.mzn文件

我希望得到一个具体化的版本作为展平的输出，但我确实得到了：

我如何以及在哪里添加我支持该谓词的 reif 和 imp 版本的信息，因此处理速度可能比自动翻译快？（这个未解决问题的重复）