基于顶点消除的无环性与可达性命题编码
人工智能
2021-05-28 v1
摘要
我们引入了对具有底层有向图的命题公式编码无环性和 s-t-可达性约束的新方法。它们基于顶点消除图，这使其适用于底层图稀疏的情况。与具有针对无环性和可达性约束的特设约束传播器的求解器（如 GraphSAT）不同，我们的方法将这些约束编码为标准命题子句，从而可直接用于任何 SAT 求解器。实证研究表明，我们的方法与高效的 SAT 求解器结合，能够胜过这些约束的早期编码以及 GraphSAT，尤其在底层图稀疏时。
引用
@article{arxiv.2105.12908,
title = {Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination},
author = {Masood Feyzbakhsh Rankooh and Jussi Rintanen},
journal= {arXiv preprint arXiv:2105.12908},
year = {2021}
}