Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination

TL;DR

This paper presents new propositional encoding methods for acyclicity and reachability constraints using vertex elimination graphs, which are effective especially for sparse graphs and compatible with standard SAT solvers.

Contribution

The paper introduces novel encoding techniques based on vertex elimination graphs for acyclicity and reachability, improving performance on sparse graph problems.

Findings

Outperforms previous encodings and GraphSAT in sparse graph scenarios

Compatible with any SAT solver due to standard propositional clauses

Empirical results show efficiency gains with the proposed methods

Abstract

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.