Document Open Access Logo

A Comparison of SAT Encodings for Acyclicity of Directed Graphs

Authors Neng-Fa Zhou, Ruiwei Wang, Roland H. C. Yap

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.30.pdf
  • Filesize: 0.6 MB
  • 9 pages

Document Identifiers

Author Details

Neng-Fa Zhou
  • The City University of New York, NY, USA
  • Relational AI, Berkeley, CA, USA
Ruiwei Wang
  • National University of Singapore, Singapore
Roland H. C. Yap
  • National University of Singapore, Singapore

Funding

R. Wang and R. H. C. Yap’s work was partly suported by NUS grant T1 251RES2219.

Cite AsGet BibTex

Neng-Fa Zhou, Ruiwei Wang, and Roland H. C. Yap. A Comparison of SAT Encodings for Acyclicity of Directed Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 30:1-30:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.30

Abstract

Many practical applications require synthesizing directed graphs that satisfy the acyclic constraint along with some side constraints. Several methods have been devised for encoding acyclicity of directed graphs into SAT, each of which is based on a cycle-detecting algorithm. The leaf-elimination encoding (LEE) repeatedly eliminates leaves from the graph, and judges the graph to be acyclic if the graph becomes empty at a certain time. The vertex-elimination encoding (VEE) exploits the property that the cyclicity of the resulting graph produced by the vertex-elimination operation entails the cyclicity of the original graph. While VEE is significantly smaller than the transitive-closure encoding for sparse graphs, it generates prohibitively large encodings for large dense graphs. This paper reports on a comparison study of four SAT encodings for acyclicity of directed graphs, namely, LEE using unary encoding for time variables (LEE-u), LEE using binary encoding for time variables (LEE-b), VEE, and a hybrid encoding which combines LEE-b and VEE. The results show that the hybrid encoding significantly outperforms the others.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Knowledge representation and reasoning
  • Computing methodologies → Planning and scheduling
  • Hardware → Theorem proving and SAT solving
Keywords
  • Graph constraints
  • Acyclic constraint
  • SAT encoding
  • Graph Synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jeremias Berg, Matti Järvisalo, and Brandon Malone. Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability. In Samuel Kaski and Jukka Corander, editors, Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, volume 33 of Proceedings of Machine Learning Research, pages 86-95, Reykjavik, Iceland, 22-25 April 2014. PMLR. URL: https://proceedings.mlr.press/v33/berg14.html.
  2. Jukka Corander, Tomi Janhunen, Jussi Rintanen, Henrik J. Nyman, and Johan Pensar. Learning chordal markov networks by constraint satisfaction. In Christopher J. C. Burges, Léon Bottou, Zoubin Ghahramani, and Kilian Q. Weinberger, editors, Advances in Neural Information Processing Systems 26: 27th Annual Conference on Neural Information Processing Systems 2013. Proceedings of a meeting held December 5-8, 2013, Lake Tahoe, Nevada, United States, pages 1349-1357, 2013. URL: https://proceedings.neurips.cc/paper/2013/hash/c06d06da9666a219db15cf575aff2824-Abstract.html.
  3. Johan de Kleer. A comparison of ATMS and CSP techniques. In N. S. Sridharan, editor, Proceedings of the 11th International Joint Conference on Artificial Intelligence. Detroit, MI, USA, August 1989, pages 290-296. Morgan Kaufmann, 1989. URL: http://ijcai.org/Proceedings/89-1/Papers/046.pdf.
  4. Martin Gebser, Tomi Janhunen, and Jussi Rintanen. SAT modulo graphs: Acyclicity. In Eduardo Fermé and João Leite, editors, Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, volume 8761 of Lecture Notes in Computer Science, pages 137-151. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11558-0_10.
  5. Kazuo Iwama and Shuichi Miyazaki. Sat-varible complexity of hard combinatorial problems. In Björn Pehrson and Imre Simon, editors, Technology and Foundations - Information Processing '94, Volume 1, Proceedings of the IFIP 13th World Computer Congress, Hamburg, Germany, 28 August - 2 September, 1994, volume A-51 of IFIP Transactions, pages 253-258. North-Holland, 1994. Google Scholar
  6. Mikolas Janota, Radu Grigore, and Vasco M. Manquinho. On the quest for an acyclic graph. CoRR, abs/1708.01745, 2017. URL: https://arxiv.org/abs/1708.01745.
  7. Donald Knuth. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison-Wesley, 2015. Google Scholar
  8. Zhenyu A. Liao, Charupriya Sharma, James Cussens, and Peter van Beek. Finding all bayesian network structures within a factor of optimal. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 7892-7899. AAAI Press, 2019. URL: https://doi.org/10.1609/aaai.v33i01.33017892.
  9. Binda Pandey and Jussi Rintanen. Planning for partial observability by SAT and graph constraints. In Mathijs de Weerdt, Sven Koenig, Gabriele Röger, and Matthijs T. J. Spaan, editors, Proceedings of the Twenty-Eighth International Conference on Automated Planning and Scheduling, ICAPS 2018, Delft, The Netherlands, June 24-29, 2018, pages 190-198. AAAI Press, 2018. URL: https://aaai.org/ocs/index.php/ICAPS/ICAPS18/paper/view/17756.
  10. Masood Feyzbakhsh Rankooh and Jussi Rintanen. Propositional encodings of acyclicity and reachability by using vertex elimination. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pages 5861-5868. AAAI Press, 2022. URL: https://ojs.aaai.org/index.php/AAAI/article/view/20530.
  11. Donald J. Rose, Robert Endre Tarjan, and George S. Lueker. Algorithmic aspects of vertex elimination on graphs. SIAM J. Comput., 5(2):266-283, 1976. URL: https://doi.org/10.1137/0205021.
  12. Neng-Fa Zhou and Håkan Kjellerstrand. The Picat-SAT compiler. In Marco Gavanelli and John H. Reppy, editors, Practical Aspects of Declarative Languages - 18th International Symposium, PADL 2016, St. Petersburg, FL, USA, January 18-19, 2016. Proceedings, volume 9585 of Lecture Notes in Computer Science, pages 48-62. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-28228-2_4.
  13. Neng-Fa Zhou and Håkan Kjellerstrand. Optimizing SAT encodings for arithmetic constraints. In CP, pages 671-686, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_43.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact