Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Address non-feasibility in solveset - current code breaks solveset #19189

Merged
merged 6 commits into from Sep 5, 2020

Conversation

nsfinkelstein
Copy link

@nsfinkelstein nsfinkelstein commented Apr 25, 2020

Brief description of what is fixed or changed

The _solve_using_known_values function calls the add_intersection_complement function with potential solutions that may be infeasible, such that the feasible region for a possible parameter might be the emptyset.

The current code adds a "result" that is an empty dictionary to the result list. This causes key-errors downstream, when code in _solve_using_known_values tries to index into that empty dictionary.

This pull request changes the code such that if any symbol has an empty feasible region in a solution, that solution is recognized as non-viable, and, it is "removed" from the results list (instead of being added as an empty dictionary).

Other comments

Here is a example of the bug:

import sympy as sy
α00, α01, α10, α11, λ0, λ1, λ2, λ3, μ0, μ1, μ2, μ3, μ4, μ5, μ6, μ7, ψ00, ψ01, ψ10, ψ11, ϕ00, ϕ01, ϕ10, ϕ11 = sy.symbols(
    'α00, α01, α10, α11, λ0, λ1, λ2, λ3, μ0, μ1, μ2, μ3, μ4, μ5, μ6, μ7, ψ00, ψ01, ψ10, ψ11, ϕ00, ϕ01, ϕ10, ϕ11'
)
solvefor = [ϕ00, ϕ01, ϕ10, ϕ11, ψ00, ψ01, ψ10, ψ11, μ0, μ1, μ3, λ0, λ1, λ2, λ3]
system = [
    -λ0 * ψ00 - λ1 * ψ01 + μ0 + ψ00 + ψ01,
    -λ0 * ψ10 - λ1 * ψ11 + μ1,
    -λ2 * ψ00 - λ3 * ψ01 + ψ00 + ψ01,
    -λ2 * ψ10 - λ3 * ψ11 + μ3,
    -λ0 * ϕ00 - λ2 * ϕ10 + ϕ00 + ϕ10,
    -λ1 * ϕ00 - λ3 * ϕ10 + ϕ00 + ϕ10,
    -λ0 * ϕ01 - λ2 * ϕ11,
    -λ1 * ϕ01 - λ3 * ϕ11,
    -α00 + ψ00 * ϕ00 + ψ10 * ϕ01,
    -α01 + ψ01 * ϕ00 + ψ11 * ϕ01,
    -α10 + ψ00 * ϕ10 + ψ10 * ϕ11,
    -α11 + ψ01 * ϕ10 + ψ11 * ϕ11,
    -μ0 * ϕ00,
    -μ1 * ϕ01,
    -μ2 * ϕ10,
    -μ3 * ϕ11,
    -μ4 * ψ00,
    -μ5 * ψ01,
    -μ6 * ψ10,
    -μ7 * ψ11,
    μ2,
    μ4,
    μ5,
    μ6,
    μ7
]

solution = sy.nonlinsolve(system, solvefor)
sy.pprint(solution)

Under the old code, this would throw the following:

Traceback (most recent call last):
  File "sympybug.py", line 34, in <module>
    solution = sy.nonlinsolve(system, solvefor)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3435, in nonlinsolve
    polys_expr + nonpolys, symbols, exclude=denominators)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3147, in substitution
    temp = [r[symb] for symb in all_symbols]
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3147, in <listcomp>
    temp = [r[symb] for symb in all_symbols]
KeyError: ϕ00

Under the new code, the output is:

