This problem can be considered as an instance of the more general SAT problem, in which you're trying to find a satisfying assignment to a predicate. You might want to give that approach a try, though it does require changes in representation. Here's a *very* simple example:
Prelude> :m Data.SBV
Prelude Data.SBV> let f (x, y, z) = 0 .<= x &&& y .>= 2 &&& z .<= x+(y::SInteger)
Prelude Data.SBV> sat f
Satisfiable. Model:
s0 = 0 :: Integer
s1 = 2 :: Integer
s2 = 2 :: Integer
Your "f" is probably going to be much more complicated, but if you can afford to move to symbolic types, then SBV can bridge the gap and a SAT/SMT solver can give you the required points. Or tell you if there isn't any, like in the following example:
Prelude Data.SBV> sat $ \x y -> x .> y &&& x .< (y::SInteger)
Unsatisfiable
-Levent.