[next] [prev] [prev-tail] [tail] [up]

Chapter 6
Relaxation Algorithm

The solver provides a special algorithm for constraints of the form

(∃⃗a ∈ A) ∧ θ (⃗a) k k

where θk(⃗a) is either of the form ∑ iciai + di = 0, or of the form

( ) (∀⃗x ∈ X ) ∑ a ϕ (⃗x) ≤ 0∨ ψ(⃗x) , i i i

where ϕi(x) and ψ(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 ai only occur linearly. This allows solving the problem using linear-programming relaxations [16].

[next] [prev] [prev-tail] [front] [up]