Abstract: We introduce novel methods for encoding acyclicity and s-t-reachability constraints for propositional formulas with underlying directed graphs. They are based on \emph{vertex elimination graphs}, which makes them suitable for cases where the underlying graph has a low \emph{directed elimination width}. In contrast to solvers with ad hoc constraint propagators for acyclicity and reachability constraints such as GraphSAT, our methods encode these constraints as standard propositional clauses, making them directly applicable with any SAT solver. An empirical study demonstrates that our methods together with an efficient SAT solver do often outperform both earlier encodings of these constraints as well as GraphSAT, particularly when underlying graphs have low directed elimination width.