software for numerical constraint satisfaction problems Let $m$ be an even integer greater than $8$. Is there any software I can use to determine for some small $m$ whether the following constraints on $t_0,\ldots,t_{m-1}$ and $w$ have solutions? 
$-\pi\leq t_r\leq\pi,\ r=0,\ldots,m-1,$
$0\leq w\leq\frac{1}{m},$
$\sum\limits_{j=1}^{2r-1}\cos(t_j+t_{2r-j})+\sum\limits_{j=2r+1}^{m-1}\cos(t_j+t_{2r+m-j})=2w\cos t_{2r},\ r=1,\ldots,\frac{m}{2}-1,$
$\sum\limits_{j=1}^{2r-1}\sin(t_j+t_{2r-j})+\sum\limits_{j=2r+1}^{m-1}\sin(t_j+t_{2r+m-j})=2w\sin t_{2r},\ r=1,\ldots,\frac{m}{2}-1,$
$t_r+t_{m-r}=0,\ r=1,\ldots,\frac{m}{2},$
$\cos(t_r+t_{\frac{m}{2}+r})=\cos(t_{2r}+rt_0),\ r=1,\ldots,\frac{m}{2}-1,$
$\sin(t_r+t_{\frac{m}{2}+r})=\sin(t_{2r}+rt_0),\ r=1,\ldots,\frac{m}{2}-1,$
$\cos(\frac{mt_0}{2})=1.$
 A: It seems to me that methods based on interval analysis are very efficient for solving hard constraints satisfaction problems. In particular, SIVIA (Set Inversion Via Interval Analysis) is an algorithm which can approximate using small "boxes" a subset of $\mathbb{R}^n$ satisfying a given set of constraints. It's a branch and bound algorithm, with quite a big complexity, but if the set is actually empty it can answer rather quickly. To be precise, it find an "inner" and an "outer" approximation of this set: if the outer approximation is empty, then your set is guaranteed to be empty, if the inner approximation is non empty then your set is guaranteed to be non empty, otherwise you can't tell and have to try with a higher precision, which increase the computing time and memory usage exponentially.
Unfortunately I'm not aware of an easy to use implementation of this algorithm. There are some links on Luc Jaulin's home page, and I know that there exists various interval libraries for most of programming language and numerical softwares.
