Detail publikace

Antichain with SAT and Tries

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

Originální název

Antichain with SAT and Tries

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

SAT, alternating automata, antichain, trie

Autoři

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

Vydáno

27. 8. 2024

Nakladatel

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo

Dagstuhl

ISBN

978-3-95977-334-8

Kniha

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

Edice

Leibniz International Proceedings in Informatics (LIPIcs)

ISSN

1868-8969

Periodikum

Leibniz International Proceedings in Informatics, LIPIcs

Ročník

2024

Číslo

305

Stát

neuvedeno

Strany od

1

Strany do

15

Strany počet

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"
}