A Dynamic MaxSAT-based Approach to Directed Feedback Vertex Sets

TL;DR

This paper introduces DAGer, a MaxSAT-based solver for the Directed Feedback Vertex Set Problem, utilizing novel data reductions and dynamic cycle propagation encoding to achieve superior performance and solve many instances directly.

Contribution

The paper presents new data reduction techniques inspired by vertex cover reductions and a dynamic encoding method using cycle propagation for the DFVSP, improving solver efficiency.

Findings

DAGer outperforms existing solvers on benchmark instances.

Data reductions alone solve many instances without full solving.

Dynamic cycle propagation enhances MaxSAT solver performance.

Abstract

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.