Document Open Access Logo

Antichain with SAT and Tries

Authors Lukáš Holík , Pavol Vargovčík

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2024.15.pdf
  • Filesize: 2.46 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Regular languages
Keywords
  • SAT
  • Trie
  • Antichain
  • Alternating automata
  • Subset query

Metrics

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

Abstract

We introduce a SAT-enabled version of an antichain algorithm for checking language emptiness of alternating finite automata (AFA) with complex transition relations encoded as compact logical formulae. The SAT solver is used to compute predecessors of AFA configurations, and at the same time, to evaluate the subsumption of newly found configurations in the antichain of the previously found ones. The algorithm could be naively implemented by an incremental SAT solver where the growing antichain is represented by adding new clauses. To make it efficient, we 1) force the SAT solver to prioritize largest/subsumption-strongest predecessors (so that weaker configurations are not even generated), and 2) store the antichain clauses in a special variant of a trie that allows fast subsumption testing. The experimental results suggest that the resulting emptiness checker is very efficient compared to the state of the art and that our techniques improve the performance of the SAT solver.

Cite As Get BibTex

Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.15

Author Details

Lukáš Holík
  • Faculty of Information Technology, Brno University of Technology, Czech Republic
Pavol Vargovčík
  • Faculty of Information Technology, Brno University of Technology, Czech Republic

Funding

This work was supported by the Czech Ministry of Education, Youth and Sports ERC.CZ project LL1908 and the FIT BUT internal project FIT-S-23-8151.