⎧                                                           ⎛                                
⎨(0, {ϕ01} \ {0}, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, λ2, λ3), ⎜0, {ϕ01} \ {0}, 0, ϕ11, 0, 0, 0,
⎩                                                           ⎝                                

                -λ3⋅ϕ11   -ϕ01     ⎞  ⎛                                             -λ2⋅ϕ11  
 0, 0, 0, 0, 1, ────────, ─────, λ3⎟, ⎜0, {ϕ01} \ {0}, 0, ϕ11, 0, 0, 0, 0, 0, 0, 0, ────────,
                  ϕ01      ϕ11     ⎠  ⎝                                               ϕ01    

 -λ3⋅ϕ11         ⎞  ⎛                                                     -ϕ01   -ϕ01 ⎞⎫
 ────────, λ2, λ3⎟, ⎜ϕ00, {ϕ01} \ {0}, 0, ϕ11, 0, 0, 0, 0, 0, 0, 0, 1, 1, ─────, ─────⎟⎬
   ϕ01           ⎠  ⎝                                                      ϕ11    ϕ11 ⎠⎭

Thanks very much

  • solvers
    • Fix bug in nonlinsolve leading to key-error

@sympy-bot
Copy link

sympy-bot commented Apr 25, 2020

Hi, I am the SymPy bot (v160). I'm here to help you write a release notes entry. Please read the guide on how to write release notes.

Your release notes are in good order.

Here is what the release notes will look like:

This will be added to https://github.com/sympy/sympy/wiki/Release-Notes-for-1.7.

Note: This comment will be updated with the latest check if you edit the pull request. You need to reload the page to see it.

Click here to see the pull request description that was parsed.

## Brief description of what is fixed or changed

The `_solve_using_known_values` function calls the `add_intersection_complement` function with potential solutions that may be infeasible, such that the feasible region for a possible parameter might be the emptyset.

The current code adds a "result" that is an empty dictionary to the result list. This causes key-errors downstream, when code in `_solve_using_known_values` tries to index into that empty dictionary.

This pull request changes the code such that if any symbol has an empty feasible region in a solution, that solution is recognized as non-viable, and, it is "removed" from the results list (instead of being added as an empty dictionary).

#### Other comments

Here is a example of the bug:

```py
import sympy as sy
α00, α01, α10, α11, λ0, λ1, λ2, λ3, μ0, μ1, μ2, μ3, μ4, μ5, μ6, μ7, ψ00, ψ01, ψ10, ψ11, ϕ00, ϕ01, ϕ10, ϕ11 = sy.symbols(
    'α00, α01, α10, α11, λ0, λ1, λ2, λ3, μ0, μ1, μ2, μ3, μ4, μ5, μ6, μ7, ψ00, ψ01, ψ10, ψ11, ϕ00, ϕ01, ϕ10, ϕ11'
)
solvefor = [ϕ00, ϕ01, ϕ10, ϕ11, ψ00, ψ01, ψ10, ψ11, μ0, μ1, μ3, λ0, λ1, λ2, λ3]
system = [
    -λ0 * ψ00 - λ1 * ψ01 + μ0 + ψ00 + ψ01,
    -λ0 * ψ10 - λ1 * ψ11 + μ1,
    -λ2 * ψ00 - λ3 * ψ01 + ψ00 + ψ01,
    -λ2 * ψ10 - λ3 * ψ11 + μ3,
    -λ0 * ϕ00 - λ2 * ϕ10 + ϕ00 + ϕ10,
    -λ1 * ϕ00 - λ3 * ϕ10 + ϕ00 + ϕ10,
    -λ0 * ϕ01 - λ2 * ϕ11,
    -λ1 * ϕ01 - λ3 * ϕ11,
    -α00 + ψ00 * ϕ00 + ψ10 * ϕ01,
    -α01 + ψ01 * ϕ00 + ψ11 * ϕ01,
    -α10 + ψ00 * ϕ10 + ψ10 * ϕ11,
    -α11 + ψ01 * ϕ10 + ψ11 * ϕ11,
    -μ0 * ϕ00,
    -μ1 * ϕ01,
    -μ2 * ϕ10,
    -μ3 * ϕ11,
    -μ4 * ψ00,
    -μ5 * ψ01,
    -μ6 * ψ10,
    -μ7 * ψ11,
    μ2,
    μ4,
    μ5,
    μ6,
    μ7
]

solution = sy.nonlinsolve(system, solvefor)
sy.pprint(solution)
```

