# A Dynamic MaxSAT-based Approach to Directed Feedback Vertex Sets

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Nov 2022.

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

- [Approaching the Source of Symbol Grounding with Confluent Reductions of Abstract Meaning Representation Directed Graphs](https://mlsanity.com/paper/2508.11068/) (2025)

## Abstract (arXiv)

We propose a new approach to the Directed Feedback Vertex Set Problem (DFVSP), where the input is a directed graph and the solution is a minimum set of vertices whose removal makes the graph acyclic. Our approach, implemented in the solver DAGer, is based on two novel contributions: Firstly, we add a wide range of data reductions that are partially inspired by reductions for the similar vertex cover problem. For this, we give a theoretical basis for lifting reductions from vertex cover to DFVSP but also incorporate novel ideas into strictly more general and new DFVSP reductions. Secondly, we propose dynamically encoding DFVSP in propositional logic using cycle propagation for improved performance. Cycle propagation builds on the idea that already a limited number of the constraints in a propositional encoding is usually sufficient for finding an optimal solution. Our algorithm, therefore, starts with a small number of constraints and cycle propagation adds additional constraints when necessary. We propose an efficient integration of cycle propagation into the workflow of MaxSAT solvers, further improving the performance of our algorithm. Our extensive experimental evaluation shows that DAGer significantly outperforms the state-of-the-art solvers and that our data reductions alone directly solve many of the instances.