Supplementary Materials

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janků, Hsin-Hung Lin, Lukáš Holík, and Wei-Cheng Wu. Efficient handling of string-number conversion. In Proc. of PLDI'20, pages 943-957. ACM, 2020. Google Scholar
  2. Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso. Regular model checking made simple and efficient. In Proc. of CONCUR'02, volume 2421 of LNCS, pages 116-130. Springer, 2002. Google Scholar
  3. Saeed Amizadeh, Sergiy Matyunin, Helmut Weimer, and Marco Maratea. Learning combinatorial optimization algorithms over graphs. In Proc. of NeurIPS'18, volume 31, 2018. Google Scholar
  4. Gilles Audemard and Laurent Simon. Glucose: A solver that predicts learnt clauses quality. In SAT Competition, 2009. Google Scholar
  5. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In SAT Competition, 2020. Google Scholar
  6. Bernard Boigelot and Pierre Wolper. Representing arithmetic constraints with finite automata: an overview. In Proc. of ICLP'02, volume 2401 of LNCS, pages 1-19. Springer, 2002. Google Scholar
  7. Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili. Regular model checking. In Proc. of CAV'20, volume 1855 of LNCS, pages 403-418. Springer, 2000. Google Scholar
  8. Aaron R Bradley. SAT-based model checking without unrolling. In Proc. of VMCAI'11, pages 70-87. Springer, 2011. Google Scholar
  9. Aaron R. Bradley and Zohar Manna. Checking safety by inductive generalization of counterexamples to induction. In Proc. of FMCAD'07, pages 173-180. IEEE Computer Society, 2007. Google Scholar
  10. Robert Brayton and Alan Mishchenko. ABC: An academic industrial-strength verification tool. In Proc. of CAV'10, pages 24-40. Springer, 2010. Google Scholar
  11. Thierry Castell, Claudette Cayrol, Michel Cayrol, and Daniel Le Berre. Using the Davis and Putnam procedure for an efficient computation of preferred models. In Proc. of ECAI'96, volume 96, pages 350-354. Citeseer, 1996. Google Scholar
  12. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. Google Scholar
  13. David Chocholatý, Tomáš Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruška, Ondřej Lengál, and Juraj Síč. Mata: A fast and simple finite automata library. In Proc. of TACAS'24, pages 130-151. Springer, 2024. Google Scholar
  14. Arlen Cox. Model Checking Regular Expressions. url: https://mosca19.github.io/slides/cox.pdf, 2019. Presented at MOSCA'19.
  15. Arlen Cox and Jason Leasure. Model checking regular language constraints. CoRR, abs/1708.09073, 2017. URL: https://arxiv.org/abs/1708.09073.
  16. Loris D'Antoni, Zachary Kincaid, and Fang Wang. A symbolic decision procedure for symbolic alternating finite automata. Electronic Notes in Theoretical Computer Science, 336:79-99, 2018. Google Scholar
  17. Loris D'Antoni and Margus Veanes. Minimization of symbolic automata. ACM SIGPLAN Notices - POPL'14, 49(1):541-553, 2014. Google Scholar
  18. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, July 1960. Google Scholar
  19. M. De Wulf, L. Doyen, N. Maquet, and J. F. Raskin. Antichains: Alternative algorithms for LTL satisfiability and model-checking. In Proc. of TACAS'08, pages 63-77. Springer, 2008. Google Scholar
  20. Giorgio Delzanno and Jean-François Raskin. Symbolic representation of upward-closed sets. In Proc. of TACAS'00, pages 426-441. Springer, 2000. Google Scholar
  21. Emanuele Di Rosa, Enrico Giunchiglia, and Marco Maratea. Solving satisfiability problems with preferences. Constraints, 15:485-515, 2010. Google Scholar
  22. Laurent Doyen and Jean-François Raskin. Antichain algorithms for finite automata. In Proc. of TACAS'10, LNCS. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_2.
  23. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Proc. of SAT'03, volume 2919 of LNCS, pages 502-518. Springer, 2003. Google Scholar
  24. Tomáš Fiedor, Lukáš Holík, Martin Hruška, Adam Rogalewicz, Juraj Síč, and Pavol Vargovčík. Reasoning about regular properties: a comparative study. In Proc. of CADE'23, pages 286-306. Springer, 2023. Google Scholar
  25. Tomáš Fiedor, Lukáš Holík, Petr Janků, Ondřej Lengál, and Tomáš Vojnar. Lazy automata techniques for WS1S. In Proc. of TACAS'17, volume 10205 of LNCS, pages 407-425. Springer, 2017. Google Scholar
  26. Bernd Finkbeiner and Henny Sipma. Checking finite traces using alternating automata. Formal Methods in System Design, 24(2):101-127, 2004. Google Scholar
  27. Edward Fredkin. Trie memory. Communications of the ACM, 3(9):490-499, 1960. Google Scholar
  28. Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, and Peter Schachte. Unbounded model-checking with interpolation for regular language constraints. In Proc. of TACAS'13, LNCS. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_20.
  29. Pierre Ganty, Nicolas Maquet, and Jean-François Raskin. Fixed point guided abstraction refinement for alternating automata. Theory of Computer Science, 411(38-39):3444-3459, 2010. Google Scholar
  30. Gilles Geeraerts, Gabriel Kalyon, Tristan Le Gall, Nicolas Maquet, and Jean-Francois Raskin. Lattice-valued binary decision diagrams. In Proc. of ATVA'10, pages 158-172. Springer, 2010. Google Scholar
  31. Hyojung Han and Fabio Somenzi. Alembic: an efficient algorithm for CNF preprocessing. In Proc. of DAC'07, DAC '07, pages 582-587. ACM, 2007. Google Scholar
  32. Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. Mona: Monadic second-order logic in practice. In Proc. of TACAS '95, volume 1019 of LNCS. Springer, 1995. Google Scholar
  33. Krystof Hoder and Nikolaj Bjørner. Generalized property directed reachability. In Proc. of SAT'12, volume 7317 of LNCS, pages 157-171. Springer, 2012. Google Scholar
  34. Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar. String constraints with concatenation and transducers solved efficiently. PACMPL, 2(POPL), 2018. Google Scholar
  35. Peter Kelb, Tiziana Margaria, Michael Mendler, and Claudia Gsottberger. MOSEL: A sound and efficient tool for m2l(str). In Proc. of CAV '97, volume 1254 of LNCS, pages 448-451. Springer, 1997. URL: https://doi.org/10.1007/3-540-63166-6_45.
  36. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Logic, 2(3):408-429, 2001. Google Scholar
  37. Ondřej Lengál, Jiří Šimáček, and Tomáš Vojnar. VATA: A library for efficient manipulation of non-deterministic tree automata. In Proc. of TACAS'12, volume 7214 of LNCS. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28756-5_7.
  38. João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput., 48(5):506-521, May 1999. Google Scholar
  39. Kenneth L. McMillan. Lazy abstraction with interpolants. In Proc. of CAV'06, volume 4144 of LNCS, pages 123-136. Springer, 2006. Google Scholar
  40. Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton. DAG-aware AIG rewriting a fresh look at combinational logic synthesis. In Proc. of DAC '06, pages 532-535. ACM, 2006. Google Scholar
  41. Anders Møller et al. Brics automata library. URL: https://www.brics.dk/automaton/.
  42. M. W. Moskewicz, L. Zhang, C. F. Madigan, S. Malik, and Y. Zhao. Chaff: Engineering an efficient sat solver. In Design Automation Conference, pages 530-535. IEEE Computer Society, 2001. Google Scholar
  43. Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. In Proc. of ICLR'19, 2019. Google Scholar
  44. Mate Soos. Enhancing CDCL SAT solvers with extended resolution. In Proc. of Pragmatics of SAT. EasyChair, 2010. Google Scholar
  45. Niklas Sörensson and Niklas Eén. Minisat - A SAT solver with conflict-clause minimization. Proc. of SAT'05, pages 1-2, 2005. Google Scholar
  46. Niklas Sörensson and Niklas Eén. Minisat 2.1 and minisat++ 1.0-sat race 2008 editions. Proc. of SAT'09, page 31, 2009. Google Scholar
  47. Dmitriy Traytel. A coalgebraic decision procedure for WS1S. In Proc. of CSL'15, volume 41 of LIPIcs, pages 487-503. Schloss Dagstuhl, 2015. Google Scholar
  48. Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Proc. of LICS'96, volume 1043 of LNCS, pages 238-266. Springer, 1996. Google Scholar
  49. Pavol Vargovčík and Lukáš Holík. Simplifying alternating automata for emptiness testing. In Proc. of APLAS'21, pages 243-264. Springer, 2021. Google Scholar
  50. Pavol Vargovčík. AntiSAT. Software, version 0.1.0., Czech Ministry of Education, Youth and Sports ERC.CZ LL1908 FIT BUT FIT-S-23-8151, (visited on 2024-07-31). URL: https://github.com/p4l1ly/antisat/tree/5901055e699e7b95ba3dec63d11445fcd791f5de
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.22499
  51. Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and Jie-Hong R. Jiang. String analysis via automata manipulation with logic circuit representation. In Proc. of CAV'16, volume 9779 of LNCS. Springer, 2016. Google Scholar
  52. Pierre Wolper. On the use of automata for deciding linear arithmetic. In Proc. of TABLEAUX'09, volume 5607 of LNCS, page 16. Springer, 2009. Google Scholar
  53. Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. of CAV'98, pages 88-97. Springer, 1998. Google Scholar
  54. Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Antichains: A new algorithm for checking universality of finite automata. In Proc. of CAV'06, volume 4144 of LNCS, pages 17-30. Springer, 2006. Google Scholar
  55. Hantao Zhang and Mark Stickel. Implementing the Davis-Putnam method. Journal of Automated Reasoning, 24(1):277-296, 2000. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact