Publication Details
Antichain with SAT and Tries
SAT, alternating automata, antichain, trie
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.
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.
@INPROCEEDINGS{FITPUB13356,
author = "Luk\'{a}\v{s} Hol\'{i}k and Pavol Vargov\v{c}\'{i}k",
title = "Antichain with SAT and Tries",
pages = "1--15",
booktitle = "27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) ",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
journal = "Leibniz International Proceedings in Informatics (LIPIcs)",
volume = 2024,
number = 305,
year = 2024,
location = "Dagstuhl, DE",
publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
ISBN = "978-3-95977-334-8",
ISSN = "1868-8969",
doi = "10.4230/LIPIcs.SAT.2024.15",
language = "english",
url = "https://www.fit.vut.cz/research/publication/13356"
}