Under the old code, this would throw the following:
```
Traceback (most recent call last):
  File "sympybug.py", line 34, in <module>
    solution = sy.nonlinsolve(system, solvefor)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3435, in nonlinsolve
    polys_expr + nonpolys, symbols, exclude=denominators)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3147, in substitution
    temp = [r[symb] for symb in all_symbols]
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3147, in <listcomp>
    temp = [r[symb] for symb in all_symbols]
KeyError: ϕ00
```

Under the new code, the output is:

```
⎧                                                           ⎛                                
⎨(0, {ϕ01} \ {0}, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, λ2, λ3), ⎜0, {ϕ01} \ {0}, 0, ϕ11, 0, 0, 0,
⎩                                                           ⎝                                

                -λ3⋅ϕ11   -ϕ01     ⎞  ⎛                                             -λ2⋅ϕ11  
 0, 0, 0, 0, 1, ────────, ─────, λ3⎟, ⎜0, {ϕ01} \ {0}, 0, ϕ11, 0, 0, 0, 0, 0, 0, 0, ────────,
                  ϕ01      ϕ11     ⎠  ⎝                                               ϕ01    

 -λ3⋅ϕ11         ⎞  ⎛                                                     -ϕ01   -ϕ01 ⎞⎫
 ────────, λ2, λ3⎟, ⎜ϕ00, {ϕ01} \ {0}, 0, ϕ11, 0, 0, 0, 0, 0, 0, 0, 1, 1, ─────, ─────⎟⎬
   ϕ01           ⎠  ⎝                                                      ϕ11    ϕ11 ⎠⎭
```

Thanks very much

<!-- BEGIN RELEASE NOTES -->
* solvers
  * Fix bug in nonlinsolve leading to key-error
<!-- END RELEASE NOTES -->

Update

The release notes on the wiki have been updated.

@codecov
Copy link

codecov bot commented Apr 25, 2020

Codecov Report

Merging #19189 into master will decrease coverage by 0.052%.
The diff coverage is 100.000%.

@@              Coverage Diff              @@
##            master    #19189       +/-   ##
=============================================
- Coverage   75.666%   75.613%   -0.053%     
=============================================
  Files          651       652        +1     
  Lines       169336    169572      +236     
  Branches     39970     40010       +40     
=============================================
+ Hits        128131    128220       +89     
- Misses       35605     35736      +131     
- Partials      5600      5616       +16     

@oscarbenjamin
Copy link
Contributor

Thanks for this.

Can you add an example that demonstrates the bug to the tests?

Maybe it would be simpler just to check if res_copy is an empty dict before appending. It could also be set to None rather than an empty dict if the value is just used as a flag.

@nsfinkelstein
Copy link
Author

Thank you for the quick response.

I have changed the feasible flag into a None assignment and check, as per your suggestion. I've also added the above example as a test, and confirmed that it fails on the master branch and passes with the new code.

Thanks very much

@oscarbenjamin
Copy link
Contributor

Is the given solution correct? If so it would be good to assert that we get that solution in the tests e.g.:

sol = ...
assert nonlinsolve(...) == sol

You can use repr to see how to represent the solution directly.

The tests have failed because of the use of unicode characters. It is possible to make them pass by adding an encoding header and whitelisting this file. I think it would be better in this case just to use ASCII for the symbol names because it makes it easier for people to edit the file.

@nsfinkelstein
Copy link
Author

Thanks - I can use ascii characters.

Actually, the solutions are incorrect. Note for example the equation -α10 + ψ00 * ϕ10 + ψ10 * ϕ11 in the system. The first solution in the set has all variables other than α10 (which was not solved for) equal to 0. Then clearly this equation is not equal to 0 at the first solution - it is equal to -α10.

However, I can see no way this change could possibly have introduced this bug. I've observed similar issues before this change as well.

How should this be handled? As you say, it seems incorrect to assert the solution is something it is not.

