Symbolic Backward Reachability with Effectively Propositional Logic-Applications to Security Policy Analysis