Python libraries for representing distance between a point and DNF of inequalities

Question

Let us fix the number of variables to be 4: so x0, x1, x2, x3.

I am looking for a python construct which allows me to:

(i) store in memory, a disjunctive normal formula where the atomic formulas are inequalities: a0x0 + a1x1 + a2x2 + a3x3 >= a4 or equalities: a0x0 + a1x1 + a2x2 + a3x3 == a4.

(ii) Given a formula not in DNF, I have a function to convert it to such.

(iii) Given a point (u1,u2,u3,u4), I can find the set distance of this point to the DNF formula.

I know that numpy allows me to write atomic formulas and calculate their distance from a point, but it doesn't allow me to write conjunctions or disjunctions of them; and I can't compute set distance from a point to a DNF.

I even checked out pyeda, but there the atomic formulas have to be boolean variables, and inequalities and equalities are not allowed.

I can rewrite the whole code to define my own classes for a DNF, and define my own distance function, but I don't want to reinvent the wheel. Which python libraries can I use (and how) to make me achieve my task in the easiest fashion?

Answer 1

My response is to my interpretation of your problem, but I recognize that I am filling some gaps with my assumptions.

(i) can be solved with linear programming.

(ii) is a very open question, I will skip it.

(iii) If you are happy with the distance sum |x[i] - u[i]| the problem can still be handled with linproc, you will have to use auxiliary variables though.