Thanks very much.

@oscarbenjamin
Copy link
Contributor

How should this be handled? As you say, it seems incorrect to assert the solution is something it is not.

I think the best way is to add a test asserting that the solution is not what is currently returned. That test will obviously fail but you can mark the test as XFAIL. That way if something changes in future and the test begins to pass someone will be alerted to the XPASS and can investigate (the solution might still be incorrect but someone can at least look).

You could also open a github issue to describe the incorrect answer and then put a url for the issue in a code comment of the XFAIL test so anyone looking at it can see the discussion.

@oscarbenjamin
Copy link
Contributor

If you can come up with an example where sympy actually gets the correct result then that's also good :)

I see that for the example above solve gives an empty list:

In [2]: solve(system, solvefor)                                                                                                                
Out[2]: []

There can be differences in the way that solve and nonlinsolve handle "overdetermined" systems. For example if μ4 does not equal zero then there are no solutions. I think that solve will ignore cases like that on their own but not necessarily when part of the system like [x = 0, x = μ4] where x is to be solved for but μ4 is not.

I have discussed ideas about this in #16861

@oscarbenjamin
Copy link
Contributor

The Groebner basis for the system has each individual unknown as a generator:

In [18]: system                                                                                                                                
Out[18]: 
[-λ0ψ00 - λ1ψ01 + μ0 + ψ00 + ψ01, -λ0ψ10 - λ1ψ11 + μ1, -λ2ψ00 - λ3ψ01 + ψ00 + ψ01, -λ2ψ10 - λ3ψ11 + μ3, -λ0ϕ00 - λ2ϕ10 + ϕ00 + ϕ10,
 -λ1ϕ00 - λ3ϕ10 + ϕ00 + ϕ10, -λ0ϕ01 - λ2ϕ11, -λ1ϕ01 - λ3ϕ11, -α00 + ψ00ϕ00 + ψ10ϕ01, -α01 + ψ01ϕ00 + ψ11ϕ01, -α10 + ψ00ϕ10 + ψ10ϕ
11, -α11 + ψ01ϕ10 + ψ11ϕ11, -μ0ϕ00, -μ1ϕ01, -μ2ϕ10, -μ3ϕ11, -μ4ψ00, -μ5ψ01, -μ6ψ10, -μ7ψ11, μ2, μ4, μ5, μ6, μ7]

In [19]: solvefor                                                                                                                              
Out[19]: [ϕ00, ϕ01, ϕ10, ϕ11, ψ00, ψ01, ψ10, ψ11, μ0, μ1, μ3, λ0, λ1, λ2, λ3]

In [20]: groebner(system, solvefor)                                                                                                            
Out[20]: 
GroebnerBasis([1], ϕ00, ϕ01, ϕ10, ϕ11, ψ00, ψ01, ψ10, ψ11, μ0, μ1, μ3, λ0, λ1, λ2, λ3, domain=ℤ[α00, α01, α10, α11, μ2, μ4, μ5, μ6, μ7], orde
r=lex)

I think this implies that the only possible solution would be one in which every unknown is zero in which case the system becomes:

In [21]: rep = {x: 0 for x in solvefor}                                                                                                        

In [22]: for e in system: pprint(e.subs(rep))                                                                                                  
0
0
0
0
0
0
0
0
-α00
-α01
-α10
-α11
0
0
0
0
0
0
0
0
μ2
μ4
μ5
μ6
μ7

So maybe the only possible solution is the trivial solution and it only exists if these parameters are all zero.

@nsfinkelstein
Copy link
Author

nsfinkelstein commented Apr 25, 2020

Thank you, that is very interesting.

If I follow, this implies that were I to solve for the system all the variables used in it, I should get a solution where all variables turn out to be zeros. This is not quite what I see.

With nonlinsolve I get the following error:

