问题标签 [choco]

If have a set of rules -

1 : If x then a

2 : If x then b

Then these rules shall be conflicting as we shall not know what is the action to be performed when x is triggered. Therefore -

Now suppose I want to check for consistency of rules such as -

1: If (100 < m < 120) and (200 < n < 220) then output = 200

2: If (110 < m < 120) and (200 < n <210) then output =220

Clearly rules 1 and 2 are conflicting because if m = 115 and n = 205, then output can be either 200 or 220.

Is there a way I can check for the consistency of the above rules using the Z3 library ? Or using the pure SMT-lib2 ? Pls help. If you can give me an example of the actual code which can be run on https://rise4fun.com/Z3/vd?frame=1&menu=0&course=1 I shall be really grateful.

Thank you

我在 Java 中使用 choco 求解器。如何获得域的最大值？

例如，这是我的域：

如何获得域的最大值？（这里的最大值是 10）

当我运行 choco solver 4.0.6 时，我得到了这种解决方案：

除了 X 和 Y 的值，有人能告诉我解决方案的其余部分是什么意思吗？

我刚刚使用管理外壳中的以下步骤通过 nuGet 安装了 Chocolatey：Chocolatey nuget install。但是，当我尝试获取任何包裹时，系统会要求我提供凭据（我认为这不会发生）。谁能指出我做错了什么？

巧克力味的

我正在玩 choco solver 来解决一些任务调度问题。

我有几个作业和可能的插槽（可以执行作业）。有一些限制，例如：

• 每个插槽只能有一个作业 (C.1)
• 一个工作需要一定的时间t，并且槽有一个可用的持续时间d。该工作必须适合该可用持续时间：t<=d（C.2）

所以，基本上用一些基本/伪类来表达：

目前，我可以为每个作业分配一个插槽，假设作业的 id 和插槽是连续编号的

这按预期工作。但现在我也想对其他约束进行建模。但我坚持如何将工作/时段与时间/持续时间结合起来，因为时间和持续时间是一个因变量。

第一步，我为时间和持续时间建模了两个额外的变量：

现在，我需要表达时间应该适合持续时间（C.2）的约束。

是否可以定义这样的约束（无效/有效的伪代码）：

还是模型完全错误？！

也许有人有解决方案或想法？！

我choco用来解决虚拟机分配问题，这就是我想要做的：

假设我们有 3 个用于物理机属性的数组（PMcpu、PMram、PMbw）和 3 个用于虚拟机的数组（VMcpu、VMram、VMbw）。现在我们定义一个具有这些维度的矩阵：PM*VM这样 choco 将设置值（0 或 1 表示特定 VM 是否分配给 PM）。根据常识，我们知道 PM 资源应该大于或等于所有分配的 VM 资源的总量，因此我们将分配矩阵中的每个元素与相应的资源相乘，例如假设：

分配矩阵：

行代表 PM，列代表 VM，所以这里：

所以我写了这段代码：

我试图通过检查要在行中填充的矩阵的每一列来确保分配所有 VM model.arithm(sum_of_col.get(i), "=", 1).post();。如果我评论约束和目标，矩阵将被随机分配，但在应用约束时，choco 不会解决任何问题（没有输出，因为while(model.getSolver().solve()永远不会正确，所以 choco 似乎没有解决它）。我不知道我在哪里做错了。任何帮助表示赞赏:)

提前致谢

编辑：我意识到问题是 choco 只在第一次检查这些约束，所以当一切都为 0 时它会检查它，这就是它不会继续的原因，但是在 solve() 循环中添加约束后，我仍然得到相同的结果，也许我应该以choco理解它们的另一种方式应用这些约束，我现在真的很沮丧:(

我目前正在尝试 Choco Solver (4.0.8)，我正在尝试解决这个方程：

最大化
服从

我坚持最大化第一个方程。我想我只需要提示 VaraibleEQUATION应该是哪个子类型。

我想在 CHOCO 中模拟以下约束。请提供任何帮助

这就是我想要做的

给定产品的各种功能、功能选项以及功能之间的兼容性规则，我想生成所有可行产品配置的列表。

例如，我当前的用例类似于配置笔记本电脑。许多变量，如屏幕尺寸、内存、cpu、主板，每个变量都有多个有效值。我们也可以有限制，比如这个主板与这个 cpu 兼容等。我需要的输出是笔记本电脑所有有效配置的列表。

该场景看起来像一个典型的约束满足问题 (CSP)。我尝试了 Minion、Choco 等 CSP 库。不幸的是，它们只使用数字变量，并且兼容性规则也是一个数学函数。

我还尝试了http://labix.org/python-constraint，我在其中使用了功能约束，并将我的兼容性规则作为 If 语句提供。这适用于小场景。但根据我的要求，我将拥有 10 个功能，每个功能都有 4 到 5 个选项，从而产生数百万个配置。

有人可以建议我的要求的最佳方法吗？

我正在使用 choco 来解决 CSP，我的限制之一是一个变量 ( X[i][j]) 的总和小于N=10, and i=j=1....N.

我该如何做到这一点？感谢您的帮助。