A SAT solver[1] can automatically figure out a range of acceptable solutions for your conditions. 'I want this goal, is there a way to make that happen?' Security people love this. SMT solvers are even crazier[2] and can automatically determine solutions to linear equations or inequalities (this comes in handy when analyzing loops). Z3 has an online version at [3].
Also, if you have a lot of nasty cascaded if-statements, a K-map[4] and espresso[5] can reduce those down to a minimal set of branches. Note that fewer branches means fewer branch prediction penalties, which means faster code!
