ask: handle real linear inequalities

[TiloRC]

\

Here are some examples of what this PR enables ask to do:

x, y, z = symbols("x y z", real=True)
ask(x + y > 2, (x < 0) & (y <0)) # returns False instead of None
ask(x > z, (x > y) & (y > z)) # returns True instead of None

Unfortunately, I didn't have time to figure out how to handle infinite values, non-rational values, or complex variables. In the future, it might make sense to remove the lra_satask function and integrate the code from this pull request into satask once these cases are handled. Then again, one advantage of keeping it separate might be speed.

Currently, variables need to be specified to be real when they are created using the old assumptions. In other words, queries like ask(x > 0, (x > 1) & Q.real(x)) don't currently work.

Also, if a disallowed predicate such as Q.even is part of a query, that disables inequality handling. This could be changed fairly easily. However, I wanted to avoid slowing down queries that weren't primarily about inequalities.

logic/algorithms/lra_theory.py

Contains the LRASolver object which is designed to work in conjunction with a SAT solver to determine if a boolean formula involving inequalities is satisfiable or not.

sympy/assumptions/lra_satask.py

A function that's called in ask when satask returns None. It does some preprocessing so that all predicates are either Q.gt, Q.lt, Q.ge, Q.le or Q.eq and then makes some calls to satisfiable with use_lra_solver set to True. The use_lra_solver parameter tells satisfiable to use an LRASolver object in conjunction with the dpll2 algorithm.

Release Notes

• assumptions

  • Linear inequalities and equalities with real variables and rational coefficients are now understood by ask. For example, queries like ask(x > 1, x> 0) will no longer return None. However, x needs to be initialized as a real variable like this: x = symbols("x", real=True).

• logic

  • The dpll2 algorithm now has the option to use an LRA theory solver.

[TiloRC]

@asmeurer been a bit busy with college so I haven't worked on this in a few days much. How close do you think this PR is to merging?

As it stands there are only a few things I need to change:

• seems like I missed a few commented out pieces of code that should be deleted
• either get rid of the debug function or address comments about it and possibly improve it in other ways
• change some static methods to class methods

[asmeurer]

I think the only thing here is removing the extra print statements and debug code. I wouldn't worry about the staticmethod vs. classmethod thing.

[TiloRC]

I had an insight in the best way to make it so you don't have to explicitly specify variables are real.

Currently, the reason why you have to specify this is because subtleties of negating inequalities when variables are allowed to be complex; ~Q.gt(x, y) is not equivalent to Q.le(x,y) like it is when x and y must be reals.

My idea is to do things in a similar way to how I implemented the z3 wrapper. How that works is that a formula like (x > 0) & (x < 0) becomes b1 & b2 & (b1 $\implies$ (x > 0)) & (b2 $\implies$ (x < 0)).

This approach has the advantage that we can keep the implementation of the LRA Solver as close to the paper it was based on as possible. Also, this should have a speed advantage; the conflict clauses produced by the LRA solver will all be over the reals which will allow it to take advantage of the ~Q.gt(x, y) if an only if Q.le(x,y) property. Also this shouldn't be too bad to implement.

However, it might be better to do this in a follow up pull request.

[asmeurer]

Yes, let's implement ideas like that in a followup PR. I'd like to get this PR merged ASAP.

[asmeurer]

Currently, the reason why you have to specify this is because subtleties of negating inequalities when variables are allowed to be complex; ~Q.gt(x, y) is not equivalent to Q.le(x,y) like it is when x and y must be reals.

My idea is to do things in a similar way to how I implemented the z3 wrapper. How that works is that a formula like (x > 0) & (x < 0) becomes b1 & b2 & (b1 $\implies$ (x > 0)) & (b2 $\implies$ (x < 0)).

There might be more work required here because SymPy doesn't currently actually have (x > y) == False for non-real x and y. So there might be places that need to be adapted for that. Definitely the core inequality classes won't work (they raise an exception if they know the inputs aren't real), but it could be the case for the Q.le classes as well.

Although perhaps we could use a similar idea to make setting things as real with the new assumptions work. If x > y is an inequality in the input, add the fact (x > y) >> (Q.real(x) & Q.real(y)). If Q.real(x) and Q.real(y) are provided, this will effectively be ignored by the solver. However, if they are not provided, and the LRA solver produces a model where x > y is true, then ask will know that this is not possible if Q.real(x) can be False and so it will return None.

[TiloRC]

I think it was a mistake to allow predicates such as Q.complex, Q.transcendental, .. etc.

None of these predicates are actually safe to ignore. ~Q.complex(x) for example contradicts x > 0.

[oscarbenjamin]

~Q.complex(x) for example contradicts x > 0.

What is wrong with that?

Note that the reals are a subset of the complexes so real numbers are also complex:

In [102]: ask(Q.complex(1))
Out[102]: True

If ~Q.complex(x) means that x is not complex then it also means that x is not real.

The only object in SymPy for which x > 0 makes sense that is not complex is x = oo:

In [103]: ask(Q.complex(oo))
Out[103]: False

[TiloRC]

What is wrong with that?

I didn't consider infinite values would be considered non-complex so my original reasoning was bad. Regardless, I think it was still a mistake to allow these "benign" predicates.

Currently infinite values are not handled and all the variables must be real so ~Q.complex would be in conflict with this assumption. One of the goals of future work would be to handle infinite values.

[oscarbenjamin]

~Q.complex would be in conflict with this assumption.

I don't understand why this matters.

Why in the context of real linear inequalities do you need to care about someone using an assumption like ~Q.complex(x)?

Any time such an assumption is used real linear inequalities would not be applicable anyway.

[asmeurer]

Tilo is right here. The reason is that it was just ignoring these predicates entirely in lra_satask. But in the commit prior to 71a96b9, you would get things like:

>>> x = symbols('x', real=True)
>>> lra_satask((x > 0), ~Q.complex(x) & (x > 1))
True

which is wrong (and indeed ask() itself returns False because it never calls lra_satask in this case).

Actually I expect that my solution of adding the (x > y) >> (Q.real(x) & Q.real(y)) from #25544 (comment) would make this work. But let's do that in a follow up PR.

Any time such an assumption is used real linear inequalities would not be applicable anyway.

It's not that simple. Assumptions in the new assumptions can appear in arbitrary predicates. The ~Q.complex(x) assumption could appear in a way that makes it irrelevant to the actual deduction, or even in a way that makes it never possible to be true.

[asmeurer]

Regarding the debug code, you should also remove all the stuff that uses time (again, we can add benchmarks separately to https://github.com/sympy/sympy_benchmarks if you want).

Once that happens, I'm +1 to merging this.