Hello everyone!

Recently, I am working on a problem where I have systems of nonlinear strict inequalities, shell constraints (some points must lay on a sphere) and rational versions of Cos and Sin and I only want to check if constraints are valid or not. Moreover, I am rather interested in exact computations eg with CAD and fast answers (I need to check a lot of such systems). So far, I have tried some built in Mathematica 10.0.2 functions and all of them seems to failed to help me and I started to think that maybe I use these functions in a wrong way.

First of all, I've tried FindInstance with "simple" systems and then I tried to add a new constrains to see if it works. Surprisingly, even for few constraints it never gave me any solution if I asked it to give me only one. But if I changed n to be equal to 2 I got answers in few seconds.

system = {-(1/2) + x + (1 - \[Theta]^2)/(
   1 + \[Theta]^2) + (1 - (1 - \[Theta]^2)/(
      1 + \[Theta]^2)) \[Omega]1^2 > 0, 
 1/2 + x + (1 - \[Theta]^2)/(
   1 + \[Theta]^2) + (1 - (1 - \[Theta]^2)/(
      1 + \[Theta]^2)) \[Omega]1^2 > 
  0, -(1/2) + 
   y + (1 - (1 - \[Theta]^2)/(1 + \[Theta]^2)) \[Omega]1 \[Omega]2 + (
   2 \[Theta] \[Omega]3)/(1 + \[Theta]^2) < 0, 
 1/2 + y + (1 - (1 - \[Theta]^2)/(
      1 + \[Theta]^2)) \[Omega]1 \[Omega]2 + (2 \[Theta] \[Omega]3)/(
   1 + \[Theta]^2) > 
  0, -(1/2) + z - (2 \[Theta] \[Omega]2)/(
   1 + \[Theta]^2) + (1 - (1 - \[Theta]^2)/(
      1 + \[Theta]^2)) \[Omega]1 \[Omega]3 < 0, 
 1/2 + z - (2 \[Theta] \[Omega]2)/(
   1 + \[Theta]^2) + (1 - (1 - \[Theta]^2)/(
      1 + \[Theta]^2)) \[Omega]1 \[Omega]3 > 
  0, -\[Infinity] <= \[Theta] <= \[Infinity], {\[Omega]1, \[Omega]2, \
\[Omega]3} \[Element] Sphere[{0, 0, 0}, 1], 
 0 <= \[Omega]1 <= \[Omega]2 <= \[Omega]3 <= 1, -(1/2) < x < 1/
  2, -(1/2) < y < 1/2, -(1/2) < z < 1/2};
FindInstance[system, {\[Theta], \[Omega]1, \[Omega]2, \[Omega]3, x, y,
   z}, Reals, 1] (*change n to two to get the answer*)

Well, never the less it completely failed with more complex systems --- this one above it is only a test case. In more complex cases I have around 30 inequalities like these ones which contains Cos and Sin. Then, I have tried less suitable for me way where I used much faster numerical approach -- NMaximzie for a modified version of my systems. These modifications consist in replacing strict inequalities by inequalities and replacing zero in them by small epsilon. Nevertheless, I found that I cannot always trust obtained solutions even if error NMaximize::nosat does not appeared, etc.

Right now, I think that my problem is too huge for CAD like techniques therefore, I would like to ask you if you have any idea how I could break my problem down to be able to handle it with Mathematica. For instance, I had in mind to use Reduce as a reprocessing step and after that to combine obtained simpler inequalities, but I am not sure if I will gain something, after all. At the end, I have to say once again that I am not interested in any values of variables or functions itself. I want to know if constraints are valid or not and yes, I am aware that constraints satisfaction problem is NP complete, etc.

I hope I made myself clear. If not please do not hesitate to as me any question.

Thanks for any interest.