Chapter 5
Running RSolver

After starting the program, it asks for the inputs described in Chapter 3. Example inputs are contained in the distribution package. For controlling the solver further, one can use arguments when calling the program. These arguments are described when calling the solver by rsolver -h.

Note that the efficiency of the algorithm depends on the specific form, an input constraint is given. For example, a constraint of the form ∀x is handled in a different way than a constraint of the form ∀xϕ₁ ∧∀xϕ₂.

Usually (but not always!) the following transformations increase the efficiency:

• Rewriting constraint of the form ∀x , or ∃x to ∀xϕ₁ ∧∀xϕ₂, and ∃xϕ₁ ∨∃xϕ₂, respectively.
• Factoring terms as much as possible.
• Decomposing terms that can be written as f(g(x)) to a term f(y) with an additional constraint y = f(x).

Other possibilities of influencing the efficiency of RSolver  are the following:

• If the input has a large linear part it often helps to switch on linear relaxations using the flag -f LinearRelaxation.
• If the solver tends to produce many small boxes for a certain example, the use of mean value constraints [7], using the flag -f MeanValueConstraint, may help.

If RSolver  still cannot solve your problem, we strongly encourage you to contact us ( ). Your feedback will be essential for improving the software further.