Open oscarbenjamin opened 10 months ago
Another reason is that this method already proves that the inequalities are or are not satisfiable
Note that for checking satisfiability we know what signs each polynomial is required to have which can be used to prune cases making the whole operation much more efficient. It is probably possible to do some pruning in the general case but I am not sure what the exact conditions would be and where they could be checked. Certainly some common cases could be handled more efficiently.
This is essentially a simplified version of a cylindrical algebraic decomposition but with one major restriction which is that it is only for strict inequalities and not equations or non-strict inequalities.
Note that even if sympy had CAD it would be useful to have a function like this because there are some cases where a full CAD would be far too expensive to compute but this more restricted version could still be computed. In many practical applications only full dimensional components are of interest.
The find_poly_sign
function above prunes cases that have the same signs for the polynomials. This assumes that we only care about finding cases where the polynomials have a give sign. That is different from enumerating all components within which the signs of the polynomials are unchanging which is what the _find_poly_sign
function computes. Both cases are useful in different situations. For the truth table we want the former but in other cases we want the latter. You can see the difference in a simple case like:
In [11]: find_poly_sign([x**2], [x])
Out[11]:
⎡⎛⎡ 2 ⎤ ⎞⎤
⎣⎝⎣x > 0⎦, {x: -1}⎠⎦
In [12]: _find_poly_sign([Poly(x**2)], [x])
Out[12]: [{x: -1}, {x: 1}]
In more complicated cases the difference is less obvious but the number of cases can be much larger without this pruning e.g.:
In [19]: for c, p in find_poly_sign([x**2+y**2-1, x+2*y], [x, y]): print(p, And(*c))
{x: 3, y: -2} (x + 2*y < 0) & (x**2 + y**2 - 1 > 0)
{x: 5, y: -2} (x + 2*y > 0) & (x**2 + y**2 - 1 > 0)
{x: 0, y: -1/2} (x + 2*y < 0) & (x**2 + y**2 - 1 < 0)
{x: 1/2, y: 0} (x + 2*y > 0) & (x**2 + y**2 - 1 < 0)
In [20]: for p in _find_poly_sign([Poly(x**2+y**2-1, [x, y]), Poly(x+2*y, [x, y])], [x, y]): print(p)
...:
{x: 3, y: -2}
{x: 5, y: -2}
{x: -1, y: -1/2}
{x: 0, y: -1/2}
{x: 7/8, y: -1/2}
{x: 2, y: -1/2}
{x: -2, y: 0}
{x: -1/2, y: 0}
{x: 1/2, y: 0}
{x: 2, y: 0}
{x: -2, y: 1/2}
{x: -7/8, y: 1/2}
{x: 0, y: 1/2}
{x: 1, y: 1/2}
{x: -5, y: 2}
{x: -3, y: 2}
I can see several different cases:
_find_poly_sign
does).Certainly the first case and possibly the second case can be handled much more efficiently than the code shown by pruning cases in different ways inside _find_poly_sign
. I suppose that a general function for this could allow an argument like list[Expr | Gt | Lt]
and then if Expr
is given it is assumed that all combinations of sign are wanted. A different function name could be used for distinguishing constant-sign vs sign like find_poly_sign
and find_poly_constant_sign
.
I'm not sure what a good API is...
For comparison Mathematica has the functions SemiAlgebraicComponentInstances
and GenericCylindricalDecomposition
. Also Mathematica's CylindricalDecomposition
function takes an option op
to specify what kind of decomposition is wanted.
These functions all take inequalities as arguments though so none of the quite produces the set of all points giving all signs meaning that they are not directly comparable to find_poly_sign
or find_poly_constant_sign
(they are all case 1 above). It would be good to make functions that are similar to those Mathematica functions though.
https://reference.wolfram.com/language/ref/SemialgebraicComponentInstances.html https://reference.wolfram.com/language/ref/GenericCylindricalDecomposition.html https://reference.wolfram.com/language/ref/CylindricalDecomposition.html
find_poly_constant_sign
Maybe this should be something like find_nonzero_instances
. It is a function that finds rational points that (redundantly) enumerate all geometric components in which the polynomials are nonzero.
I think that there are only two articles so far relevant to the discussion.
https://academic.oup.com/comjnl/article/36/5/432/392361 https://core.ac.uk/download/pdf/82649664.pdf
However, I'm not really sure if LC + Discriminants + Pairwise resultants can be right projection, and we should read the papers more meticuously about how to define the projection operators. For example, McCallum's projection often has more preconditions, that you should use squarefree decomposition first, or it may not always work. And also, original McCallum's projection I believe, expects you to add all coefficients, than the leading coefficients, while it looks slightly different for Strzebonski's article.
And we should also amalgamate some knowledge that for strict inequalities, it is no problem to use that projection operator.
CRootOf
or roots, real_roots
. So even if I have written everything with PolyElement, I can't avoid some overhead of converting to Expr
and such things.z < sqrt(1 - x**2 - z**2)
The paper from Strzebonski, for example, only gives examples with square roots, that can be done with symbolic computation, and avoids showing more complicated examples.
- One major bottleneck is that computing the roots
I'm pretty sure that RootOf can be made faster. Also there is an implementation of this in Flint but I am not sure how well exposed it is by python-flint:
In [1]: import flint
In [2]: p = flint.fmpz_poly([2, 0, 1])
In [3]: p
Out[3]: x^2 + 2
In [4]: p.complex_roots()
Out[4]: [([1.41421356237310 +/- 4.96e-15]j, 1), ([-1.41421356237310 +/- 4.96e-15]j, 1)]
- So even if I have written everything with PolyElement, I can't avoid some overhead of converting to
Expr
and such things.
You can use Poly.real_roots
rather than Expr
.
- The other major bottleneck comes from representing the results of solution as algebraic functions
Note that the code shown above deliberately does not do this. Every full-dimensional component is represented but only by rational points.
However, I'm not really sure if LC + Discriminants + Pairwise resultants can be right projection,
Maybe the projection that is needed depends on what you are trying to do. Our limited goal here maybe does not need as much as full CAD.
Can you think of a counter example where these are not sufficient to separate the full dimensional components?
I can see why square free would be needed e.g. to stop the discriminant from just being zero everywhere. For the resultant also I guess it is necessary to use gcd and then resultant of the cofactors. A full factorisation of everything would handle these cases but I'm not sure if that is a good idea: in context the factorisation is relatively cheap but the algorithm scales badly with the number of distinct polynomials so we want to avoid increasing that unecessarily.
I can't see why all coefficients rather than just LC would need to be added though. The roots are continuous functions of the coefficients provided the LC is nonzero.
Our limited goal here maybe does not need as much as full CAD.
I think that this applies to the limited CAD, like here as well. I think that the problem is often called 'open CAD'. I can't give the counter example yet, however, I think that it is better to ask for someone who comes up with the code to prove. It is not easy to see how it fails very complicated cases, because there are very limited numbers of examples given by the articles, and often the visualization is not intutitive if we think more of 4D+ cases. I think that Strzebonski's article may contain the proof.
You can use Poly.real_roots rather than Expr.
I thought that we should also avoid Poly
as well, because that uses dense representation. Maybe we only need dense univariate polynomial just before calculating the roots.
A full factorisation of everything would handle these cases but I'm not sure if that is a good idea:
I think that Strzebonski's article does not worry about using full factorization.
In our implementation for polynomials with rational number coe cients we use the set of irreducible factors of F, and our experience is that polynomial factorization is not a signi cant part of the execution time of the whole algorithm
I think that Strzebonski's article is good because it can be implementation with proof, and contains concrete algorithm such that we can extend with design/API issues.
I think that Strzebonski's article is good
Yes, I agree. It seems to describe exactly the algorithm that I was thinking of.
I am still unsure about what is good API though because different things can be useful for different situations.
I thought that we should also avoid
Poly
as well, because that uses dense representation.
In this particular situation I am not sure that the dense representation is bad. I have come to think now that the Poly representation is perhaps "semi-dense" for multivariate polynomials. Perhaps a better description of it is that it is a "recursive" representation whereas PolyElement
is a "flat" representation. An algorithm like this that naturally recurses through the variables seems to be almost precisely the situation that the DMP representation is designed for although it still might be the case that PolyElement
is faster in many cases.
A full factorisation of everything would handle these cases but I'm not sure if that is a good idea:
I think that Strzebonski's article does not worry about using full factorization.
I don't think that the cost of calling factor is significant in this context. Rather the cost is to do with having more polynomials after factorisation. For example if there are 2 polynomials and we factorise them each into 4 factors then we have 8 polynomials. Now instead of 2 discriminants and 1 resultant we need 8 discriminants and 28 resultants. Of course all of these will be lower degree though and maybe it is generally better to exchange a small number of large polynomials for a large number of small ones if the total degrees are the same (this is the case in other contexts).
We want to control the growth in the number of cells though and it is possible that we can end up having resultants between factors of the same polynomial that would lead to redundant cells. Presumably though the same polynomials will either end up appearing as discriminant factors or as resultant factors in the end so maybe we always end up having the same number of cells either way.
QEPCAD also contains the test sets, which can be helpful to verify the implementation in some scale
https://github.com/chriswestbrown/qepcad/tree/master/regressiontests
It doesn't look like any of the qepcad test suite is a case of only strict inequalities.
I have tried to implement with PolyElement, using the projection as described above
I think that one of the difficulty is that dealing with some missing features of sparse polynomial
(For example, resultant
still dispatches to dense version, however, we should have it implemented with sparse)
And the other major problem is fuzzy/surprising outputs of types for some functions like resultant, discriminant which mixes PolyElement/Ground outputs, and seems like causing errors, however, it can be improved.
I think that the low level API can just be simplified to 'points', and the problem is well defined that given a list of polynomials, regardless of the logical forumlations of inequality (like and-or combinations), a list of 'interesting' sample points can be returned. And I think that more high-level work can begin from there.
However, I get different results for the sample points
R, x, y = ring(['x', 'y'], QQ)
for point in recursive([x**2 + y**2 - 1, x - y], [x, y]):
print(point)
(-2, -3)
(-2, -1)
(-3/4, -1)
(-3/4, -11/16)
(-3/4, 0)
(-3/4, 1)
(0, -2)
(0, -1/2)
(0, 1/2)
(0, 2)
(3/4, -1)
(3/4, 0)
(3/4, 11/16)
(3/4, 1)
(2, 1)
(2, 3)
https://www.desmos.com/calculator/dxi1kqm9j5
for point in recursive([x**2 + y**2 - 7, x + y - 2, x**2 + y - 10], [x, y]):
print(point)
(-3, 0)
(-3, 3)
(-3, 6)
(-5/2, -1)
(-5/2, 0)
(-5/2, 2)
(-5/2, 4)
(-5/2, 5)
(-2, -2)
(-2, 0)
(-2, 2)
(-2, 5)
(-2, 7)
(1, -3)
(1, -1)
(1, 2)
(1, 5)
(1, 10)
(21/8, -1)
(21/8, -1/2)
(21/8, 0)
(21/8, 2)
(21/8, 4)
(3, -2)
(3, 0)
(3, 2)
(4, -7)
(4, -4)
(4, -1)
Looks good.
We can just use discriminant rather than resultant of p and p.diff. I just did that because it implicitly includes the LC.
There seems to be a problem with the types returned somewhere:
In [1]: a, b, c, d, e = symbols('a, b, c, d, e')
In [2]: p = Poly([1, a, b, c, d, e], x).as_expr()
In [3]: p1, p2 = p.subs(x, I*x).as_poly(I).all_coeffs()
In [4]: eqs = [LC(p2, x), resultant(p1, p2, x)]
In [5]: R, *symsp = ring('a, b, c, d, e', QQ)
In [6]: eqsp = [R(eq) for eq in eqs]
In [7]: edit find2.py
Editing... done. Executing edited code...
In [8]: for point in recursive(eqsp, symsp): print(point)
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
Cell In[8], line 1
----> 1 for point in recursive(eqsp, symsp): print(point)
File ~/current/active/sympy/find2.py:167, in recursive(polys, vars)
165 yield (root,)
166 return
--> 167 ps = proj(sfrp(polys), vars[-1])
168 for roots in recursive(ps, vars[:-1]):
169 for root in between_real_roots(polys_subs(polys, vars[:-1], roots)):
File ~/current/active/sympy/find2.py:156, in proj(gs, x)
154 """Projection of the polynomials to the variable x."""
155 c = {lc_wrt(p, x) for p in gs}
--> 156 d = {disc_wrt(p, x) for p in gs}
157 r = {res_wrt(p, q, x) for p, q in combinations(gs, 2)}
158 return c.union(d, r)
File ~/current/active/sympy/find2.py:156, in <setcomp>(.0)
154 """Projection of the polynomials to the variable x."""
155 c = {lc_wrt(p, x) for p in gs}
--> 156 d = {disc_wrt(p, x) for p in gs}
157 r = {res_wrt(p, q, x) for p, q in combinations(gs, 2)}
158 return c.union(d, r)
File ~/current/active/sympy/find2.py:30, in disc_wrt(p, x)
28 c = lc_wrt(p, x)
29 res = res_wrt(p, p.diff(x), x)
---> 30 return s * res // c
TypeError: unsupported operand type(s) for //: 'int' and 'PolyElement'
This is a simple implementation of the operation described in https://github.com/sympy/sympy/issues/26162#issuecomment-1925752873.
This is essentially a simplified version of a cylindrical algebraic decomposition but with one major restriction which is that it is only for strict inequalities and not equations or non-strict inequalities. This restriction simplifies the problem massively by allowing to work mostly only with rational numbers. Regardless of this limitation I still think that a function that can do this would be a very useful addition to SymPy.
Given a set of polynomials the method below finds example points giving rise to all combinations of the polynomials having different signs:
This is useful for several reasons. One reason is that we can use the numerical values to check some condition that is known to depend only on the signs of the polynomials. Another reason is that this method already proves that the inequalities are or are not satisfiable. The output can also be viewed as a truth table that can be used to determine whether some inequalities imply others etc so you could use this to simplify a system of inequalities or to do something like
ask(x**2+y**2 > 7, [x+y>2, x**2+y>10])
e.g.:This shows that
(x + y - 2 > 0) & (x**2 + y - 10 > 0) --> (x**2 + y**2 - 7 > 0)
.This is the code. It likely has bugs and can certainly be made more efficient. I just wanted to put this here for discussion for now so that the code can be improved later: