表示不等式点和DNF之间距离的Python库

Question

让我们把变量的数量确定为4:所以x0，x1，x2，x3。

我正在寻找一个python构造，它允许我：

(i)在内存中存储一个分离的正规公式，其中原子公式是不等式: a0x0 + a1x1 + a2x2 + a3x3 >= a4或等式: a0x0 + a1x1 + a2x2 + a3x3 == a4。

(ii)给定一个不在DNF中的公式，我有一个函数将其转换为DNF。

(iii)给定一个点(u1，u2，u3，u4)，我可以找到这一点到DNF公式的设定距离。

我知道numpy允许我编写原子公式并计算它们从点到点的距离，但它不允许我编写它们的连词或分离；我不能计算从一个点到一个DNF的设定距离。

我甚至签出了pyeda，但是原子公式必须是布尔变量，不允许不等式和等式。

我可以重写整个代码来为DNF定义自己的类，也可以定义自己的距离函数，但我不想重新发明轮子。我可以使用哪个python库(以及如何)使我以最简单的方式完成任务？

Answer 1

我的反应是对你的问题的解释，但我认识到，我正在填补一些空白，我的假设。

(i)可以用线性规划解决。

(ii)这是一个非常公开的问题，我会略过它。

(iii)如果您对距离sum |x[i] - u[i]|感到满意，那么仍然可以使用linproc来处理问题，但是您必须使用辅助变量。