问题标签 [optimathsat]

我基本上只是在运行一个实验，在其中运行一个带有变体输入的文件。该代码适用于某些值，而对于某些值，它只是给了我：

在我的结果文件中，这是我的输出：

我正在运行的实验总是在相同的输入值处停止（输出文件中打印的最后一个），然后从那里开始出现所有解析器错误！为什么这样做？我该如何解决？我已经尝试了多种解决方案，我在这里找到了类似问题（与 bc 相关），但没有一个有效。

solve minimize即使有多个最佳解决方案，我也只能得到一个解决方案。我在求解器配置中启用了多个解决方案的打印输出。其他最优解solve satisfy与非最优解一起找到。

可能是基数函数card()在两个集合的大小相等的情况下按枚举值排序吗？换句话说，那card(A, B) > card(B, C)？如果是这样，我是否必须切换顶点的表示？

我正在创建一个 MiniZinc 程序来查找给定图形的最小顶点覆盖。此示例中的图表是这样的：

最小顶点覆盖解决方案是： [{A, B, C, E}, {A, B, E, F}, {A, C, D, E}, {B, C, D, E}, {B, C, D, F}, {B, D, E, F}]. 我的代码只输出{A, B, C, E}.

数据文件：

求解程序：

我正在使用带有内置 Gecode 6.1.1 的 minizinc，我想最大化一个目标函数，其值远大于 max int 32。32 位整数的最大值是 2147483646。虽然似乎没有太多信息与minizinc 参考中的整数最大值相关。然而，以下测试表明 Minizinc 使用 32 位整数。

测试非常简单，它只是试图最大化一个 var int。

结果是

最大整数 = 2147483646

结果接近最大 int32 值，并且 miniZinc 似乎无法进一步“最大化”它。以下示例返回一个奇怪的错误。

错误消息如下。该错误消息的信息量不是很大，但在尝试使用大于 2147483646 的数字时会显示。

错误：行号中的整数文字无效。2 错误：语法错误，行号中出现意外的“，”。2 进程以非零退出代码 1 结束

我的问题如下：我可以将 int64 位整数或任何其他大整数表示与 minizinc 一起使用吗？如果可以，如何？（使用浮点数不是一种选择）理想情况下，我想举一些例子来说明如何最大化某些东西

继续另一篇文章（Minizinc：生成有效班次）。我试图在双 ls 之间最多有 2 分钟。使用常规约束执行此操作非常困难，因为转换表会很大（路径太多）。有什么办法可以解决吗？我试过这个，但它给了我错误：

嗨，帕特里克……我又卡住了……我继续开发正则表达式，但我达到了 55 个状态……然后我停止了。我正在尝试一种不同的方法，即在连续工作日之间建立一系列休息时间。例如：mmmtnllmmlttlnnlllm（m1 早上 6 点到 13 点；m 早上 7 点到 14 点开始；t 晚上 14 点到 21 点；晚上 22 点到 7 点；l 休息日；o 办公室 10 点到 14 点；im 早上 6 点到 14 点待命；它on call night 13 to 22; ino on call night 21 to 7) 应该创建一个数组，如 17,17,24,24,48,48,17,48,48,16... 这是轮班的开始时间 [day+ 1] - (轮班开始时间 [天] + 轮班持续时间 [天])。这是编码的。连续工作班次之间必须有 12 小时或更长时间。

当有休息日（l）时，我打算重复最后一个休息时间（示例中为 48,48）。这个我不知道该怎么做。然后的想法是计算周期之间的工作日以检查以下内容： - 连续工作班次之间至少 12 小时 - 在 48 小时或更长时间休息之前的周期最多有 5 个工作日。- 休息 54 小时或更长时间前的周期最多为 6 个工作日。

夜晚的限制（一晚后 48 小时，除非是另一个晚上或休息日，两晚后 54 小时）我已经用约束完成了它，或者我可以用正则表达式来做......这很好

有任何想法吗？

我编写了这段代码，可以在我的 Linux 远程机器上执行一些不同输入的重复实验。

我已经在我自己的 mac 机器上执行了这段代码并且它有效（使用 gtime 而不是 /usr/bin/time ）但现在我收到了这个错误，我不知道它是什么意思/

当我尝试手动执行指令时，我得到了这个：

我检查了file.smt2，它应该是，然后发生这种情况

所以现在我正在使用 SAT 来解决最小顶点覆盖问题，这是我对图 G = {V,E} 的编码有 k 个顶点覆盖，下面是子句：

首先，至少一个顶点在顶点覆盖中：

那么，任何一个顶点都不能在顶点覆盖中出现两次：

之后，顶点覆盖中的特定位置只能出现一个顶点：

最后，顶点覆盖中的至少一个顶点应该来自边：

现在我可以通过使用这种编码获得最小的顶点覆盖，但是效率很差。我只能得到小于 20 个顶点的任何图的结果，否则只需要几分钟和几小时就能得到结果。我现在正在考虑将其从 SAT 进一步降低，也许是 3SAT。但看起来我不能简单地将所有子句从 nCNF 更改为 3CNF 以获得相同的结果。谁能帮我弄清楚下一步该怎么做？我需要全新的编码吗？

太感谢了。

顺便说一句，我正在使用 MiniSAT 作为求解器。

我们可以在 z3 中以增量方式使用 MaxSMT 求解器（优化）的先前解决方案吗？另外，有没有办法在优化器上打印出软断言？

我想使用 z3 优化类来获得次优结果，同时仍然能够控制我与最佳结果之间的距离。我正在使用 C++ API。

例如，CPLEX 具有分别用于相对容差和绝对容差的参数 epgap 和 epagap。它使用当前的下限或上限（取决于它是最小化还是最大化）来评估当前解决方案与最佳解决方案之间的距离（最多）。

当近似解决方案已经足够好时，这会导致运行时间更短。

这可能使用优化类，还是我需要使用求解器实例来实现并自己控制边界？

您如何为 z3 优化器设置超时，以便在超时时为您提供最知名的解决方案？

后续问题，您可以将 z3 设置为随机爬山还是始终执行完整搜索？

我正在编写一个需要将一些转换Int为BitVec反之亦然的问题的 BV 编码。

在mathsat/optimathsat一个可以使用：

在z3一个可以使用：

在CVC4一个可以使用：

问：

• 有签名z3的功能吗？（看起来没有。）bv2intBitVec
• CVC4有什么功能bv2int吗？（我没有任何线索。）
• 是否有记录这些转换功能的地方？（关于逻辑/理论的 SMT-LIB 网页似乎没有任何关于它们的信息。）

注意：我受限于基于文本的 SMT-LIB 接口（没有 API 解决方案）。