Propositional Encodings of Acyclicity and Reachability by Using Vertex Elimination
DOI:
https://doi.org/10.1609/aaai.v36i5.20530Keywords:
Knowledge Representation And Reasoning (KRR), Constraint Satisfaction And Optimization (CSO)Abstract
We introduce novel methods for encoding acyclicity and s-t-reachability constraints for propositional formulas with underlying directed graphs, based on vertex elimination graphs, which makes them suitable for cases where the underlying graph has a low directed elimination width. In contrast to solvers with ad hoc constraint propagators for graph 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 do often outperform both earlier encodings of these constraints as well as GraphSAT especially when underlying graphs have a low directed elimination width.Downloads
Published
2022-06-28
How to Cite
Rankooh, M. F., & Rintanen, J. (2022). Propositional Encodings of Acyclicity and Reachability by Using Vertex Elimination. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5), 5861-5868. https://doi.org/10.1609/aaai.v36i5.20530
Issue
Section
AAAI Technical Track on Knowledge Representation and Reasoning