问题标签 [optimathsat]

我遇到了一个之前提到的问题，我并没有完全得到解决方案（将替代与简化相结合）。在我的编码中，我有严格的不等式，我需要将 epsilon 设置为 0 或非常小的值。例如，我有以下简化的 Python 代码：

如何让 p 被分配最大值 1？（现在分配为 1/2。）非常感谢！

目前我正在仔细研究 Minizinc。Minizinc 在求解模型时会在输出窗口中显示我的模型的所有有效解。我有点困惑，因为我没有要求 minizinc 将模型作为满意度问题来解决。是否有可能只显示最佳解决方案？感谢您的回答。

最好的祝福

我正在使用 Runtime.getRuntime().exec() 方法运行“optimathsat.exe”文件。我的代码就像

运行此代码后，它在控制台中显示以下行

并在 bibi.txt 文件中显示以下错误

但是，当我将上述代码的一些行复制到一个单独的项目（只有一个类）中，并在 winCommand 变量中替换生成的命令时，它可以完美地工作。

我猜第一个项目的配置不正确，但我不知道该如何解决。

问题：是否可以在 z3 中控制对模型返回值的某种偏好？

示例：给定以下命题逻辑公式，有两种可能的模型。

• a: True, b: True, c: False （首选）
• a: True, b: False, c: True （仍然有效，只是“第二选择”）

我想通过布尔公式/断言本身来控制 wherea和bare模型True应该优先于 wherea和care模型True。但是考虑到b不可能True因为添加了额外的约束的情况，应该返回带有a和c存在的模型。True

SMT2 公式： 这里是 SMT2 示例公式，可以通过rise4fun进行测试。

观察：我注意到实际上可以通过实际切换子句中子句的顺序来控制是否b或c是否在返回的模型中。对于这个微不足道的例子，这在某种程度上是可靠的还是偶然发生的？Trueandor

我正在研究一个玩具问题来学习 minizinc。取一个介于 0 和 9 之间的值的数组（现在硬编码为 3 大小），并找到总和等于乘积的组合。

输出

这可以按预期工作，但是，接下来我尝试进行约束，以便值必须按顺序增加。

首先我尝试了这个：

这是不令人满意的。我在想这可能是由于i+1索引大于最后一项的数组大小。所以我在 forall 中添加了一个条件，以防止最后一项的索引超出范围：

然而，这也是不令人满意的。

我的概念理解有些不对劲。我的方法有什么问题？

I'm trying to minimize a variable, but z3 takes to long in order to give me a solution.

And I would like to know if it's possible to get a solution when timeout gets triggered.

If yes how can i do that?

Thx in advance!

我想并行化内部循环（重复）。

我已经安装了 GNU 并行并且我知道一些基础知识，但是因为循环有多个命令，我不知道如何并行化它们。

我将循环的内容转移到另一个脚本，我猜这是要走的路，但我的 3 个命令需要获取变量（tracelength、ratio、short、long）并根据它们运行。任何想法如何将参数从脚本传递到下标。还是您对并行化有更好的了解？

我正在编辑这个问题，因为我使用了下面的答案，但现在我的执行时间总是 0.00，不管 file.smt2 有多大。

这是新版本的代码：

我需要执行下面的命令（作为脚本的一部分），但我不知道按什么顺序放置东西才能正确执行。我想要做的是将file.smt2作为 optimathsat 的输入 ，执行它，获取执行时间。但我希望使用所有 CPU 内核并行执行多次。

我#!/bin/bash -x在文件开头添加了查看正在发生的事情，这是输出：

...从第一行，我可以看出顺序是错误的。从第 2,3 和 4 行开始，缺少语法。我怎样才能解决这个问题？

我需要 results.csv 中给出的数据按顺序排列。每个作业都会打印其输入，即开头提到的 3 个变量：$tracelength、$short、$long和$ratio，然后是该作业的相关执行时间；都在一条线上。到目前为止，我的结果看起来像这样：

我怎样才能修复订单？为什么执行时间总是0.00？file.smt2是一个大文件，执行时间绝不可能是0.00。

我需要执行一个命令并获取它的执行时间。我正在使用 gtime 但输出与我想要的有点不同。

gtime 返回执行结果，然后返回执行时间。我需要将命令的输出（我需要它只是时间）存储在一个变量中，然后再使用它。有没有办法更改命令以仅获取执行时间？

所以如果我写下面的命令：

那么这是我得到的输出示例：