# Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination

arXiv: https://arxiv.org/abs/2105.12908 · HTML: https://mlsanity.com/paper/2105.12908/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 23 references that are in the map.
- First posted on arXiv 27 May 2021.

## Builds on (most cited first, 5 of 5)

- [A Symbolic SAT-based Algorithm for Almost-sure Reachability with Small Strategies in POMDPs](https://mlsanity.com/paper/1511.08456/) (2015)
- [Turbocharging Treewidth-Bounded Bayesian Network Structure Learning](https://mlsanity.com/paper/2006.13843/) (2020)
- [Learning Chordal Markov Networks by Constraint Satisfaction](https://mlsanity.com/paper/1310.0927/) (2013)
- [Computing All-Pairs Shortest Paths by Leveraging Low Treewidth](https://mlsanity.com/paper/1401.4609/) (2014)
- [On the Quest for an Acyclic Graph](https://mlsanity.com/paper/1708.01745/) (2017)

## Built on by (most cited first, 3 of 3)

- [The Complexity of Why-Provenance for Datalog Queries](https://mlsanity.com/paper/2303.12773/) (2023)
- [Capturing (Optimal) Relaxed Plans with Stable and Supported Models of Logic Programs](https://mlsanity.com/paper/2306.05069/) (2023)
- [A Good Snowman is Hard to Plan](https://mlsanity.com/paper/2310.01471/) (2023)

## Abstract (arXiv)

We introduce novel methods for encoding acyclicity and s-t-reachability constraints for propositional formulas with underlying directed graphs. They are based on vertex elimination graphs, which makes them suitable for cases where the underlying graph is sparse. 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 can outperform both earlier encodings of these constraints as well as GraphSAT, particularly when underlying graphs are sparse.