Relaxation Algorithm

The solver provides a special algorithm for constraints of the form

where θ_{k}() is either of the form ∑
_{i}c_{i}a_{i} + d_{i} = 0, or of the form

where ϕ_{i}(x) and ψ(x) may be an arbitrary Boolean combination of constraints,
but they are only allowed to contain the variables .

For using this algorithm, RSolver has to be called using the parameters -f Sample -p DeductionStrategy RelaxationUniv, and the existential quantifier has to be written in the variant EXISTS*. See the examples in the directory examples/relax of the distribution.

The corresponding algorithm exploits the fact that the a_{i} only occur linearly.
This allows solving the problem using linear-programming relaxations [16].