Traceback (most recent call last):
  File "sympybug.py", line 35, in <module>
    solution = sy.nonlinsolve(system, symbols)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3438, in nonlinsolve
    polys_expr + nonpolys, symbols, exclude=denominators)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3103, in substitution
    old_result, solveset_real)
  File "/home/noam/projects/sympy/sympy/solvers/solveset.py", line 3076, in _solve_using_known_values
    rnew[k] = v.subs(sym, sol)
  File "/home/noam/projects/sympy/sympy/core/basic.py", line 971, in subs
    rv = rv._subs(old, new, **kwargs)
  File "/home/noam/projects/sympy/sympy/core/cache.py", line 94, in wrapper
    retval = cfunc(*args, **kwargs)
  File "/home/noam/projects/sympy/sympy/core/basic.py", line 1085, in _subs
    rv = fallback(self, old, new)
  File "/home/noam/projects/sympy/sympy/core/basic.py", line 1057, in fallback
    arg = arg._subs(old, new, **hints)
  File "/home/noam/projects/sympy/sympy/core/cache.py", line 94, in wrapper
    retval = cfunc(*args, **kwargs)
  File "/home/noam/projects/sympy/sympy/core/basic.py", line 1083, in _subs
    rv = self._eval_subs(old, new)
  File "/home/noam/projects/sympy/sympy/core/power.py", line 804, in _eval_subs
    return new**self.exp._subs(old, new)
  File "/home/noam/projects/sympy/sympy/core/decorators.py", line 251, in _func
    return func(self, other)
  File "/home/noam/projects/sympy/sympy/sets/sets.py", line 660, in __pow__
    raise ValueError("%s: Exponent must be a positive Integer" % exp)
ValueError: -1: Exponent must be a positive Integer

Using solve, with dict=True, I obtain the following solutions.

⎡⎧                                                                                                       ϕ11⋅
⎢⎨α00: -ψ01⋅ϕ00 - ψ11⋅ϕ01, α01: ψ01⋅ϕ00 + ψ11⋅ϕ01, α10: -ψ01⋅ϕ10 - ψ11⋅ϕ11, α11: ψ01⋅ϕ10 + ψ11⋅ϕ11, λ0: ─────
⎣⎩                                                                                                      ϕ00⋅ϕ

(ϕ00 + ϕ10)        ϕ11⋅(ϕ00 + ϕ10)       -ϕ01⋅(ϕ00 + ϕ10)       -ϕ01⋅(ϕ00 + ϕ10)                             
────────────, λ1: ─────────────────, λ2: ─────────────────, λ3: ─────────────────, μ0: 0, μ1: 0, μ2: 0, μ3: 0
11 - ϕ01⋅ϕ10      ϕ00⋅ϕ11 - ϕ01⋅ϕ10      ϕ00⋅ϕ11 - ϕ01⋅ϕ10      ϕ00⋅ϕ11 - ϕ01⋅ϕ10                            

                                                  ⎫                                                          
, μ4: 0, μ5: 0, μ6: 0, μ7: 0, ψ00: -ψ01, ψ10: -ψ11⎬, {α00: ψ01⋅ϕ10 + ψ10⋅ϕ01, α01: -ψ01⋅ϕ10 + ψ11⋅ϕ01, α10: -
                                                  ⎭                                                          

                                                                                                             
ψ01⋅ϕ10 + ψ10⋅ϕ11, α11: ψ01⋅ϕ10 + ψ11⋅ϕ11, λ0: 0, λ1: 0, λ2: 0, λ3: 0, μ0: 0, μ1: 0, μ2: 0, μ3: 0, μ4: 0, μ5:
                                                                                                             

                                         ⎧                                                                   
 0, μ6: 0, μ7: 0, ψ00: -ψ01, ϕ00: -ϕ10}, ⎨α00: -ψ01⋅ϕ00 - ψ11⋅ϕ01, α01: ψ01⋅ϕ00 + ψ11⋅ϕ01, α10: -ψ01⋅ϕ10, α11
                                         ⎩                                                                   

                             ϕ00 + ϕ10      ϕ00 + ϕ10                                                        
