Publication detail

Antichain with SAT and Tries

VARGOVČÍK, P. HOLÍK, L.

Original Title

Antichain with SAT and Tries

Type

article in a collection out of WoS and Scopus

Language

English

Original 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.

Keywords

SAT, alternating automata, antichain, trie

Authors

VARGOVČÍK, P.; HOLÍK, L.

Released

27. 8. 2024

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Dagstuhl

ISBN

978-3-95977-334-8

Book

27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Edition

Leibniz International Proceedings in Informatics (LIPIcs)

ISBN

1868-8969

Periodical

Leibniz International Proceedings in Informatics, LIPIcs

Year of study

2024

Number

305

State

unknown

Pages from

1

Pages to

15

Pages count

15

URL

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15

BibTex

@inproceedings{BUT194224,
  author="Pavol {Vargovčík} and Lukáš {Holík}",
  title="Antichain with SAT and Tries",
  booktitle="27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)",
  year="2024",
  series="Leibniz International Proceedings in Informatics (LIPIcs)",
  journal="Leibniz International Proceedings in Informatics, LIPIcs",
  volume="2024",
  number="305",
  pages="1--15",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  doi="10.4230/LIPIcs.SAT.2024.15",
  isbn="978-3-95977-334-8",
  issn="1868-8969",
  url="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15"
}