LRSlv is a logical relation solver that provides just enough functionality to be useful for solving boundary-crossing problems encountered in use by the CMSlv solver. We've also made use of it in our recent event-handling enhancements to the IDA solver (by User:Ksenija).
The ASCEND modeling language allows a logical boundary expression to be represented in terms of a combination of:
- Boolean variables.
- Boolean operators (see logical expression)
- The truth value of conditions expressed in term of real variables (see SATISFIED)
In LRSlv, we assume that we can explicitly evaluate all the boolean variables in some precedence order. In other words, LRSlv does not perform logical inference. Therefore, while finding the value of a boolean variable, we require the truth values of all the boolean variables and conditions on which each boolean variable depends to have been previously given or previously evaluated. Also, we assume that we can evaluate at any time the truth value of a condition expressed in terms of real variables. Both of our assumptions are met when the boundary crossing algorithm is being used to solve conditional models. LRSlv has also been attached as an external entity providing support to CMSlv as explained above.
Text of this page is derived from Vicente Rico-Ramirez' thesis, see our publications page for details.