Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination
This work addresses the problem of efficiently handling graph constraints in SAT solving for researchers and practitioners in formal verification and combinatorial optimization, though it is incremental as it builds on existing encoding techniques.
The authors tackled the problem of encoding acyclicity and reachability constraints in propositional formulas for sparse directed graphs by introducing methods based on vertex elimination graphs, which convert these constraints into standard propositional clauses usable with any SAT solver. Their empirical study showed that these methods outperform earlier encodings and specialized solvers like GraphSAT, particularly for sparse graphs.
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.