: ψ01⋅ϕ10, λ0: 0, λ1: 0, λ2: ─────────, λ3: ─────────, μ0: 0, μ1: 0, μ2: 0, μ3: 0, μ4: 0, μ5: 0, μ6: 0, μ7: 0
                                ϕ10            ϕ10                                                           

                              ⎫                                                                              
, ψ00: -ψ01, ψ10: -ψ11, ϕ11: 0⎬, {α00: ψ01⋅ϕ10 + ψ10⋅ϕ01, α01: -ψ01⋅ϕ10 + ψ11⋅ϕ01, α10: -ψ01⋅ϕ10, α11: ψ01⋅ϕ1
                              ⎭                                                                              

                                                                                                             
0, λ0: 0, λ1: 0, λ2: 0, λ3: 0, μ0: 0, μ1: 0, μ2: 0, μ3: 0, μ4: 0, μ5: 0, μ6: 0, μ7: 0, ψ00: -ψ01, ϕ00: -ϕ10, 
                                                                                                             

       ⎤
ϕ11: 0}⎥
       ⎦

This leaves me unsure of which assertion to make.

For completeness, the code used to obtain these results is below, with the only change between the first and second being solve -> nonlinsolve:

import sympy as sy
symbols = sy.symbols(
    'α00, α01, α10, α11, λ0, λ1, λ2, λ3, μ0, μ1, μ2, μ3, μ4, μ5, μ6, μ7, ψ00, ψ01, ψ10, ψ11, ϕ00, ϕ01, ϕ10, ϕ11'
)
α00, α01, α10, α11, λ0, λ1, λ2, λ3, μ0, μ1, μ2, μ3, μ4, μ5, μ6, μ7, ψ00, ψ01, ψ10, ψ11, ϕ00, ϕ01, ϕ10, ϕ11 = symbols
system = [
    -λ0 * ψ00 - λ1 * ψ01 + μ0 + ψ00 + ψ01,
    -λ0 * ψ10 - λ1 * ψ11 + μ1,
    -λ2 * ψ00 - λ3 * ψ01 + ψ00 + ψ01,
    -λ2 * ψ10 - λ3 * ψ11 + μ3,
    -λ0 * ϕ00 - λ2 * ϕ10 + ϕ00 + ϕ10,
    -λ1 * ϕ00 - λ3 * ϕ10 + ϕ00 + ϕ10,
    -λ0 * ϕ01 - λ2 * ϕ11,
    -λ1 * ϕ01 - λ3 * ϕ11,
    -α00 + ψ00 * ϕ00 + ψ10 * ϕ01,
    -α01 + ψ01 * ϕ00 + ψ11 * ϕ01,
    -α10 + ψ00 * ϕ10 + ψ10 * ϕ11,
    -α11 + ψ01 * ϕ10 + ψ11 * ϕ11,
    -μ0 * ϕ00,
    -μ1 * ϕ01,
    -μ2 * ϕ10,
    -μ3 * ϕ11,
    -μ4 * ψ00,
    -μ5 * ψ01,
    -μ6 * ψ10,
    -μ7 * ψ11,
    μ2,
    μ4,
    μ5,
    μ6,
    μ7
]

solution = sy.solve(system, symbols, dict=True)
sy.pprint(solution)

Thanks very much.

@oscarbenjamin
Copy link
Contributor

Okay let's work this manually a bit.

  1. We know mu2,4,5,6,7 have to be zero so we can remove them from the picture.
  2. That also removes equations like mu2*phi10
  3. The a00 etc equations just tell us what a00 etc are so they can be removed.

That leaves us with:

system = [
    -λ0 * ψ00 - λ1 * ψ01 + μ0 + ψ00 + ψ01,
    -λ0 * ψ10 - λ1 * ψ11 + μ1,
    -λ2 * ψ00 - λ3 * ψ01 + ψ00 + ψ01,
    -λ2 * ψ10 - λ3 * ψ11 + μ3,
    -λ0 * ϕ00 - λ2 * ϕ10 + ϕ00 + ϕ10,
    -λ1 * ϕ00 - λ3 * ϕ10 + ϕ00 + ϕ10,
    -λ0 * ϕ01 - λ2 * ϕ11,
    -λ1 * ϕ01 - λ3 * ϕ11,
    -μ0 * ϕ00,
    -μ1 * ϕ01,
    -μ3 * ϕ11,
]

The equations at the bottom imply 8 possibilities (i.e. mu0 = 0 or phi00=0 etc). Taking one of these we can have mu0 = mu1 = mu3 = 0 which leads to

system = [
    -λ0 * ψ00 - λ1 * ψ01 + ψ00 + ψ01,
    -λ0 * ψ10 - λ1 * ψ11,
    -λ2 * ψ00 - λ3 * ψ01 + ψ00 + ψ01,
    -λ2 * ψ10 - λ3 * ψ11,
    -λ0 * ϕ00 - λ2 * ϕ10 + ϕ00 + ϕ10,
    -λ1 * ϕ00 - λ3 * ϕ10 + ϕ00 + ϕ10,
    -λ0 * ϕ01 - λ2 * ϕ11,
    -λ1 * ϕ01 - λ3 * ϕ11,
]

For this example nonlinsolve gives a different error.

TypeError: Argument of Integer should be of numeric type, got -oo.

With solve we get

[{ψ00: 0, ψ01: 0, ψ10: 0, ψ11: 0, ϕ00: 0, ϕ01: 0, ϕ10: 0, ϕ11: 0}]

which implies all phi and psi have to be zero but the lambdas can be anything. Indeed it's not hard to see that that is a valid family of solutions.

It looks like solve has missed a solution family though. We could also have all the lambdas be zero and then we get a system with the solution

[{ψ00: -ψ01, ϕ00: -ϕ10}]

which represents a different infinite family of solutions.

Obviously I was wrong in my interpretation of the groebner basis...

@nsfinkelstein
Copy link
Author

Thanks for working that out; I appreciate it! That certainly clarifies things for this system.

Two concluding questions:

i) To complete this pull request, what would you suggest for the assertion in the test, given all of the above?

ii) Could you point me to any materials about whether there are classes of systems for which the solvers in sympy are guaranteed to be sound and complete? Similarly, do you have suggestions for reading on the theory behind solvers of this sort in general?

Thanks very much

@oscarbenjamin
Copy link
Contributor

For now I would just make a test that asserts that we don't get the current incorrect output. Then if anything happens to change so that we start to see a different result the test can be updated. It's important to make sure that the comments on the test explain why you are doing that and clearly link to the discussion on github. Ideally create a new issue so that discussion can continue there after this PR is merged.

I can't say whether the solvers are guaranteed to be sound and complete in any particular case. It would be impossible to prove that kind of thing anyway given that there is always the possibility of bugs. When it comes to multivariate systems of polynomials I'm not even sure which classes are guaranteed to be solvable anyway. I imagine your example here is fully solvable but I'm sure it's not hard to construct examples that can't possibly be solvable in any normal kind of closed form.

It is intended that solveset should give formally correct results. However even solveset does not handle conditionally existent solutions (see #16861). More importantly for your case here solveset only handles univariate equations.

@oscarbenjamin
Copy link
Contributor

This PR just needs an XFAIL test asserting that nonlinsolve does not return the solution that it currently returns i.e.

@XFAIL
def test_example_broken():
    eq = ...
    sol = ...
    syms = ...
    assert nonlinsolve(eq, syms) != sol

where sol is the result currently returned.

@nsfinkelstein
Copy link
Author

Thanks, and apologies for the delay.

@czgdp1807
Copy link
Member

@oscarbenjamin Is this good to go?

@oscarbenjamin
Copy link
Contributor

Yes. Thanks!

@oscarbenjamin oscarbenjamin merged commit ae158d8 into sympy:master Sep 5, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants