2

我的问题总结:
我有一个像这样的Petri网(ILP)的线性方程组:

int[][] a = {
        {-1, 0, 0, 0},
        {1, -1, 0, 0},
        {1, 0, -1, 0},
        {0, 1, 0, -1},
        {0, 0, 1, -1},
        {0, 0, 0, 1}};

    int[] A = {0, 0, -1, 0, 0, 1};

x1, x2, x3, x4>=0;
x1, x2, x3, x4;  //--> must be integer

这些问题可能有更多的变量和约束。方程永远不是不等式。它也可以最大化或最小化。

我检查了一些关于所有整数问题的示例,但它们无法处理变量多于约束或其他方式的系统。

在像lp_solve这样的软件中,我可以处理这些问题,但对于这个解决方案,我必须处理许多 .dll 文件和包装器的东西。

我正在寻找 Java 解决方案或简单的嵌入库。我真的很感谢你的帮助,因为我有点卡住了。

4

1 回答 1

0

我有一些你可能会使用的 Java 代码将这些东西提供给 SMT 求解器。

基本上,Petri 网表示为两个稀疏矩阵,参见托管网络的类

可以在此处找到将其作为约束提供给 SMT 求解器的使用示例:提供状态方程的代码

根据我的经验,封装 SMT 求解器比插入 ILP 求解器更加通用和舒适。

于 2019-04-15T20:23:53.143 回答