Relaxation Algorithm

Relaxation Algorithm

The solver provides a special algorithm for constraints of the form

(exist a in A) /\_k theta_k(a)

where theta_k(a) is either of the form SUM_i c_i a_i + d_i =0, or of the form

(forall x in X) (SUM_i a_iphi_i(x) <= 0 \/psi(x))

where phi_i(x) and psi(x) may be an arbitrary Boolean combination of constraints, but they are only allowed to contain the variables x.

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 [14].

Relaxation Algorithm