Propositional encodings of acyclicity and reachability by using vertex elimination

Masood Feyzbakhsh Rankooh, Jussi Rintanen

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

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.
Original languageEnglish
Title of host publicationProceedings of the AAAI Conference on Artificial Intelligence
PublisherAAAI PRESS
Pages5861-5868
Number of pages8
ISBN (Print)978-1-57735-876-3
DOIs
Publication statusPublished - 28 Jun 2022
MoE publication typeA4 Article in a conference publication
EventAAAI Conference on Artificial Intelligence - virtual conference, Virtual, Online
Duration: 22 Feb 20221 Mar 2022
Conference number: 36
https://aaai.org/Conferences/AAAI-22/

Publication series

NameProceedings of the AAAI Conference on Artificial Intelligence
Number5
Volume36
ISSN (Print)2159-5399
ISSN (Electronic)2374-3468

Conference

ConferenceAAAI Conference on Artificial Intelligence
Abbreviated titleAAAI
CityVirtual, Online
Period22/02/202201/03/2022
Internet address

Fingerprint

Dive into the research topics of 'Propositional encodings of acyclicity and reachability by using vertex elimination'. Together they form a unique fingerprint.

Cite this