Clarify optimizer guarantees

[hexagonrecursion]

To me as a layperson from outside your theoretical field the phrasing such as "model meets the objectives", "solves objectives" and "check satisfiability while optimizing objective functions" sounds ambiguous. To me this phrasing sounds like it could mean either of the two options:

1. Best effort - try to find an optimal solution, but it's ok if you find a sub-optimal solution or if you can't prove that there are no better solutions
2. All or nothing - either find an optimal solution and prove that it is optimal or fail

From the C API documentation and from several bug reports about non-optimal solutions I have inferred that the second interpretation is correct.

Here is my attempt to document the guarantees given by the optimizer interface

The word "optimal" sounds unambiguous to me. If something is sub-optimal than it is not optimal. The words "optimize", "optimization" and "objective" on the other hand often do not imply that the result is perfect.

[hexagonrecursion]

I'll think about this. Especially about the "Governing Law/Jurisdiction" section.

[hexagonrecursion]

@microsoft-github-policy-service agree

[hexagonrecursion]

Authorship clarification "Check consistency and produce optimal values." is copy-paste from your C API docs, "is optimal" is my own addition.